Theory "ordNotationSemantics"

Signature

Definitions

ordModel_def

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

Theorems

WF_ord_less

⊢ WF ord_less

tail_dominated

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

osyntax_EQ_0

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

ordModel_lt_epsilon0

⊢ ∀a. ⟦a⟧ < ε₀

ordModel_BIJ

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

ordModel_11

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

ord_mult_correct

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

ord_less_models_ordlt

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

ord_less_modelled

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

ord_less_expt_monotone

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

ord_add_correct

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

oless_x_End

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

oless_total

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

oless_modelled

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

oless_0a

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

oless_0

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

notation_exists

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

nat_times_omega

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

mvjar_theorem10

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

mvjar_lemma5

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

mvjar_lemma4

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

mvjar_lemma3

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

model_expt

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

kexp_sum_times_nat

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

kexp_mult

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

kexp_lt

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

is_ord_expt

⊢ is_ord e ⇒ is_ord (expt e)

better_pmult_def

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

better_ord_mult_def

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

addL_disappears

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

add_nat1_disappears_kexp

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

add_nat1_disappears

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

add_disappears_kexp

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