Theory "wot"

Parents     rich_list   quantHeuristics

Signature

Constant Type
StrongWellOrder :α toto$reln -> bool
U :(ψ -> bool) toto$reln
WeakWellOrder :α toto$reln -> bool
chain :((ψ -> bool) -> bool) -> bool
comparable :(ψ -> bool) -> bool
cpl :(ψ -> bool) toto$reln
lub_sub :((ψ -> bool) -> bool) -> ψ -> bool
mex :(ψ -> bool) -> ψ
mex_less :ψ toto$reln
mex_less_eq :ψ toto$reln
preds :ψ toto$reln
preds_image :(ψ -> bool) toto$reln
setsuc :(ψ -> bool) -> ψ -> bool
succl :((ψ -> bool) -> bool) -> bool
tower :((ψ -> bool) -> bool) -> bool
uncl :((ψ -> bool) -> bool) -> bool

Definitions

cpl_def 
|- ∀A B. A cpl B ⇔ A ⊆ B ∨ B ⊆ A
chain_def 
|- ∀C. chain C ⇔ ∀a b. a ∈ C ∧ b ∈ C ⇒ a cpl b
mex_def 
|- ∀s. mex s = CHOICE (COMPL s)
setsuc_def 
|- ∀s. setsuc s = mex s INSERT s
succl_def 
|- ∀c. succl c ⇔ ∀s. s ∈ c ⇒ setsuc s ∈ c
uncl_def 
|- ∀c. uncl c ⇔ ∀w. w ⊆ c ∧ chain w ⇒ BIGUNION w ∈ c
tower_def 
|- ∀A. tower A ⇔ succl A ∧ uncl A
mex_less_eq_def 
|- ∀a b. a mex_less_eq b ⇔ preds a ⊆ preds b
mex_less_def 
|- $mex_less = STRORD $mex_less_eq
WeakWellOrder_def 
|- ∀R.
     WeakWellOrder R ⇔ WeakOrder R ∧ ∀B. B ≠ ∅ ⇒ ∃m. m ∈ B ∧ ∀b. b ∈ B ⇒ R m b
preds_image_def 
|- ∀X. preds_image X = {preds x | x ∈ X}
StrongWellOrder_def 
|- ∀R. StrongWellOrder R ⇔ StrongLinearOrder R ∧ WF R

Theorems

StrongWellOrderExists 
|- ∃R. StrongLinearOrder R ∧ WF R