Structure ordinalTheory
signature ordinalTheory =
sig
type thm = Thm.thm
(* Definitions *)
val allOrds_def : thm
val dclose_def : thm
val downward_closed_def : thm
val epsilon0_def : thm
val fromNat_def : thm
val oleast_def : thm
val omax_def : thm
val omega_def : thm
val ordADD_def : thm
val ordDIVISION : thm
val ordEXP_def : thm
val ordMULT_def : thm
val ordSUC_def : thm
val ordinal_ABS_def : thm
val ordinal_REP_def : thm
val ordinal_TY_DEF : thm
val ordinal_bijections : thm
val ordlt_def : thm
val polyform_def : thm
val preds_def : thm
val sup_def : thm
(* Theorems *)
val ADD1R : thm
val CNF_nat : thm
val CNF_thm : thm
val IFF_ZERO_lt : thm
val IMAGE_EQ_SING : thm
val IN_preds : thm
val ORD_ONE : thm
val Unum_cle_Uinf : thm
val WIN_allOrds : thm
val ZERO_lt_ordEXP : thm
val ZERO_lt_ordEXP_I : thm
val addL_fixpoint_iff : thm
val add_nat_islimit : thm
val add_omega_islimit : thm
val cord_countable_preds : thm
val countableOrds_dclosed : thm
val countableOrds_uncountable : thm
val csup_lesup : thm
val csup_suple : thm
val csup_thm : thm
val cx_lt_x : thm
val dclose_BIGUNION : thm
val dclose_cardleq_univinf : thm
val elsOf_allOrds : thm
val epsilon0_fixpoint : thm
val epsilon0_least_fixpoint : thm
val eval_poly_def : thm
val eval_poly_ind : thm
val expbound_add : thm
val fixpoints_exist : thm
val fromNat_11 : thm
val fromNat_SUC : thm
val fromNat_compute : thm
val fromNat_eq_omega : thm
val fromNat_lt_epsilon0 : thm
val fromNat_lt_omega : thm
val fromNat_ordlt : thm
val generic_continuity : thm
val is_polyform_CONS_E : thm
val is_polyform_ELthm : thm
val is_polyform_def : thm
val is_polyform_head_dominates_tail : thm
val is_polyform_ind : thm
val islimit_0 : thm
val islimit_SUC : thm
val islimit_SUC_lt : thm
val islimit_fromNat : thm
val islimit_mul_R : thm
val leqLEFT_CANCEL : thm
val lt_omega : thm
val lt_suppreds : thm
val mul_omega_islimit : thm
val no_maximal_ordinal : thm
val oleast_intro : thm
val olog_correct : thm
val omax_EMPTY : thm
val omax_NONE : thm
val omax_SOME : thm
val omax_preds_SUC : thm
val omax_preds_omega : thm
val omax_sup : thm
val omega_MUL_fromNat : thm
val omega_exp_islimit : thm
val omega_islimit : thm
val omega_lt_epsilon0 : thm
val ordADD_0L : thm
val ordADD_ASSOC : thm
val ordADD_CANCEL1 : thm
val ordADD_EQ_0 : thm
val ordADD_MONO : thm
val ordADD_RIGHT_CANCEL : thm
val ordADD_continuous : thm
val ordADD_fromNat : thm
val ordADD_fromNat_omega : thm
val ordADD_le_MONO_L : thm
val ordADD_under_epsilon0 : thm
val ordADD_weak_MONO : thm
val ordDIV_UNIQUE : thm
val ordEXP_1L : thm
val ordEXP_1R : thm
val ordEXP_2R : thm
val ordEXP_ADD : thm
val ordEXP_EQ_0 : thm
val ordEXP_MUL : thm
val ordEXP_ZERO_limit : thm
val ordEXP_ZERO_nonlimit : thm
val ordEXP_continuous : thm
val ordEXP_fromNat : thm
val ordEXP_le_MONO_L : thm
val ordEXP_le_MONO_R : thm
val ordEXP_lt_IFF : thm
val ordEXP_lt_MONO_R : thm
val ordEXP_under_epsilon0 : thm
val ordLOG_correct : thm
val ordMOD_UNIQUE : thm
val ordMULT_0L : thm
val ordMULT_0R : thm
val ordMULT_1L : thm
val ordMULT_1R : thm
val ordMULT_2R : thm
val ordMULT_ASSOC : thm
val ordMULT_CANCEL_R : thm
val ordMULT_EQ_0 : thm
val ordMULT_LDISTRIB : thm
val ordMULT_continuous : thm
val ordMULT_fromNat : thm
val ordMULT_le_MONO_L : thm
val ordMULT_le_MONO_R : thm
val ordMULT_lt_MONO_R : thm
val ordMULT_lt_MONO_R_EQN : thm
val ordMUL_under_epsilon0 : thm
val ordSUC_11 : thm
val ordSUC_MONO : thm
val ordSUC_NUMERAL : thm
val ordSUC_ZERO : thm
val ordZERO_ltSUC : thm
val ord_CASES : thm
val ord_RECURSION : thm
val ord_induction : thm
val orderiso_wobound2 : thm
val orderlt_iso_REFL : thm
val ordinal_ABS_REP_CLASS : thm
val ordinal_IVT : thm
val ordinal_QUOTIENT : thm
val ordle_ANTISYM : thm
val ordle_CANCEL_ADDR : thm
val ordle_EXISTS_ADD : thm
val ordle_TRANS : thm
val ordle_lteq : thm
val ordleq0 : thm
val ordlet_TRANS : thm
val ordlt_CANCEL : thm
val ordlt_CANCEL_ADDL : thm
val ordlt_CANCEL_ADDR : thm
val ordlt_DISCRETE1 : thm
val ordlt_EXISTS_ADD : thm
val ordlt_REFL : thm
val ordlt_SUC : thm
val ordlt_SUC_DISCRETE : thm
val ordlt_TRANS : thm
val ordlt_WF : thm
val ordlt_ZERO : thm
val ordlt_fromNat : thm
val ordlt_mkOrdinal : thm
val ordlt_trichotomy : thm
val ordlte_TRANS : thm
val polyform_0 : thm
val polyform_EQ_NIL : thm
val polyform_UNIQUE : thm
val polyform_eval_poly : thm
val polyform_exists : thm
val predimage_sup_thm : thm
val predimage_suplt_ELIM : thm
val preds_0 : thm
val preds_11 : thm
val preds_EQ_EMPTY : thm
val preds_bij : thm
val preds_downward_closed : thm
val preds_inj_univ : thm
val preds_lesup : thm
val preds_lt_PSUBSET : thm
val preds_omax_SOME_SUC : thm
val preds_ordSUC : thm
val preds_sup : thm
val preds_sup_thm : thm
val preds_suple : thm
val preds_surj : thm
val preds_wobound : thm
val simple_ord_induction : thm
val strict_continuity_preserves_islimit : thm
val sup_EMPTY : thm
val sup_EQ_0 : thm
val sup_SING : thm
val sup_eq_SUC : thm
val sup_eq_max : thm
val sup_eq_sup : thm
val sup_lt_implies : thm
val sup_preds_SUC : thm
val sup_preds_omax_NONE : thm
val sup_thm : thm
val suple_thm : thm
val suppred_suplt_ELIM : thm
val ubsup_thm : thm
val unitinf_univnum : thm
val univ_cord_uncountable : thm
val univ_ord_greater_cardinal : thm
val wellorder_allOrds : thm
val wellorder_ordinal_isomorphism : thm
val x_le_ordEXP_x : thm
val ordinal_grammars : type_grammar.grammar * term_grammar.grammar
(*
[cardinal] Parent theory of "ordinal"
[quotient_list] Parent theory of "ordinal"
[quotient_option] Parent theory of "ordinal"
[quotient_pair] Parent theory of "ordinal"
[quotient_sum] Parent theory of "ordinal"
[allOrds_def] Definition
⊢ allOrds = mkWO {(x,y) | x = y ∨ x < y}
[dclose_def] Definition
⊢ ∀s. dclose s = {x | ∃y. y ∈ s ∧ x < y}
[downward_closed_def] Definition
⊢ ∀s. downward_closed s ⇔ ∀a b. a ∈ s ∧ b < a ⇒ b ∈ s
[epsilon0_def] Definition
⊢ ε₀ = oleast x. ω ** x = x
[fromNat_def] Definition
⊢ 0 = (oleast a. T) ∧ ∀n. &SUC n = (&n)⁺
[oleast_def] Definition
⊢ ∀P. $oleast P = @x. P x ∧ ∀y. y < x ⇒ ¬P y
[omax_def] Definition
⊢ ∀s. omax s = some a. maximal_elements s {(x,y) | x ≤ y} = {a}
[omega_def] Definition
⊢ ω = sup {(&i) | T}
[ordADD_def] Definition
⊢ ∀b. b + 0 = b ∧ (∀a. b + a⁺ = (b + a)⁺) ∧
∀a. 0 < a ∧ islimit a ⇒ b + a = sup (IMAGE ($+ b) (preds a))
[ordDIVISION] Definition
⊢ ∀a b. 0 < b ⇒ a = b * (a / b) + a % b ∧ a % b < b
[ordEXP_def] Definition
⊢ (∀a. a ** 0 = 1) ∧ (∀a a'. a ** a'⁺ = a ** a' * a) ∧
∀a a'.
0 < a' ∧ islimit a' ⇒ a ** a' = sup (IMAGE ($** a) (preds a'))
[ordMULT_def] Definition
⊢ ∀b. b * 0 = 0 ∧ (∀a. b * a⁺ = b * a + b) ∧
∀a. 0 < a ∧ islimit a ⇒ b * a = sup (IMAGE ($* b) (preds a))
[ordSUC_def] Definition
⊢ ∀a. a⁺ = oleast b. a < b
[ordinal_ABS_def] Definition
⊢ ∀r. mkOrdinal r = ordinal_ABS_CLASS (orderiso r)
[ordinal_REP_def] Definition
⊢ ∀a. ordinal_REP a = $@ (ordinal_REP_CLASS a)
[ordinal_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. orderiso r r ∧ c = orderiso r) rep
[ordinal_bijections] Definition
⊢ (∀a. ordinal_ABS_CLASS (ordinal_REP_CLASS a) = a) ∧
∀r. (λc. ∃r. orderiso r r ∧ c = orderiso r) r ⇔
ordinal_REP_CLASS (ordinal_ABS_CLASS r) = r
[ordlt_def] Definition
⊢ ∀T1 T2. T1 < T2 ⇔ orderlt (ordinal_REP T1) (ordinal_REP T2)
[polyform_def] Definition
⊢ ∀a b.
1 < a ⇒
is_polyform a (polyform a b) ∧ b = eval_poly a (polyform a b)
[preds_def] Definition
⊢ ∀w. preds w = {w0 | w0 < w}
[sup_def] Definition
⊢ ∀ordset. sup ordset = oleast a. a ∉ BIGUNION (IMAGE preds ordset)
[ADD1R] Theorem
⊢ a + 1 = a⁺
[CNF_nat] Theorem
⊢ CNF (&n) = if n = 0 then [] else [(&n,0)]
[CNF_thm] Theorem
⊢ ∀b. is_polyform ω (CNF b) ∧ b = eval_poly ω (CNF b)
[IFF_ZERO_lt] Theorem
⊢ (x ≠ 0 ⇔ 0 < x) ∧ (1 ≤ x ⇔ 0 < x)
[IMAGE_EQ_SING] Theorem
⊢ IMAGE f s = {x} ⇔ (∃y. y ∈ s) ∧ ∀y. y ∈ s ⇒ f y = x
[IN_preds] Theorem
⊢ x ∈ preds w ⇔ x < w
[ORD_ONE] Theorem
⊢ 0⁺ = 1
[Unum_cle_Uinf] Theorem
⊢ 𝕌(:num) ≼ 𝕌(:num + α)
[WIN_allOrds] Theorem
⊢ (x,y) WIN allOrds ⇔ x < y
[ZERO_lt_ordEXP] Theorem
⊢ 0 < a ** x ⇔ 0 < a ∨ islimit x
[ZERO_lt_ordEXP_I] Theorem
⊢ ∀a x. 0 < a ⇒ 0 < a ** x
[addL_fixpoint_iff] Theorem
⊢ a + b = b ⇔ a * ω ≤ b
[add_nat_islimit] Theorem
⊢ 0 < n ⇒ (islimit (a + &n) ⇔ F)
[add_omega_islimit] Theorem
⊢ islimit (a + ω)
[cord_countable_preds] Theorem
⊢ countableOrd ord
[countableOrds_dclosed] Theorem
⊢ a < b ∧ countableOrd b ⇒ countableOrd a
[countableOrds_uncountable] Theorem
⊢ ¬COUNTABLE {a | countableOrd a}
[csup_lesup] Theorem
⊢ COUNTABLE s ⇒ ∀d. d ∈ s ⇒ d ≤ sup s
[csup_suple] Theorem
⊢ COUNTABLE s ⇒ (sup s ≤ b ⇔ ∀d. d ∈ s ⇒ d ≤ b)
[csup_thm] Theorem
⊢ COUNTABLE s ⇒ ∀b. b < sup s ⇔ ∃d. d ∈ s ∧ b < d
[cx_lt_x] Theorem
⊢ x * c < x ⇔ 0 < x ∧ c = 0
[dclose_BIGUNION] Theorem
⊢ dclose s = BIGUNION (IMAGE preds s)
[dclose_cardleq_univinf] Theorem
⊢ s ≼ 𝕌(:num + α) ⇒ dclose s ≼ 𝕌(:num + α)
[elsOf_allOrds] Theorem
⊢ elsOf allOrds = 𝕌(:α ordinal)
[epsilon0_fixpoint] Theorem
⊢ ω ** ε₀ = ε₀
[epsilon0_least_fixpoint] Theorem
⊢ ∀a. a < ε₀ ⇒ a < ω ** a ∧ ω ** a < ε₀
[eval_poly_def] Theorem
⊢ (∀a. eval_poly a [] = 0) ∧
∀t e c a. eval_poly a ((c,e)::t) = a ** e * c + eval_poly a t
[eval_poly_ind] Theorem
⊢ ∀P. (∀a. P a []) ∧ (∀a c e t. P a t ⇒ P a ((c,e)::t)) ⇒
∀v v1. P v v1
[expbound_add] Theorem
⊢ ∀a x y. x < ω ** a ∧ y < ω ** a ⇒ x + y < ω ** a
[fixpoints_exist] Theorem
⊢ (∀s. s ≠ ∅ ∧ s ≼ 𝕌(:num + α) ⇒ f (sup s) = sup (IMAGE f s)) ∧
(∀x. x ≤ f x) ⇒
∀a. ∃b. a ≤ b ∧ f b = b
[fromNat_11] Theorem
⊢ ∀x y. &x = &y ⇔ x = y
[fromNat_SUC] Theorem
⊢ ∀n. &SUC n = (&n)⁺
[fromNat_compute] Theorem
⊢ 0 = (oleast a. T) ∧
(∀n. &NUMERAL (BIT1 n) = (&(NUMERAL (BIT1 n) − 1))⁺) ∧
∀n. &NUMERAL (BIT2 n) = (&NUMERAL (BIT1 n))⁺
[fromNat_eq_omega] Theorem
⊢ ∀n. &n ≠ ω
[fromNat_lt_epsilon0] Theorem
⊢ &n < ε₀
[fromNat_lt_omega] Theorem
⊢ ∀n. &n < ω
[fromNat_ordlt] Theorem
⊢ &n < &m ⇔ n < m
[generic_continuity] Theorem
⊢ (∀a. 0 < a ∧ islimit a ⇒ f a = sup (IMAGE f (preds a))) ∧
(∀x y. x ≤ y ⇒ f x ≤ f y) ⇒
∀s. s ≼ 𝕌(:num + α) ∧ s ≠ ∅ ⇒ f (sup s) = sup (IMAGE f s)
[is_polyform_CONS_E] Theorem
⊢ is_polyform a ((c,e)::t) ⇒ 0 < c ∧ c < a ∧ is_polyform a t
[is_polyform_ELthm] Theorem
⊢ is_polyform a ces ⇔
(∀i j. i < j ∧ j < LENGTH ces ⇒ SND (EL j ces) < SND (EL i ces)) ∧
∀c e. MEM (c,e) ces ⇒ 0 < c ∧ c < a
[is_polyform_def] Theorem
⊢ (∀a. is_polyform a [] ⇔ T) ∧
(∀e c a. is_polyform a [(c,e)] ⇔ 0 < c ∧ c < a) ∧
∀t e2 e1 c2 c1 a.
is_polyform a ((c1,e1)::(c2,e2)::t) ⇔
0 < c1 ∧ c1 < a ∧ e2 < e1 ∧ is_polyform a ((c2,e2)::t)
[is_polyform_head_dominates_tail] Theorem
⊢ 1 < a ∧ is_polyform a ((c,e)::t) ⇒ eval_poly a t < a ** e
[is_polyform_ind] Theorem
⊢ ∀P. (∀a. P a []) ∧ (∀a c e. P a [(c,e)]) ∧
(∀a c1 e1 c2 e2 t. P a ((c2,e2)::t) ⇒ P a ((c1,e1)::(c2,e2)::t)) ⇒
∀v v1. P v v1
[islimit_0] Theorem
⊢ islimit 0
[islimit_SUC] Theorem
⊢ islimit x⁺ ⇔ F
[islimit_SUC_lt] Theorem
⊢ islimit b ∧ a < b ⇒ a⁺ < b
[islimit_fromNat] Theorem
⊢ islimit (&x) ⇔ x = 0
[islimit_mul_R] Theorem
⊢ ∀a. islimit a ⇒ islimit (b * a)
[leqLEFT_CANCEL] Theorem
⊢ ∀x a. x ≤ a + x
[lt_omega] Theorem
⊢ ∀a. a < ω ⇔ ∃m. a = &m
[lt_suppreds] Theorem
⊢ ∀b. b < sup (preds a) ⇔ ∃d. d < a ∧ b < d
[mul_omega_islimit] Theorem
⊢ islimit (ω * a)
[no_maximal_ordinal] Theorem
⊢ ∀a. ∃b. a < b
[oleast_intro] Theorem
⊢ ∀Q P.
(∃a. P a) ∧ (∀a. (∀b. b < a ⇒ ¬P b) ∧ P a ⇒ Q a) ⇒ Q ($oleast P)
[olog_correct] Theorem
⊢ 0 < x ⇒ ω ** olog x ≤ x ∧ ∀a. olog x < a ⇒ x < ω ** a
[omax_EMPTY] Theorem
⊢ omax ∅ = NONE
[omax_NONE] Theorem
⊢ omax s = NONE ⇔ ∀a. a ∈ s ⇒ ∃b. b ∈ s ∧ a < b
[omax_SOME] Theorem
⊢ omax s = SOME a ⇔ a ∈ s ∧ ∀b. b ∈ s ⇒ b ≤ a
[omax_preds_SUC] Theorem
⊢ omax (preds a⁺) = SOME a
[omax_preds_omega] Theorem
⊢ islimit ω
[omax_sup] Theorem
⊢ omax s = SOME a ⇒ sup s = a
[omega_MUL_fromNat] Theorem
⊢ 0 < n ⇒ &n * ω = ω
[omega_exp_islimit] Theorem
⊢ 0 < a ⇒ islimit (ω ** a)
[omega_islimit] Theorem
⊢ islimit ω
[omega_lt_epsilon0] Theorem
⊢ ω < ε₀
[ordADD_0L] Theorem
⊢ ∀a. 0 + a = a
[ordADD_ASSOC] Theorem
⊢ ∀a b c. a + (b + c) = a + b + c
[ordADD_CANCEL1] Theorem
⊢ (∀c a. a = a + c ⇔ c = 0) ∧ ∀c a. a + c = a ⇔ c = 0
[ordADD_EQ_0] Theorem
⊢ ∀y x. x + y = 0 ⇔ x = 0 ∧ y = 0
[ordADD_MONO] Theorem
⊢ ∀b a c. a < b ⇒ c + a < c + b
[ordADD_RIGHT_CANCEL] Theorem
⊢ ∀b a c. a + b = a + c ⇔ b = c
[ordADD_continuous] Theorem
⊢ ∀s. s ≼ 𝕌(:num + α) ∧ s ≠ ∅ ⇒ a + sup s = sup (IMAGE ($+ a) s)
[ordADD_fromNat] Theorem
⊢ &n + &m = &(n + m)
[ordADD_fromNat_omega] Theorem
⊢ &n + ω = ω
[ordADD_le_MONO_L] Theorem
⊢ x ≤ y ⇒ x + z ≤ y + z
[ordADD_under_epsilon0] Theorem
⊢ x < ε₀ ∧ y < ε₀ ⇒ x + y < ε₀
[ordADD_weak_MONO] Theorem
⊢ ∀c a b. a < b ⇒ a + c ≤ b + c
[ordDIV_UNIQUE] Theorem
⊢ ∀a b q r. 0 < b ∧ a = b * q + r ∧ r < b ⇒ a / b = q
[ordEXP_1L] Theorem
⊢ ∀a. 1 ** a = 1
[ordEXP_1R] Theorem
⊢ a ** 1 = a
[ordEXP_2R] Theorem
⊢ a ** 2 = a * a
[ordEXP_ADD] Theorem
⊢ 0 < x ⇒ x ** (y + z) = x ** y * x ** z
[ordEXP_EQ_0] Theorem
⊢ ∀y x. x ** y = 0 ⇔ x = 0 ∧ omax (preds y) ≠ NONE
[ordEXP_MUL] Theorem
⊢ 0 < x ⇒ x ** (y * z) = (x ** y) ** z
[ordEXP_ZERO_limit] Theorem
⊢ ∀x. islimit x ⇒ 0 ** x = 1
[ordEXP_ZERO_nonlimit] Theorem
⊢ omax (preds x) ≠ NONE ⇒ 0 ** x = 0
[ordEXP_continuous] Theorem
⊢ ∀a s.
0 < a ∧ s ≼ 𝕌(:num + α) ∧ s ≠ ∅ ⇒
a ** sup s = sup (IMAGE ($** a) s)
[ordEXP_fromNat] Theorem
⊢ &x ** &n = &(x ** n)
[ordEXP_le_MONO_L] Theorem
⊢ ∀x a b. a ≤ b ⇒ a ** x ≤ b ** x
[ordEXP_le_MONO_R] Theorem
⊢ ∀x y a. 0 < a ∧ x ≤ y ⇒ a ** x ≤ a ** y
[ordEXP_lt_IFF] Theorem
⊢ ∀x y a. 1 < a ⇒ (a ** x < a ** y ⇔ x < y)
[ordEXP_lt_MONO_R] Theorem
⊢ ∀y x a. 1 < a ∧ x < y ⇒ a ** x < a ** y
[ordEXP_under_epsilon0] Theorem
⊢ a < ε₀ ∧ b < ε₀ ⇒ a ** b < ε₀
[ordLOG_correct] Theorem
⊢ 1 < b ∧ 0 < x ⇒
b ** ordLOG b x ≤ x ∧ ∀a. ordLOG b x < a ⇒ x < b ** a
[ordMOD_UNIQUE] Theorem
⊢ ∀a b q r. 0 < b ∧ a = b * q + r ∧ r < b ⇒ a % b = r
[ordMULT_0L] Theorem
⊢ ∀a. 0 * a = 0
[ordMULT_0R] Theorem
⊢ ∀a. a * 0 = 0
[ordMULT_1L] Theorem
⊢ ∀a. 1 * a = a
[ordMULT_1R] Theorem
⊢ ∀a. a * 1 = a
[ordMULT_2R] Theorem
⊢ a * 2 = a + a
[ordMULT_ASSOC] Theorem
⊢ ∀a b c. a * (b * c) = a * b * c
[ordMULT_CANCEL_R] Theorem
⊢ z * x = z * y ⇔ z = 0 ∨ x = y
[ordMULT_EQ_0] Theorem
⊢ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0
[ordMULT_LDISTRIB] Theorem
⊢ ∀a b c. c * (a + b) = c * a + c * b
[ordMULT_continuous] Theorem
⊢ ∀s. s ≼ 𝕌(:num + α) ⇒ a * sup s = sup (IMAGE ($* a) s)
[ordMULT_fromNat] Theorem
⊢ &n * &m = &(n * m)
[ordMULT_le_MONO_L] Theorem
⊢ ∀a b c. a ≤ b ⇒ a * c ≤ b * c
[ordMULT_le_MONO_R] Theorem
⊢ ∀a b c. a ≤ b ⇒ c * a ≤ c * b
[ordMULT_lt_MONO_R] Theorem
⊢ ∀a b c. a < b ∧ 0 < c ⇒ c * a < c * b
[ordMULT_lt_MONO_R_EQN] Theorem
⊢ c * a < c * b ⇔ a < b ∧ 0 < c
[ordMUL_under_epsilon0] Theorem
⊢ x < ε₀ ∧ y < ε₀ ⇒ x * y < ε₀
[ordSUC_11] Theorem
⊢ a⁺ = b⁺ ⇔ a = b
[ordSUC_MONO] Theorem
⊢ a⁺ < b⁺ ⇔ a < b
[ordSUC_NUMERAL] Theorem
⊢ (&NUMERAL n)⁺ = &(NUMERAL n + 1)
[ordSUC_ZERO] Theorem
⊢ a⁺ ≠ 0
[ordZERO_ltSUC] Theorem
⊢ 0 < x⁺
[ord_CASES] Theorem
⊢ ∀a. a = 0 ∨ (∃a0. a = a0⁺) ∨ 0 < a ∧ islimit a
[ord_RECURSION] Theorem
⊢ ∀z sf lf. ∃h.
h 0 = z ∧ (∀a. h a⁺ = sf a (h a)) ∧
∀a. 0 < a ∧ islimit a ⇒ h a = lf a (IMAGE h (preds a))
[ord_induction] Theorem
⊢ (∀min. (∀b. b < min ⇒ P b) ⇒ P min) ⇒ ∀a. P a
[orderiso_wobound2] Theorem
⊢ orderiso (wobound x w) (wobound y w) ⇒ (x,y) ∉ strict (destWO w)
[orderlt_iso_REFL] Theorem
⊢ orderiso w1 w2 ⇒ ¬orderlt w1 w2
[ordinal_ABS_REP_CLASS] Theorem
⊢ (∀a. ordinal_ABS_CLASS (ordinal_REP_CLASS a) = a) ∧
∀c. (∃r. orderiso r r ∧ c = orderiso r) ⇔
ordinal_REP_CLASS (ordinal_ABS_CLASS c) = c
[ordinal_IVT] Theorem
⊢ (∀a. 0 < a ∧ islimit a ⇒ f a = sup (IMAGE f (preds a))) ∧
(∀x y. x ≤ y ⇒ f x ≤ f y) ∧ a1 < a2 ∧ f a1 ≤ c ∧ c < f a2 ⇒
∃b. a1 ≤ b ∧ b < a2 ∧ f b ≤ c ∧ c < f b⁺
[ordinal_QUOTIENT] Theorem
⊢ QUOTIENT orderiso mkOrdinal ordinal_REP
[ordle_ANTISYM] Theorem
⊢ a ≤ b ∧ b ≤ a ⇒ a = b
[ordle_CANCEL_ADDR] Theorem
⊢ x ≤ x + a
[ordle_EXISTS_ADD] Theorem
⊢ ∀a b. a ≤ b ⇔ ∃c. b = a + c
[ordle_TRANS] Theorem
⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
[ordle_lteq] Theorem
⊢ a ≤ b ⇔ a < b ∨ a = b
[ordleq0] Theorem
⊢ x ≤ 0 ⇔ x = 0
[ordlet_TRANS] Theorem
⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z
[ordlt_CANCEL] Theorem
⊢ ∀b a c. c + a < c + b ⇔ a < b
[ordlt_CANCEL_ADDL] Theorem
⊢ a + b < a ⇔ F
[ordlt_CANCEL_ADDR] Theorem
⊢ ∀b a. a < a + b ⇔ 0 < b
[ordlt_DISCRETE1] Theorem
⊢ ¬(a < b ∧ b < a⁺)
[ordlt_EXISTS_ADD] Theorem
⊢ ∀a b. a < b ⇔ ∃c. c ≠ 0 ∧ b = a + c
[ordlt_REFL] Theorem
⊢ ∀w. w ≤ w
[ordlt_SUC] Theorem
⊢ a < a⁺
[ordlt_SUC_DISCRETE] Theorem
⊢ a < b⁺ ⇔ a < b ∨ a = b
[ordlt_TRANS] Theorem
⊢ ∀w1 w2 w3. w1 < w2 ∧ w2 < w3 ⇒ w1 < w3
[ordlt_WF] Theorem
⊢ WF $<
[ordlt_ZERO] Theorem
⊢ 0 ≤ a
[ordlt_fromNat] Theorem
⊢ ∀n x. x < &n ⇔ ∃m. x = &m ∧ m < n
[ordlt_mkOrdinal] Theorem
⊢ o1 < o2 ⇔
∀w1 w2. mkOrdinal w1 = o1 ∧ mkOrdinal w2 = o2 ⇒ orderlt w1 w2
[ordlt_trichotomy] Theorem
⊢ ∀w2 w1. w1 < w2 ∨ w1 = w2 ∨ w2 < w1
[ordlte_TRANS] Theorem
⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z
[polyform_0] Theorem
⊢ 1 < a ⇒ polyform a 0 = []
[polyform_EQ_NIL] Theorem
⊢ 1 < a ⇒ (polyform a x = [] ⇔ x = 0)
[polyform_UNIQUE] Theorem
⊢ ∀a b ces.
1 < a ∧ is_polyform a ces ∧ b = eval_poly a ces ⇒
polyform a b = ces
[polyform_eval_poly] Theorem
⊢ 1 < a ∧ is_polyform a b ⇒ polyform a (eval_poly a b) = b
[polyform_exists] Theorem
⊢ ∀a b. 1 < a ⇒ ∃ces. is_polyform a ces ∧ b = eval_poly a ces
[predimage_sup_thm] Theorem
⊢ ∀b. b < sup (IMAGE f (preds a)) ⇔ ∃d. d < a ∧ b < f d
[predimage_suplt_ELIM] Theorem
⊢ sup (IMAGE f (preds a)) < b ⇒ ∀d. d < a ⇒ f d ≤ b
[preds_0] Theorem
⊢ preds 0 = ∅
[preds_11] Theorem
⊢ preds w1 = preds w2 ⇔ w1 = w2
[preds_EQ_EMPTY] Theorem
⊢ preds x = ∅ ⇔ x = 0
[preds_bij] Theorem
⊢ BIJ preds 𝕌(:α ordinal) (downward_closed DELETE 𝕌(:α ordinal))
[preds_downward_closed] Theorem
⊢ downward_closed (preds w)
[preds_inj_univ] Theorem
⊢ preds ord ≼ 𝕌(:num + α)
[preds_lesup] Theorem
⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒ ∀d. d ∈ s ⇒ d ≤ sup s
[preds_lt_PSUBSET] Theorem
⊢ w1 < w2 ⇔ preds w1 ⊂ preds w2
[preds_omax_SOME_SUC] Theorem
⊢ omax (preds a) = SOME b ⇔ a = b⁺
[preds_ordSUC] Theorem
⊢ preds a⁺ = a INSERT preds a
[preds_sup] Theorem
⊢ s ≼ 𝕌(:num + α) ⇒ preds (sup s) = dclose s
[preds_sup_thm] Theorem
⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒
∀b. b < sup s ⇔ ∃d. d ∈ s ∧ b < d
[preds_suple] Theorem
⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒
(sup s ≤ b ⇔ ∀d. d ∈ s ⇒ d ≤ b)
[preds_surj] Theorem
⊢ ∀x. downward_closed x ∧ x ≠ 𝕌(:α ordinal) ⇒ ∃y. preds y = x
[preds_wobound] Theorem
⊢ preds ord = elsOf (wobound ord allOrds)
[simple_ord_induction] Theorem
⊢ ∀P. P 0 ∧ (∀a. P a ⇒ P a⁺) ∧
(∀a. islimit a ∧ 0 < a ∧ (∀b. b < a ⇒ P b) ⇒ P a) ⇒
∀a. P a
[strict_continuity_preserves_islimit] Theorem
⊢ (∀s. s ≼ 𝕌(:num + α) ∧ s ≠ ∅ ⇒ f (sup s) = sup (IMAGE f s)) ∧
(∀x y. x < y ⇒ f x < f y) ∧ islimit a ∧ a ≠ 0 ⇒
islimit (f a)
[sup_EMPTY] Theorem
⊢ sup ∅ = 0
[sup_EQ_0] Theorem
⊢ s ≼ 𝕌(:num + α) ⇒ (sup s = 0 ⇔ s = ∅ ∨ s = {0})
[sup_SING] Theorem
⊢ sup {a} = a
[sup_eq_SUC] Theorem
⊢ s ≼ 𝕌(:num + α) ∧ sup s = a⁺ ⇒ a⁺ ∈ s
[sup_eq_max] Theorem
⊢ (∀b. b ∈ s ⇒ b ≤ a) ∧ a ∈ s ⇒ sup s = a
[sup_eq_sup] Theorem
⊢ s1 ≼ 𝕌(:num + α) ∧ s2 ≼ 𝕌(:num + α) ∧
(∀a. a ∈ s1 ⇒ ∃b. b ∈ s2 ∧ a ≤ b) ∧
(∀b. b ∈ s2 ⇒ ∃a. a ∈ s1 ∧ b ≤ a) ⇒
sup s1 = sup s2
[sup_lt_implies] Theorem
⊢ s ≼ 𝕌(:num + α) ∧ sup s < a ∧ b ∈ s ⇒ b < a
[sup_preds_SUC] Theorem
⊢ sup (preds a⁺) = a
[sup_preds_omax_NONE] Theorem
⊢ islimit a ⇔ sup (preds a) = a
[sup_thm] Theorem
⊢ s ≼ 𝕌(:num + α) ⇒ ∀a. a < sup s ⇔ ∃b. b ∈ s ∧ a < b
[suple_thm] Theorem
⊢ ∀b s. s ≼ 𝕌(:num + α) ∧ b ∈ s ⇒ b ≤ sup s
[suppred_suplt_ELIM] Theorem
⊢ sup (preds a) < b ⇒ ∀d. d < a ⇒ d ≤ b
[ubsup_thm] Theorem
⊢ (∀a. a ∈ s ⇒ a < b) ⇒ ∀c. c < sup s ⇔ ∃d. d ∈ s ∧ c < d
[unitinf_univnum] Theorem
⊢ 𝕌(:num + unit) ≈ 𝕌(:num)
[univ_cord_uncountable] Theorem
⊢ ¬COUNTABLE 𝕌(:unit ordinal)
[univ_ord_greater_cardinal] Theorem
⊢ 𝕌(:num + α) ≺ 𝕌(:α ordinal)
[wellorder_allOrds] Theorem
⊢ wellorder {(x,y) | x = y ∨ x < y}
[wellorder_ordinal_isomorphism] Theorem
⊢ ∀w. orderiso w (wobound (mkOrdinal w) allOrds)
[x_le_ordEXP_x] Theorem
⊢ ∀a x. 1 < a ⇒ x ≤ a ** x
*)
end
HOL 4, Kananaskis-14