The Theory wf_relp
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
fill• tc r
fill= (λ s t
fill• ∀ tr
fill• trans tr ∧ (∀ v u• r v u ⇒ tr v u) ⇒ tr s t)
well_founded
⊢ ∀ r
fill• well_founded r
fill⇔ (∀ s
fill• (∀ 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
fill• (∀ x y• r1 x y ⇒ r2 x y)
fill⇒ (∀ 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
fill• well_founded r
fill⇒ (∀ x
fill• (∀ y• tc r y x ⇒ (∀ z• tc r z y ⇒ s z) ⇒ s y)
fill⇒ (∀ y• tc r y x ⇒ s y))
tcwf_lemma2
⊢ ∀ r
fill• well_founded r
fill⇒ (∀ s
fill• (∀ t• (∀ u• tc r u t ⇒ s u) ⇒ s t)
fill⇒ (∀ 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
fill• well_founded r
fill⇒ (∀ x
fill• ¬ (∃ p v
fill• p v
fill∧ (∀ y
fill• p y ⇒ tc r y x ∧ (∃ z• p z ∧ r z y))))
wf_wf_thm
⊢ ∀ r
fill• well_founded r
fill⇒ ¬ (∃ p v
fill• p v ∧ (∀ y• p y ⇒ (∃ z• p z ∧ r z y)))
nochain_wf_thm
⊢ ∀ r
fill• (∀ x
fill• ¬ (∃ p v
fill• p v
fill∧ (∀ y
fill• p y ⇒ tc r y x ∧ (∃ z• p z ∧ r z y))))
fill⇒ well_founded r
wf_induct_thm
⊢ ¬ (∃ p v• p v ∧ (∀ y• p y ⇒ (∃ z• p z ∧ r z y)))
fill⇒ well_founded r
nochain_wf_thm2
⊢ ∀ r
fill• (∀ x
fill• ¬ (∃ p v
fill• p v ∧ (∀ y• p y ⇒ (∃ z• p z ∧ r z y))))
fill⇒ well_founded r
nochain_min_thm
⊢ ∀ r
fill• (∀ x
fill• ¬ (∃ p v
fill• p v
fill∧ (∀ y
fill• p y ⇒ tc r y x ∧ (∃ z• p z ∧ r z y))))
fill⇒ (∀ x
fill• (∃ y• r y x)
fill⇒ (∃ z• r z x ∧ ¬ (∃ v• r v z ∧ r v x)))
nochain_min_thm2
⊢ ∀ r
fill• (∀ x
fill• ¬ (∃ p v
fill• p v ∧ (∀ y• p y ⇒ (∃ z• p z ∧ r z y))))
fill⇒ (∀ p
fill• (∃ y• p y) ⇒ (∃ z• p z ∧ ¬ (∃ v• r v z ∧ p v)))
wf_min_thm
⊢ ∀ r
fill• well_founded r
fill⇒ (∀ x
fill• (∃ y• r y x)
fill⇒ (∃ z• r z x ∧ ¬ (∃ v• r v z ∧ r v x)))
minr_not_wf_thm
⊢ ∃ r
fill• (∀ x
fill• (∃ y• r y x)
fill⇒ (∃ z• r z x ∧ ¬ (∃ v• r v z ∧ r v x)))
fill∧ ¬ well_founded r
wf_restrict_wf_thm
⊢ ∀ r
fill• well_founded r
fill⇒ (∀ r2• well_founded (λ x y• r2 x y ∧ r x y))

up quick index

privacy policy

Created:

V