Theory "wot"

Parents     indexedLists   patternMatches

Signature

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

Definitions

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

Theorems

StrongWellOrderExists 
⊢ ∃R. StrongLinearOrder R ∧ WF R