Theory ordNotationSemantics

⊢ (∀n. ⟦End n⟧ = &n) ∧ ∀e c t. ⟦Plus e c t⟧ = ω ** ⟦e⟧ * &c + ⟦t⟧

⊢ WF ord_less

⊢ ∀e a. a < ω ** e ⇒ (a + ω ** e = ω ** e)

⊢ e ≠ 0 ∧ 0 < k ∧ a < ω ** e ⇒ (a + ω ** e * &k = ω ** e * &k)

⊢ ω ≤ a ⇒ (&n + a = a)

⊢ e ≠ 0 ∧ 0 < k ⇒ (&n + ω ** e * &k = ω ** e * &k)

⊢ ord_mult a (Plus be bc bt) =
  if a = End 0 then End 0
  else Plus (ord_add (expt a) be) bc (ord_mult a bt)

⊢ pmult a (Plus be bc bt) n =
  if a = End 0 then End 0
  else
    (let
       m = cf2 (expt a) be n
     in
       Plus (padd (expt a) be m) bc (pmult a bt m))

⊢ is_ord e ⇒ is_ord (expt e)

⊢ e1 < e2 ⇒ ω ** e1 * &k < ω ** e2

⊢ ∀e2 e1 c t.
    0 < e2 ∧ t < ω ** e1 ∧ 0 < c ⇒
    ((ω ** e1 * &c + t) * ω ** e2 = ω ** (e1 + e2))

⊢ ∀c2 c t e.
    0 < c2 ∧ 0 < c ∧ t < ω ** e ⇒
    ((ω ** e * &c + t) * &c2 = ω ** e * &(c * c2) + t)

⊢ is_ord a ⇒ (⟦expt a⟧ = if a = End 0 then 0 else olog ⟦a⟧)

⊢ ord_less d b ⇒ cf1 a b ≤ cf1 a d

⊢ ∀a n b. n ≤ cf1 a b ⇒ (cf1 a b = cf2 a b n)

⊢ padd a b (cf1 a b) = ord_add a b

⊢ ∀n a b.
    is_ord a ∧ is_ord b ∧ n ≤ cf1 (expt a) (expt b) ⇒
    (⟦pmult a b n⟧ = ⟦a⟧ * ⟦b⟧)

⊢ ∀e m. 0 < m ∧ 0 < e ⇒ (&m * ω ** e = ω ** e)

⊢ ∀a. a < ε₀ ⇒ ∃n. is_ord n ∧ (⟦n⟧ = a) ∧ (0 < a ⇒ (⟦expt n⟧ = olog a))

⊢ ∀n. oless n (End 0) ⇔ F

⊢ oless (End 0) n ⇔ n ≠ End 0

⊢ is_ord x ∧ is_ord y ⇒ (oless x y ⇔ ⟦x⟧ < ⟦y⟧)

⊢ ∀m n. oless m n ∨ oless n m ∨ (m = n)

⊢ oless x (End n) ⇔ ∃m. (x = End m) ∧ m < n

⊢ is_ord n1 ∧ is_ord n2 ⇒ ((⟦n1⟧ = ⟦n2⟧) ⇔ (n1 = n2))

⊢ BIJ ordModel {n | is_ord n} {a | a < ε₀}

⊢ ∀a. ⟦a⟧ < ε₀

⊢ ∀x y. is_ord x ∧ is_ord y ⇒ (⟦ord_add x y⟧ = ⟦x⟧ + ⟦y⟧)

⊢ ord_less x y ⇒ (expt x = expt y) ∨ ord_less (expt x) (expt y)

⊢ ord_less x y ⇔ is_ord x ∧ is_ord y ∧ ⟦x⟧ < ⟦y⟧

⊢ ∀x. is_ord x ⇒
      (∀y. oless x y ∧ is_ord y ⇒ ⟦x⟧ < ⟦y⟧) ∧
      (¬finp x ⇒ ⟦tail x⟧ < ω ** ⟦expt x⟧)

⊢ ∀x y. is_ord x ∧ is_ord y ⇒ (⟦ord_mult x y⟧ = ⟦x⟧ * ⟦y⟧)

⊢ ∀a. is_ord a ⇒ ((⟦a⟧ = 0) ⇔ (a = End 0))

⊢ ⟦expt t⟧ < ⟦e⟧ ∧ is_ord e ∧ is_ord t ⇒ ⟦t⟧ < ω ** ⟦e⟧