| Parents |
| basic_hol |
| Children |
| orders | set_thms | |
hol |
| Constants |
|
IsSetRep
|
('a  BOOL) BOOL
|
|
$
 |
'a 'a SET BOOL
|
|
$SetComp
|
('a BOOL) 'a SET
|
|
Insert
|
'a 'a SET 'a SET
|
|
Universe
|
'a SET |
|
{}
|
'a SET |
|
~
|
'a SET 'a SET
|
|
$
 |
'a SET 'a SET 'a SET
|
|
$
 |
'a SET 'a SET 'a SET
|
|
$\
|
'a SET 'a SET 'a SET
|
|
$⊖
|
'a SET 'a SET 'a SET
|
|
$
 |
'a SET 'a SET BOOL
|
|
$
 |
'a SET 'a SET BOOL
|
 |
'a SET SET 'a SET
|
 |
'a SET SET 'a SET
|
 |
'a SET 'a SET SET
|
| Types |
|
'1 SET
|
| Fixity |
| Binder: | SetComp |
Left Infix 265: |
\ |
Right Infix 230: |
|
|
|
Right Infix 250: |
⊖ |
Right Infix 260: |
|
Right Infix 270: |
|
| Definitions |
|
IsSetRep
is_set_rep_def
|
 IsSetRep = ( x T)
|
|
SET
set_def
|
 f TypeDefn IsSetRep f
|
|
SetComp
set_comp_def
|
 x p a b  (x {v|p v}  p x)  (a = b ( x x a x b))
|
|
Empty
Universe
Insert
insert_def
|
x y a  x {} x Universe (x Insert y a x = y  x a)
|
|
~
complement_def
|
x a x ~ a x a
|
|
_def
|
x a b x a b x a x b
|
|
_def
|
x a b x a b x a x b
|
|
\
set_dif_def
|
x a b x a \ b x a x b
|
|
⊖
⊖_def
|
x a b x a ⊖ b (x a x b)
|
|
_def
|
a b a b ( x x a  x b)
|
|
_def
|
a b a b a b ( x x a x b)
|
|
_def
|
x a x a ( s x s s a)
|
|
_def
|
x a x a ( s s a x s)
|
|
_def
|
x a x a x a
|
| Theorems |
|
sets_clauses
|
x y p q (x {} F) (x Universe T) (x {v|q} q) (x {v|p v} p x) (x {v|v = y} x = y) (x {y} x = y)
|
|
complement_clauses
|
( x a x ~ a x a)
~ Universe = {} ~ {} = Universe
|
|
_clauses
|
a a {} = a {} a = a a Universe = Universe Universe a = Universe a a = a
|
|
_clauses
|
a a {} = {} {} a = {} a Universe = a Universe a = a a a = a
|
|
set_dif_clauses
|
a
a \ {} = a {} \ a = {} a \ Universe = {} Universe \ a = ~ a a \ a = {}
|
|
⊖_clauses
|
a a ⊖ {} = a {} ⊖ a = a a ⊖ Universe = ~ a Universe ⊖ a = ~ a a ⊖ a = {}
|
|
_clauses
|
a a a {} a a Universe
|
|
_clauses
|
a a a a {} {} Universe
|
|
_clauses
|
{} = {} Universe = Universe
|
|
_clauses
|
{} = Universe Universe = {}
|
|
_clauses
|
a {} = {{}} Universe = Universe a a {} a
|
 _clauses
|
x a {x|F} = {} x {} {} a = a a {} = a {} a = {} a {} = {} a \ {} = a {} \ a = {} a ⊖ {} = a {} ⊖ a = a {} a (a {} a = {}) ({} a a = {}) a {} x {} x {} {} a {} = {{}}
|
|
_in_clauses
|
( x y a (x Universe T) (x {} F) (x Insert y a x = y x a)) ( x a b (x a b x a x b) (x a b x a x b) (x a \ b x a x b) (x a ⊖ b (x a x b))) ( x a (x a ( s x s s a)) (x a ( s s a x s)) ( x a x a x a))
|
|
sets_ext_clauses
|
a b
(a b ( x x a x b) ( x x a x b)) (a b ( x x a x b)) (a = b ( x x a x b))
|
