Theory ordinal

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

⊢ ∀a b. ival a b = {e | a < e ∧ e < b}

⊢ ω₁ = sup {a | countableOrd a}

⊢ ∀a b. a / b = FST (ordDIVMOD a b)

⊢ ∀a b.
    0 < b ⇒
    a = b * FST (ordDIVMOD a b) + SND (ordDIVMOD a b) ∧
    SND (ordDIVMOD a b) < b

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

⊢ ∀a b. a % b = SND (ordDIVMOD a b)

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

⊢ ordlt_top =
  topology
    {s |
     (∀e. e ∈ s ⇒
          (∃a b. e ∈ ival a b ∧ ival a b ⊆ s) ∨
          ∃b. e < b ∧ ∀d. d < b ⇒ d ∈ s)}

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

⊢ a + 1 = a⁺

⊢ CARD (preds (&n)) = CARD (preds (&n))

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

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

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

⊢ 𝕌(:num) ≼ 𝕌(:num + (α + num -> bool))

⊢ 𝕌(:num) ≺ 𝕌(:num + (α + num -> bool))

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

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

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

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

⊢ islimit (a + ω)

⊢ closed_in ordlt_top {x}

⊢ countableOrd ord

⊢ a < b ∧ countableOrd b ⇒ countableOrd a

⊢ ¬countable {a | countableOrd a}

⊢ csuc (&n) = (&n)⁺

⊢ csuc ω = ω₁

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

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

⊢ ω ** ε₀ = ε₀

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

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

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

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

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

⊢ &n < ε₀

⊢ (∀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 a ((c,e)::t) ⇒ 0 < c ∧ c < a ∧ is_polyform a t

⊢ is_polyform a ces ⇔
  (∀i j. i < j ∧ j < LENGTH ces ⇒ SND ces❲j❳ < SND ces❲i❳) ∧
  ∀c e. MEM (c,e) ces ⇒ 0 < c ∧ c < a

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

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

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

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

⊢ limpt ordlt_top a (preds a) ⇔ islimit a ∧ a ≠ 0

⊢ islimit (ω * a)

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

⊢ omax s = SOME a ⇒ sup s = a

⊢ ¬countableOrd ω₁

⊢ 0 < n ⇒ &n * ω = ω

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

⊢ ω < ε₀

⊢ open_in ordlt_top s ⇔
  ∀e. e ∈ s ⇒
      (∃a b. e ∈ ival a b ∧ ival a b ⊆ s) ∨ ∃b. e < b ∧ ∀d. d < b ⇒ d ∈ s

⊢ open_in ordlt_top {x} ⇔ omax (preds x) ≠ NONE ∨ x = 0

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

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

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

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

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

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

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

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

⊢ ∀a. 1 ** a = 1

⊢ a ** 1 = a

⊢ a ** 2 = a * a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀a. 0 * a = 0

⊢ ∀a. a * 0 = 0

⊢ ∀a. 1 * a = a

⊢ ∀a. a * 1 = a

⊢ a * 2 = a + a

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

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

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

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

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

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

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

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

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

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

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

⊢ istopology
    {s |
     (∀e. e ∈ s ⇒
          (∃a b. e ∈ ival a b ∧ ival a b ⊆ s) ∨
          ∃b. e < b ∧ ∀d. d < b ⇒ d ∈ s)}

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

⊢ x ≤ x + a

⊢ a < b ⇒ preds a ≼ preds b

⊢ 1 < a ⇒ polyform a 0 = []

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

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

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

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

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

⊢ preds ω ≈ 𝕌(:num)

⊢ preds ω ≺ preds ω₁

⊢ open_in ordlt_top {x | x < a} ∧ open_in ordlt_top {x | a < x}

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

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

⊢ s1 ≼ 𝕌(:num + α) ∧ s2 ≼ 𝕌(:num + α) ∧ (∀a. a ∈ s1 ⇒ ∃b. b ∈ s2 ∧ a ≤ b) ∧
  (∀b. b ∈ s2 ⇒ ∃a. a ∈ s1 ∧ b ≤ a) ⇒
  sup s1 = sup s2

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

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

⊢ topspace ordlt_top = 𝕌(:α ordinal)

⊢ ¬countable 𝕌(:num + (α + num -> bool))

⊢ {a | countableOrd a} ≼ 𝕌(:num + (α + num -> bool))

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

⊢ ¬countable 𝕌(:unit ordinal)

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

⊢ x < ω₁ ⇔ countableOrd x