The Theory gst-ax
Parents

basic_hol
Children

gst-fun
Constants
$
'a GS 'a GS BOOL
Pue
'a 'a GS
IsPue
'a GS BOOL
PueSet
'a GS
$
'a GS 'a GS BOOL
'a GS 'a GS
'a GS 'a GS
ManyOne
('a 'b BOOL) BOOL
'a GS
Image
('a GS 'a GS) 'a GS 'a GS
Galaxy
'a GS 'a GS
Pair
'a GS 'a GS 'a GS
Unit
'a GS 'a GS
Sep
'a GS ('a GS BOOL) 'a GS
$
'a GS 'a GS 'a GS
'a GS 'a GS
$
'a GS 'a GS 'a GS
Types
'1 GS
Fixity


Infix 230: Infix 240:
Axioms
Pue_inj_axiom
OneOne Pue
PueSet_axiom
e e PueSet IsPue e
gs_ext_axiom
s t s = t ( e e s e t)
gs_wf_axiom
p ( s ( e e s p e) p s) ( s p s)
_axiom
s t t s t s
_axiom
s t t s ( e e s t e)
Replacement_axiom
r s
ManyOne r
( t u u t ( v v s r v u))
Galaxy_axiom
s
s Galaxy s
( t
t Galaxy s
t Galaxy s
t Galaxy s
t Galaxy s
( f
Image f t Galaxy s
Image f t Galaxy s))
Definitions
IsPue
s IsPue s ( t Pue t = s)
s t s t ( e e s e t)
ManyOne
r ManyOne r ( x y z r x y r x z y = z)
s s
Image
f s x x Image f s ( e e s x = f e)
Pair
s t e e Pair s t e = s e = t
Unit
s Unit s = Pair s s
Sep
s p e e Sep s p e s p e
s t e e s t e s e t
s s = Sep ( s) ( x t t s x t)
s t s t = Sep s ( x x t)
Theorems
_eq_thm
A B A = B A B B A
_refl_thm
A A A
_thm
e A B e A A B e B
_trans_thm
A B C A B B C A C
_thm
s t t s t s
Pair_eq_thm
s t u v
Pair s t = Pair u v s = u t = v s = v t = u
_thm
A B A A B B A B
_thm1
A B C A C B C A B C
_thm2
A B C D A C B D A B C D
_thm
x s e x s (e s ( y y s e y))
_thm
s t s t t s
_thm
A B A B ( C ( D D B C D) C B)
_thm
s t e e s t e s e t
_thm
A B A B A A B B
_thm1
A B C A C B C A B C
_thm2
A B C D A C B D A B C D
_thm3
A B C C A C B C A B
gst_opext_clauses
s t x f u v e p
s
(t s t s)
(t s ( e e s t e))
(x Image f s ( e e s x = f e))
(Pair s t = Pair u v
s = u t = v s = v t = u)
(e Pair s t e = s e = t)
(Unit s = Unit t s = t)
(e Unit s e = s)
(Pair s t = Unit u s = u t = u)
(Unit s = Pair t u s = t s = u)
(e Sep s p e s p e)
(e s t e s e t)
(e s t e s e t)
gst_relext_clauses
s t
(s = t ( e e s e t))
(s t ( e e s e t))

up quick index © RBJ