Theory "wot"

Parents     list

Signature

Constant Type
StrongWellOrder :α reln -> bool
U :(ψ -> bool) reln
WeakWellOrder :α reln -> bool
chain :((ψ -> bool) -> bool) -> bool
comparable :(ψ -> bool) -> bool
cpl :(ψ -> bool) reln
lub_sub :((ψ -> bool) -> bool) -> ψ -> bool
mex :(ψ -> bool) -> ψ
mex_less :ψ reln
mex_less_eq :ψ reln
preds :ψ reln
preds_image :(ψ -> bool) reln
setsuc :(ψ -> bool) -> ψ -> bool
succl :((ψ -> bool) -> bool) -> bool
t0 :(ψ -> 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
t0_def 
|- t0 = BIGINTER tower
comparable_def 
|- ∀p. comparable p ⇔ ∀q. q ∈ t0 ⇒ p cpl q
U_def 
|- ∀C. U C = {A | A ∈ t0 ∧ (A ⊆ C ∨ setsuc C ⊆ A)}
lub_sub_def 
|- ∀B. lub_sub B = BIGUNION {y | y ∈ t0 ∧ ∀x. x ∈ B ⇒ y ⊆ x}
preds_def 
|- ∀a. preds a = BIGUNION {s | s ∈ t0 ∧ a ∉ s}
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