The Theory gst-ax

Parents

wf_relp

basic_hol

Constants

$_g	GS GS BOOL
$_g	GS GS BOOL
ManyOne	('a 'b BOOL) BOOL
_g	GS GS
_g	GS GS
RelIm	(GS GS BOOL) GS GS
Sep	GS (GS BOOL) GS
galaxy	GS BOOL
Gx	GS GS
transitive	GS BOOL
_g	GS
Imagep	(GS GS) GS GS
Pair	GS GS GS
Unit	GS GS
$_g	GS GS GS
_g	GS GS
$_g	GS GS GS

Types

GS

Fixity

Right Infix 230:

_g

_g

Right Infix 240:

_g

_g

Axioms

gs_ext_axiom	s t s = t ( e e _g s e _g t)
gs_wf_axiom	well_founded $_g
Ontology_axiom	s g s _g g ( t t _g g t _g g ( p ( v v _g p v _g t) p _g g) ( u ( v v _g u ( w v _g w w _g t)) u _g g) ( rel ManyOne rel ( r ( v v _g r ( w w _g t rel w v)) (r _g g r _g g))))

Definitions

_g	s t s _g t ( e e _g s e _g t)
ManyOne	r ManyOne r ( x y z r x y r x z y = z)
_g	s t t _g _g s t _g s
_g	s t t _g _g s ( e t _g e e _g s)
RelIm	rel s t ManyOne rel (t _g RelIm rel s ( e e _g s rel e t))
Sep	s p e e _g Sep s p e _g s p e
galaxy	s galaxy s ( x x _g s) ( t t _g s t _g s _g t _g s _g t _g s ( rel ManyOne rel RelIm rel t _g s RelIm rel t _g s))
Gx	s t t _g Gx s ( g galaxy g s _g g t _g g)
transitive	s transitive s ( e e _g s e _g s)
_g	s s _g _g
Imagep	f s x x _g Imagep f s ( e e _g s x = f e)
Pair	s t e e _g Pair s t e = s e = t
Unit	s Unit s = Pair s s
_g	s t e e _g s _g t e _g s e _g t
_g	s _g s = Sep (_g s) ( x t t _g s x _g t)
_g	s t s _g t = Sep s ( x x _g t)

Theorems

gs_wf_min_thm	x ( y y _g x) ( z z _g x ( v v _g z v _g x))
gs_wf_ind_thm	s ( x ( y y _g x s y) s x) ( x s x)
_g_eq_thm	A B A = B A _g B B _g A
_g_refl_thm	A A _g A
_g_g_thm	e A B e _g A A _g B e _g B
_g_trans_thm	A B C A _g B B _g C A _g C
_g_g_thm	s t t _g s t _g _g s
galaxies__thm	s g s _g g galaxy g
t_in_Gx_t_thm	t t _g Gx t
Gx__g_galaxy	s g galaxy g s _g g Gx s _g g
galaxy_Gx	s galaxy (Gx s)
GalaxiesTransitive_thm	s galaxy s transitive s
GCloseSep	g galaxy g ( s s _g g ( p Sep s p _g g))
Gx_transitive_thm	s transitive (Gx s)
Gx_mono_thm	s t s _g t Gx s _g Gx t
Gx_mono_thm2	s t s _g t Gx s _g Gx t
t_sub_Gx_t_thm	t t _g Gx t
Gx_mono_thm3	s t s _g t s _g Gx t
Gx_trans_thm2	s t s _g t s _g Gx t
Gx_trans_thm3	s t u s _g t t _g Gx u s _g Gx u
G_gC	g galaxy g _g _g g
_g_g_thm	s _g _g t
_g_g_thm	_g _g = _g
GImagepC	g galaxy g ( s s _g g ( f Imagep f s _g g Imagep f s _g g))
Pair_eq_thm	s t u v Pair s t = Pair u v s = u t = v s = v t = u
GClosePair	g galaxy g ( s t s _g g t _g g Pair s t _g g)
GCloseUnit	g galaxy g ( s s _g g Unit s _g g)
_g_g_thm	A B A _g A _g B B _g A _g B
_g_g_thm1	A B C A _g C B _g C A _g B _g C
_g_g_thm2	A B C D A _g C B _g D A _g B _g C _g D
_g_g_clauses	A A _g _g = A _g _g A = A
GClose_g	g galaxy g ( s t s _g g t _g g s _g t _g g)
_g_thm	x s e x _g s (e _g _g s ( y y _g s e _g y))
_g_g_thm	s t s _g t _g t _g s
_g_g_thm	A B A _g B ( C ( D D _g B C _g D) C _g _g B)
_g_g_thm	_g _g = _g
GClose_g	g galaxy g ( s s _g g _g s _g g)
GClose_g	g galaxy g ( s t s _g g t _g g s _g t _g g)
_g_thm	s t e e _g s _g t e _g s e _g t
_g_g_thm	A B A _g B _g A A _g B _g B
_g_g_thm1	A B C A _g C B _g C A _g B _g C
_g_g_thm2	A B C D A _g C B _g D A _g B _g C _g D
_g_g_thm3	A B C C _g A C _g B C _g A _g B
gst_opext_clauses	s t x f u v e p s _g _g (t _g _g s t _g s) (t _g _g s ( e t _g e e _g s)) (x _g Imagep f s ( e e _g s x = f e)) (Pair s t = Pair u v s = u t = v s = v t = u) (e _g Pair s t e = s e = t) (Unit s = Unit t s = t) (e _g Unit s e = s) (Pair s t = Unit u s = u t = u) (Unit s = Pair t u s = t s = u) (e _g Sep s p e _g s p e) (e _g s _g t e _g s e _g t) (e _g s _g t e _g s e _g t)
gst_relext_clauses	s t (s = t ( e e _g s e _g t)) (s _g t ( e e _g s e _g t))

V