The Theory ord

Parents

wf_recp

gst-ax

Children

gst

Constants

connected	GS BOOL
ordinal	GS BOOL
$<_o	GS GS BOOL
$_o	GS GS BOOL
suc_o	GS GS
successor	GS BOOL
limit_ordinal	GS BOOL
natural_number	GS BOOL
$<_g_n	GS GS BOOL
rank	GS GS

Fixity

Right Infix 240:

<_g_n

<_o

_o

Definitions

connected	s connected s ( t u t _g s u _g s t _g u t = u u _g t)
ordinal	s ordinal s transitive s connected s
<_o	x y x <_o y ordinal x ordinal y x _g y
_o	x y x _o y ordinal x ordinal y x _g y x = y
suc_o	x suc_o x = x _g Unit x
successor	s successor s ( t ordinal t s = suc_o t)
limit_ordinal	s limit_ordinal s ordinal s successor s s = _g
natural_number	s natural_number s s = _g successor s ( t t _g s t = _g successor t)
<_g_n	x y x <_g_n y natural_number x natural_number y x _g y
rank	x rank x = _g (Imagep (suc_o o rank) x)

Theorems

ordinal__g	ordinal _g
trans_suc_trans	x transitive x transitive (suc_o x)
conn_suc_conn	x connected x connected (suc_o x)
ord_suc_ord_thm	x ordinal x ordinal (suc_o x)
conn_sub_conn	x connected x ( y y _g x connected y)
conn_mem_ord	x ordinal x ( y y _g x connected y)
wf_l1	x x _g x
wf_l2	x y (x _g y y _g x)
wf_l3	x y z (x _g y y _g z z _g x)
tran_mem_ord	x ordinal x ( y y _g x transitive y)
ord_mem_ord	x ordinal x ( y y _g x ordinal y)
GCloseSuc_o	g x galaxy g x _g g suc_o x _g g
tran__thm	x y transitive x transitive y transitive (x _g y)
tran__thm	x y transitive x transitive y transitive (x _g y)
conn__thm	x y connected x connected y connected (x _g y)
ord__thm	x y ordinal x ordinal y ordinal (x _g y)
trich_for_ords_thm	x y ordinal x ordinal y x <_o y x = y y <_o x
successor_ord_thm	x successor x ordinal x
wf_ordinals_thm	well_founded $<_o
wf_nat_thm	well_founded $<_g_n
nat_induct_thm	s ( x ( y y <_g_n x s y) s x) ( x s x)
nat_induct_thm2	p ( x natural_number x ( y y <_g_n x p y) p x) ( x natural_number x p x)
ord_nat_thm	n natural_number n ordinal n
mem_nat_ord_thm	n natural_number n ( m m _g n ordinal m)
ordinal_kind_thm	n ordinal n n = _g successor n limit_ordinal n
nat_not_lim_thm	n natural_number n limit_ordinal n
nat_zero_or_suc_thm	n natural_number n successor n n = _g
mem_not_empty_thm	m n m _g n n = _g
mem_nat_not_lim_thm	m n natural_number n m _g n limit_ordinal m
mem_nat_nat_thm	n natural_number n ( m m _g n natural_number m)
GCloseSuc	g galaxy g ( x x _g g suc_o x _g g)
nat_in_G_g_thm	n natural_number n n _g Gx _g
w_exists_thm	w z z _g w natural_number z

V