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-13