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))