Theory "ordNotationSemantics"

Signature

Definitions

ordModel_def

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

Theorems

osyntax_EQ_0

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

oless_0

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

oless_0a

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

oless_x_End

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

is_ord_expt

⊢ is_ord e ⇒ is_ord (expt e)

ordModel_lt_epsilon0

⊢ ∀a. ⟦a⟧ < ε₀

ord_less_models_ordlt

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

oless_total

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

ord_less_modelled

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

oless_modelled

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

WF_ord_less

⊢ WF ord_less

tail_dominated

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

addL_disappears

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

add_nat1_disappears

⊢ ω ≤ a ⇒ &n + a = a

add_nat1_disappears_kexp

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

add_disappears_kexp

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

kexp_lt

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

ord_add_correct

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

notation_exists

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

ordModel_11

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

ordModel_BIJ

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

nat_times_omega

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

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)

ord_mult_correct

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

model_expt

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

ord_less_expt_monotone

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

mvjar_lemma3

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

mvjar_lemma4

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

mvjar_lemma5

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

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)

mvjar_theorem10

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