Theory "ordinal"

Signature

Definitions

sup_def

⊢ ∀ordset. sup ordset = oleast a. a ∉ BIGUNION (IMAGE preds ordset)

preds_def

⊢ ∀w. preds w = {w0 | w0 < w}

polyform_def

⊢ ∀a b.
      1 < a ⇒ is_polyform a (polyform a b) ∧ (b = eval_poly a (polyform a b))

ordSUC_def

⊢ ∀a. a⁺ = oleast b. a < b

ordMULT_def

⊢ ∀b.
      (b * 0 = 0) ∧ (∀a. b * a⁺ = b * a + b) ∧
      ∀a. 0 < a ∧ islimit a ⇒ (b * a = sup (IMAGE ($* b) (preds a)))

ordlt_def

⊢ ∀T1 T2. T1 < T2 ⇔ orderlt (ordinal_REP T1) (ordinal_REP T2)

ordinal_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. orderiso r r ∧ (c = orderiso r)) rep

ordinal_REP_def

⊢ ∀a. ordinal_REP a = $@ (ordinal_REP_CLASS a)

ordinal_bijections

⊢ (∀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)

ordinal_ABS_def

⊢ ∀r. mkOrdinal r = ordinal_ABS_CLASS (orderiso r)

ordEXP_def

⊢ (∀a. a ** 0 = 1) ∧ (∀a a'. a ** a'⁺ = a ** a' * a) ∧
  ∀a a'. 0 < a' ∧ islimit a' ⇒ (a ** a' = sup (IMAGE ($** a) (preds a')))

ordDIVISION

⊢ ∀a b. 0 < b ⇒ (a = b * (a / b) + a % b) ∧ a % b < b

ordADD_def

⊢ ∀b.
      (b + 0 = b) ∧ (∀a. b + a⁺ = (b + a)⁺) ∧
      ∀a. 0 < a ∧ islimit a ⇒ (b + a = sup (IMAGE ($+ b) (preds a)))

omega_def

⊢ ω = sup {(&i) | T}

omax_def

⊢ ∀s. omax s = some a. maximal_elements s {(x,y) | x ≤ y} = {a}

oleast_def

⊢ ∀P. $oleast P = @x. P x ∧ ∀y. y < x ⇒ ¬P y

fromNat_def

⊢ (0 = oleast a. T) ∧ ∀n. &SUC n = (&n)⁺

epsilon0_def

⊢ ε₀ = oleast x. ω ** x = x

downward_closed_def

⊢ ∀s. downward_closed s ⇔ ∀a b. a ∈ s ∧ b < a ⇒ b ∈ s

dclose_def

⊢ ∀s. dclose s = {x | ∃y. y ∈ s ∧ x < y}

allOrds_def

⊢ allOrds = mkWO {(x,y) | (x = y) ∨ x < y}

Theorems

ZERO_lt_ordEXP_I

⊢ ∀a x. 0 < a ⇒ 0 < a ** x

ZERO_lt_ordEXP

⊢ 0 < a ** x ⇔ 0 < a ∨ islimit x

x_le_ordEXP_x

⊢ ∀a x. 1 < a ⇒ x ≤ a ** x

WIN_allOrds

⊢ (x,y) WIN allOrds ⇔ x < y

wellorder_ordinal_isomorphism

⊢ ∀w. orderiso w (wobound (mkOrdinal w) allOrds)

wellorder_allOrds

⊢ wellorder {(x,y) | (x = y) ∨ x < y}

Unum_cle_Uinf

⊢ 𝕌(:num) ≼ 𝕌(:num + α)

univ_ord_greater_cardinal

⊢ 𝕌(:num + α) ≺ 𝕌(:α ordinal)

univ_cord_uncountable

⊢ ¬COUNTABLE 𝕌(:unit ordinal)

unitinf_univnum

⊢ 𝕌(:num + unit) ≈ 𝕌(:num)

ubsup_thm

⊢ (∀a. a ∈ s ⇒ a < b) ⇒ ∀c. c < sup s ⇔ ∃d. d ∈ s ∧ c < d

suppred_suplt_ELIM

⊢ sup (preds a) < b ⇒ ∀d. d < a ⇒ d ≤ b

suple_thm

⊢ ∀b s. s ≼ 𝕌(:num + α) ∧ b ∈ s ⇒ b ≤ sup s

sup_thm

⊢ s ≼ 𝕌(:num + α) ⇒ ∀a. a < sup s ⇔ ∃b. b ∈ s ∧ a < b

sup_SING

⊢ sup {a} = a

sup_preds_SUC

⊢ sup (preds a⁺) = a

sup_preds_omax_NONE

⊢ islimit a ⇔ (sup (preds a) = a)

sup_lt_implies

⊢ s ≼ 𝕌(:num + α) ∧ sup s < a ∧ b ∈ s ⇒ b < a

sup_eq_sup

⊢ 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_eq_SUC

⊢ s ≼ 𝕌(:num + α) ∧ (sup s = a⁺) ⇒ a⁺ ∈ s

sup_eq_max

⊢ (∀b. b ∈ s ⇒ b ≤ a) ∧ a ∈ s ⇒ (sup s = a)

sup_EQ_0

⊢ s ≼ 𝕌(:num + α) ⇒ ((sup s = 0) ⇔ (s = ∅) ∨ (s = {0}))

sup_EMPTY

⊢ sup ∅ = 0

strict_continuity_preserves_islimit

⊢ (∀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)

simple_ord_induction

⊢ ∀P.
      P 0 ∧ (∀a. P a ⇒ P a⁺) ∧
      (∀a. islimit a ∧ 0 < a ∧ (∀b. b < a ⇒ P b) ⇒ P a) ⇒
      ∀a. P a

preds_wobound

⊢ preds ord = elsOf (wobound ord allOrds)

preds_surj

⊢ ∀x. downward_closed x ∧ x ≠ 𝕌(:α ordinal) ⇒ ∃y. preds y = x

preds_suple

⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒ (sup s ≤ b ⇔ ∀d. d ∈ s ⇒ d ≤ b)

preds_sup_thm

⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒ ∀b. b < sup s ⇔ ∃d. d ∈ s ∧ b < d

preds_sup

⊢ s ≼ 𝕌(:num + α) ⇒ (preds (sup s) = dclose s)

preds_ordSUC

⊢ preds a⁺ = a INSERT preds a

preds_omax_SOME_SUC

⊢ (omax (preds a) = SOME b) ⇔ (a = b⁺)

preds_lt_PSUBSET

⊢ w1 < w2 ⇔ preds w1 ⊂ preds w2

preds_lesup

⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒ ∀d. d ∈ s ⇒ d ≤ sup s

preds_inj_univ

⊢ preds ord ≼ 𝕌(:num + α)

preds_EQ_EMPTY

⊢ (preds x = ∅) ⇔ (x = 0)

preds_downward_closed

⊢ downward_closed (preds w)

preds_bij

⊢ BIJ preds 𝕌(:α ordinal) (downward_closed DELETE 𝕌(:α ordinal))

preds_11

⊢ (preds w1 = preds w2) ⇔ (w1 = w2)

preds_0

⊢ preds 0 = ∅

predimage_suplt_ELIM

⊢ sup (IMAGE f (preds a)) < b ⇒ ∀d. d < a ⇒ f d ≤ b

predimage_sup_thm

⊢ ∀b. b < sup (IMAGE f (preds a)) ⇔ ∃d. d < a ∧ b < f d

polyform_UNIQUE

⊢ ∀a b ces.
      1 < a ∧ is_polyform a ces ∧ (b = eval_poly a ces) ⇒ (polyform a b = ces)

polyform_exists

⊢ ∀a b. 1 < a ⇒ ∃ces. is_polyform a ces ∧ (b = eval_poly a ces)

polyform_eval_poly

⊢ 1 < a ∧ is_polyform a b ⇒ (polyform a (eval_poly a b) = b)

polyform_EQ_NIL

⊢ 1 < a ⇒ ((polyform a x = []) ⇔ (x = 0))

polyform_0

⊢ 1 < a ⇒ (polyform a 0 = [])

ordZERO_ltSUC

⊢ 0 < x⁺

ordSUC_ZERO

⊢ a⁺ ≠ 0

ordSUC_NUMERAL

⊢ (&NUMERAL n)⁺ = &(NUMERAL n + 1)

ordSUC_MONO

⊢ a⁺ < b⁺ ⇔ a < b

ordSUC_11

⊢ (a⁺ = b⁺) ⇔ (a = b)

ordMULT_lt_MONO_R_EQN

⊢ c * a < c * b ⇔ a < b ∧ 0 < c

ordMULT_lt_MONO_R

⊢ ∀a b c. a < b ∧ 0 < c ⇒ c * a < c * b

ordMULT_le_MONO_R

⊢ ∀a b c. a ≤ b ⇒ c * a ≤ c * b

ordMULT_le_MONO_L

⊢ ∀a b c. a ≤ b ⇒ a * c ≤ b * c

ordMULT_LDISTRIB

⊢ ∀a b c. c * (a + b) = c * a + c * b

ordMULT_fromNat

⊢ &n * &m = &(n * m)

ordMULT_EQ_0

⊢ ∀x y. (x * y = 0) ⇔ (x = 0) ∨ (y = 0)

ordMULT_continuous

⊢ ∀s. s ≼ 𝕌(:num + α) ⇒ (a * sup s = sup (IMAGE ($* a) s))

ordMULT_CANCEL_R

⊢ (z * x = z * y) ⇔ (z = 0) ∨ (x = y)

ordMULT_ASSOC

⊢ ∀a b c. a * (b * c) = a * b * c

ordMULT_2R

⊢ a * 2 = a + a

ordMULT_1R

⊢ ∀a. a * 1 = a

ordMULT_1L

⊢ ∀a. 1 * a = a

ordMULT_0R

⊢ ∀a. a * 0 = 0

ordMULT_0L

⊢ ∀a. 0 * a = 0

ordMUL_under_epsilon0

⊢ x < ε₀ ∧ y < ε₀ ⇒ x * y < ε₀

ordMOD_UNIQUE

⊢ ∀a b q r. 0 < b ∧ (a = b * q + r) ∧ r < b ⇒ (a % b = r)

ordlte_TRANS

⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z

ordlt_ZERO

⊢ 0 ≤ a

ordlt_WF

⊢ WF $<

ordlt_trichotomy

⊢ ∀w2 w1. w1 < w2 ∨ (w1 = w2) ∨ w2 < w1

ordlt_TRANS

⊢ ∀w1 w2 w3. w1 < w2 ∧ w2 < w3 ⇒ w1 < w3

ordlt_SUC_DISCRETE

⊢ a < b⁺ ⇔ a < b ∨ (a = b)

ordlt_SUC

⊢ a < a⁺

ordlt_REFL

⊢ ∀w. w ≤ w

ordlt_mkOrdinal

⊢ o1 < o2 ⇔ ∀w1 w2. (mkOrdinal w1 = o1) ∧ (mkOrdinal w2 = o2) ⇒ orderlt w1 w2

ordlt_fromNat

⊢ ∀n x. x < &n ⇔ ∃m. (x = &m) ∧ m < n

ordlt_EXISTS_ADD

⊢ ∀a b. a < b ⇔ ∃c. c ≠ 0 ∧ (b = a + c)

ordlt_DISCRETE1

⊢ ¬(a < b ∧ b < a⁺)

ordlt_CANCEL_ADDR

⊢ ∀b a. a < a + b ⇔ 0 < b

ordlt_CANCEL_ADDL

⊢ a + b < a ⇔ F

ordlt_CANCEL

⊢ ∀b a c. c + a < c + b ⇔ a < b

ordLOG_correct

⊢ 1 < b ∧ 0 < x ⇒ b ** ordLOG b x ≤ x ∧ ∀a. ordLOG b x < a ⇒ x < b ** a

ordlet_TRANS

⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z

ordleq0

⊢ x ≤ 0 ⇔ (x = 0)

ordle_TRANS

⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z

ordle_lteq

⊢ a ≤ b ⇔ a < b ∨ (a = b)

ordle_EXISTS_ADD

⊢ ∀a b. a ≤ b ⇔ ∃c. b = a + c

ordle_CANCEL_ADDR

⊢ x ≤ x + a

ordle_ANTISYM

⊢ a ≤ b ∧ b ≤ a ⇒ (a = b)

ordinal_QUOTIENT

⊢ QUOTIENT orderiso mkOrdinal ordinal_REP

ordinal_IVT

⊢ (∀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_ABS_REP_CLASS

⊢ (∀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)

ordEXP_ZERO_nonlimit

⊢ omax (preds x) ≠ NONE ⇒ (0 ** x = 0)

ordEXP_ZERO_limit

⊢ ∀x. islimit x ⇒ (0 ** x = 1)

ordEXP_under_epsilon0

⊢ a < ε₀ ∧ b < ε₀ ⇒ a ** b < ε₀

ordEXP_MUL

⊢ 0 < x ⇒ (x ** (y * z) = (x ** y) ** z)

ordEXP_lt_MONO_R

⊢ ∀y x a. 1 < a ∧ x < y ⇒ a ** x < a ** y

ordEXP_lt_IFF

⊢ ∀x y a. 1 < a ⇒ (a ** x < a ** y ⇔ x < y)

ordEXP_le_MONO_R

⊢ ∀x y a. 0 < a ∧ x ≤ y ⇒ a ** x ≤ a ** y

ordEXP_le_MONO_L

⊢ ∀x a b. a ≤ b ⇒ a ** x ≤ b ** x

ordEXP_fromNat

⊢ &x ** &n = &(x ** n)

ordEXP_EQ_0

⊢ ∀y x. (x ** y = 0) ⇔ (x = 0) ∧ omax (preds y) ≠ NONE

ordEXP_continuous

⊢ ∀a s. 0 < a ∧ s ≼ 𝕌(:num + α) ∧ s ≠ ∅ ⇒ (a ** sup s = sup (IMAGE ($** a) s))

ordEXP_ADD

⊢ 0 < x ⇒ (x ** (y + z) = x ** y * x ** z)

ordEXP_2R

⊢ a ** 2 = a * a

ordEXP_1R

⊢ a ** 1 = a

ordEXP_1L

⊢ ∀a. 1 ** a = 1

orderlt_iso_REFL

⊢ orderiso w1 w2 ⇒ ¬orderlt w1 w2

orderiso_wobound2

⊢ orderiso (wobound x w) (wobound y w) ⇒ (x,y) ∉ strict (destWO w)

ordDIV_UNIQUE

⊢ ∀a b q r. 0 < b ∧ (a = b * q + r) ∧ r < b ⇒ (a / b = q)

ordADD_weak_MONO

⊢ ∀c a b. a < b ⇒ a + c ≤ b + c

ordADD_under_epsilon0

⊢ x < ε₀ ∧ y < ε₀ ⇒ x + y < ε₀

ordADD_RIGHT_CANCEL

⊢ ∀b a c. (a + b = a + c) ⇔ (b = c)

ordADD_MONO

⊢ ∀b a c. a < b ⇒ c + a < c + b

ordADD_le_MONO_L

⊢ x ≤ y ⇒ x + z ≤ y + z

ordADD_fromNat_omega

⊢ &n + ω = ω

ordADD_fromNat

⊢ &n + &m = &(n + m)

ordADD_EQ_0

⊢ ∀y x. (x + y = 0) ⇔ (x = 0) ∧ (y = 0)

ordADD_continuous

⊢ ∀s. s ≼ 𝕌(:num + α) ∧ s ≠ ∅ ⇒ (a + sup s = sup (IMAGE ($+ a) s))

ordADD_CANCEL1

⊢ (∀c a. (a = a + c) ⇔ (c = 0)) ∧ ∀c a. (a + c = a) ⇔ (c = 0)

ordADD_ASSOC

⊢ ∀a b c. a + (b + c) = a + b + c

ordADD_0L

⊢ ∀a. 0 + a = a

ord_RECURSION

⊢ ∀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_ONE

⊢ 0⁺ = 1

ord_induction

⊢ (∀min. (∀b. b < min ⇒ P b) ⇒ P min) ⇒ ∀a. P a

ord_CASES

⊢ ∀a. (a = 0) ∨ (∃a0. a = a0⁺) ∨ 0 < a ∧ islimit a

omega_MUL_fromNat

⊢ 0 < n ⇒ (&n * ω = ω)

omega_lt_epsilon0

⊢ ω < ε₀

omega_islimit

⊢ islimit ω

omega_exp_islimit

⊢ 0 < a ⇒ islimit (ω ** a)

omax_sup

⊢ (omax s = SOME a) ⇒ (sup s = a)

omax_SOME

⊢ (omax s = SOME a) ⇔ a ∈ s ∧ ∀b. b ∈ s ⇒ b ≤ a

omax_preds_SUC

⊢ omax (preds a⁺) = SOME a

omax_preds_omega

⊢ islimit ω

omax_NONE

⊢ (omax s = NONE) ⇔ ∀a. a ∈ s ⇒ ∃b. b ∈ s ∧ a < b

omax_EMPTY

⊢ omax ∅ = NONE

olog_correct

⊢ 0 < x ⇒ ω ** olog x ≤ x ∧ ∀a. olog x < a ⇒ x < ω ** a

oleast_intro

⊢ ∀Q P. (∃a. P a) ∧ (∀a. (∀b. b < a ⇒ ¬P b) ∧ P a ⇒ Q a) ⇒ Q ($oleast P)

no_maximal_ordinal

⊢ ∀a. ∃b. a < b

mul_omega_islimit

⊢ islimit (ω * a)

lt_suppreds

⊢ ∀b. b < sup (preds a) ⇔ ∃d. d < a ∧ b < d

lt_omega

⊢ ∀a. a < ω ⇔ ∃m. a = &m

leqLEFT_CANCEL

⊢ ∀x a. x ≤ a + x

islimit_SUC_lt

⊢ islimit b ∧ a < b ⇒ a⁺ < b

islimit_SUC

⊢ islimit x⁺ ⇔ F

islimit_mul_R

⊢ ∀a. islimit a ⇒ islimit (b * a)

islimit_fromNat

⊢ islimit (&x) ⇔ (x = 0)

islimit_0

⊢ islimit 0

is_polyform_ind

⊢ ∀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

is_polyform_head_dominates_tail

⊢ 1 < a ∧ is_polyform a ((c,e)::t) ⇒ eval_poly a t < a ** e

is_polyform_ELthm

⊢ 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

⊢ (∀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_CONS_E

⊢ is_polyform a ((c,e)::t) ⇒ 0 < c ∧ c < a ∧ is_polyform a t

IN_preds

⊢ x ∈ preds w ⇔ x < w

IMAGE_EQ_SING

⊢ (IMAGE f s = {x}) ⇔ (∃y. y ∈ s) ∧ ∀y. y ∈ s ⇒ (f y = x)

IFF_ZERO_lt

⊢ (x ≠ 0 ⇔ 0 < x) ∧ (1 ≤ x ⇔ 0 < x)

generic_continuity

⊢ (∀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))

fromNat_SUC

⊢ ∀n. &SUC n = (&n)⁺

fromNat_ordlt

⊢ &n < &m ⇔ n < m

fromNat_lt_omega

⊢ ∀n. &n < ω

fromNat_lt_epsilon0

⊢ &n < ε₀

fromNat_eq_omega

⊢ ∀n. &n ≠ ω

fromNat_compute

⊢ (0 = oleast a. T) ∧ (∀n. &NUMERAL (BIT1 n) = (&(NUMERAL (BIT1 n) − 1))⁺) ∧
  ∀n. &NUMERAL (BIT2 n) = (&NUMERAL (BIT1 n))⁺

fromNat_11

⊢ ∀x y. (&x = &y) ⇔ (x = y)

fixpoints_exist

⊢ (∀s. s ≠ ∅ ∧ s ≼ 𝕌(:num + α) ⇒ (f (sup s) = sup (IMAGE f s))) ∧
  (∀x. x ≤ f x) ⇒
  ∀a. ∃b. a ≤ b ∧ (f b = b)

expbound_add

⊢ ∀a x y. x < ω ** a ∧ y < ω ** a ⇒ x + y < ω ** a

eval_poly_ind

⊢ ∀P. (∀a. P a []) ∧ (∀a c e t. P a t ⇒ P a ((c,e)::t)) ⇒ ∀v v1. P v v1

eval_poly_def

⊢ (∀a. eval_poly a [] = 0) ∧
  ∀t e c a. eval_poly a ((c,e)::t) = a ** e * c + eval_poly a t

epsilon0_least_fixpoint

⊢ ∀a. a < ε₀ ⇒ a < ω ** a ∧ ω ** a < ε₀

epsilon0_fixpoint

⊢ ω ** ε₀ = ε₀

elsOf_allOrds

⊢ elsOf allOrds = 𝕌(:α ordinal)

dclose_cardleq_univinf

⊢ s ≼ 𝕌(:num + α) ⇒ dclose s ≼ 𝕌(:num + α)

dclose_BIGUNION

⊢ dclose s = BIGUNION (IMAGE preds s)

cx_lt_x

⊢ x * c < x ⇔ 0 < x ∧ (c = 0)

csup_thm

⊢ COUNTABLE s ⇒ ∀b. b < sup s ⇔ ∃d. d ∈ s ∧ b < d

csup_suple

⊢ COUNTABLE s ⇒ (sup s ≤ b ⇔ ∀d. d ∈ s ⇒ d ≤ b)

csup_lesup

⊢ COUNTABLE s ⇒ ∀d. d ∈ s ⇒ d ≤ sup s

countableOrds_uncountable

⊢ ¬COUNTABLE {a | countableOrd a}

countableOrds_dclosed

⊢ a < b ∧ countableOrd b ⇒ countableOrd a

cord_countable_preds

⊢ countableOrd ord

CNF_thm

⊢ ∀b. is_polyform ω (CNF b) ∧ (b = eval_poly ω (CNF b))

CNF_nat

⊢ CNF (&n) = if n = 0 then [] else [(&n,0)]

addL_fixpoint_iff

⊢ (a + b = b) ⇔ a * ω ≤ b

add_omega_islimit

⊢ islimit (a + ω)

add_nat_islimit

⊢ 0 < n ⇒ (islimit (a + &n) ⇔ F)

ADD1R

⊢ a + 1 = a⁺