| Parents |
| hol |
| Children |
| surreal | gst-ax | wf_recp |
| Constants |
|
trans
|
('a  'a BOOL) BOOL
|
|
tc
|
('a 'a BOOL) 'a 'a BOOL
|
|
well_founded
|
('a 'a BOOL) BOOL
|
|
twfp
|
('a 'a BOOL) BOOL
|
| Definitions |
|
trans
|
  r trans r  ( s t u r s t  r t u  r s u)
|
|
tc
|
r  tc r = ( s t tr trans tr ( v u r v u tr v u) tr s t)
|
|
well_founded
|
r well_founded r ( s ( x ( y r y x s y) s x) ( x s x))
|
|
twfp
|
r twfp r well_founded r trans r
|
| Theorems |
|
tran_tc_thm
|
r trans (tc r)
|
|
tran_tc_thm2
|
r x y z tc r x y tc r y z tc r x z
|
|
tc_incr_thm
|
r x y r x y tc r x y
|
|
tc_decomp_thm
|
r x y tc r x y  r x y ( z tc r x z r z y)
|
|
tc_mono_thm
|
r1 r2 ( x y r1 x y r2 x y) ( x y tc r1 x y tc r2 x y)
|
|
tc_p_thm
|
r p ( x y r x y p x) ( x y tc r x y p x)
|
|
tcwf_lemma1
|
s r well_founded r ( x ( y tc r y x ( z tc r z y s z) s y) ( y tc r y x s y))
|
|
tcwf_lemma2
|
r well_founded r ( s ( t ( u tc r u t s u) s t) ( e s e))
|
|
wf_tc_wf_thm
|
r well_founded r well_founded (tc r)
|
|
tc_wf_wf_thm
|
r well_founded (tc r) well_founded r
|
|
tc_wf_twf_thm
|
r well_founded r twfp (tc r)
|
|
wf_nochain_thm
|
r
well_founded r ( x ( p v p v ( y p y tc r y x ( z p z r z y))))
|
|
wf_wf_thm
|
r well_founded r ( p v p v ( y p y ( z p z r z y)))
|
|
nochain_wf_thm
|
r
( x ( p v p v ( y p y tc r y x ( z p z r z y)))) well_founded r
|
|
wf_induct_thm
|
( p v p v ( y p y ( z p z r z y)))
well_founded r
|
|
nochain_wf_thm2
|
r
( x ( p v p v ( y p y ( z p z r z y)))) well_founded r
|
|
nochain_min_thm
|
r
( x ( p v p v ( y p y tc r y x ( z p z r z y)))) ( x ( y r y x) ( z r z x ( v r v z r v x)))
|
|
nochain_min_thm2
|
r
( x ( p v p v ( y p y ( z p z r z y)))) ( p ( y p y) ( z p z ( v r v z p v)))
|
|
wf_min_thm
|
r well_founded r ( x ( y r y x) ( z r z x ( v r v z r v x)))
|
|
minr_not_wf_thm
|
r
( x ( y r y x) ( z r z x ( v r v z r v x))) well_founded r
|
|
wf_restrict_wf_thm
|
r
well_founded r ( r2 well_founded ( x y r2 x y r x y))
|
