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