Theory "ordinal"

Signature

Definitions

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}

dclose_def

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

ordinal_TY_DEF

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

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_REP_def

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

ordinal_ABS_def

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

ordlt_def

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

allOrds_def

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

preds_def

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

downward_closed_def

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

oleast_def

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

ordSUC_def

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

fromNat_def

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

sup_def

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

omax_def

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

ordMULT_def

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

ordDIVISION

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

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

epsilon0_def

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

polyform_def

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

Theorems

lt_suppreds

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

ordADD_fromNat_omega

⊢ &n + ω = ω

omega_islimit

⊢ islimit ω

omax_preds_omega

⊢ islimit ω

ordADD_fromNat

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

ubsup_thm

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

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

fromNat_eq_omega

⊢ ∀n. &n ≠ ω

fromNat_lt_omega

⊢ ∀n. &n < ω

lt_omega

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

fromNat_ordlt

⊢ &n < &m ⇔ n < m

ordlt_fromNat

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

fromNat_11

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

preds_suple

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

preds_lesup

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

preds_sup_thm

⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒ ∀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

preds_sup

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

sup_preds_omax_NONE

⊢ islimit a ⇔ sup (preds a) = 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

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

ordinal_QUOTIENT

⊢ QUOTIENT orderiso mkOrdinal ordinal_REP

ordlt_REFL

⊢ ∀w. w ≤ w

ordlt_TRANS

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

ordlt_WF

⊢ WF $<

ordlt_trichotomy

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

wellorder_allOrds

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

WIN_allOrds

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

elsOf_allOrds

⊢ elsOf allOrds = 𝕌(:α ordinal)

ordlt_mkOrdinal

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

orderlt_iso_REFL

⊢ orderiso w1 w2 ⇒ ¬orderlt w1 w2

orderiso_wobound2

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

wellorder_ordinal_isomorphism

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

IN_preds

⊢ x ∈ preds w ⇔ x < w

preds_11

⊢ preds w1 = preds w2 ⇔ w1 = w2

preds_downward_closed

⊢ downward_closed (preds w)

preds_bij

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

preds_lt_PSUBSET

⊢ w1 < w2 ⇔ preds w1 ⊂ preds w2

preds_wobound

⊢ preds ord = elsOf (wobound ord allOrds)

preds_inj_univ

⊢ preds ord ≼ 𝕌(:α inf)

unitinf_univnum

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

cord_countable_preds

⊢ countableOrd ord

univ_ord_greater_cardinal

⊢ 𝕌(:α inf) <

univ_cord_uncountable

⊢ ¬countable 𝕌(:cord)


ordle_lteq

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


ordle_ANTISYM

⊢ a ≤ b ∧ b ≤ a ⇒ a = b


ordle_TRANS

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


ordlet_TRANS

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


ordlte_TRANS

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


oleast_intro

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


fromNat_def_compute

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


fromNat_SUC

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


ordlt_ZERO

⊢ 0 ≤ a


preds_surj

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


no_maximal_ordinal

⊢ ∀a. ∃b. a < b


ordlt_SUC

⊢ a < a⁺


ordSUC_ZERO

⊢ a⁺ ≠ 0


ordlt_DISCRETE1

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


ordlt_SUC_DISCRETE

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


ordSUC_MONO

⊢ a⁺ < b⁺ ⇔ a < b


ordSUC_11

⊢ a⁺ = b⁺ ⇔ a = b


ord_induction

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


sup_thm

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


suple_thm

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


sup_eq_sup

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


Unum_cle_Uinf

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


csup_thm

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


predimage_sup_thm

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


predimage_suplt_ELIM

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


suppred_suplt_ELIM

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


sup_EMPTY

⊢ sup ∅ = 0


sup_SING

⊢ sup {a} = a


sup_preds_SUC

⊢ sup (preds a⁺) = a


preds_ordSUC

⊢ preds a⁺ = a INSERT preds a


countableOrds_dclosed

⊢ a < b ∧ countableOrd b ⇒ countableOrd a


omax_SOME

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


omax_NONE

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


omax_EMPTY

⊢ omax ∅ = NONE


preds_0

⊢ preds 0 = ∅


ordleq0

⊢ x ≤ 0 ⇔ x = 0


preds_EQ_EMPTY

⊢ preds x = ∅ ⇔ x = 0


omax_sup

⊢ omax s = SOME a ⇒ sup s = a


preds_omax_SOME_SUC

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


omax_preds_SUC

⊢ omax (preds x⁺) = SOME x


ORD_ONE

⊢ 0⁺ = 1


ordSUC_NUMERAL

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


ordZERO_ltSUC

⊢ 0 < x⁺


ordlt_CANCEL_ADDR

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


ordlt_CANCEL_ADDL

⊢ a + b < a ⇔ F


ordADD_CANCEL1

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


ordADD_MONO

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


ordlt_CANCEL

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


ordADD_RIGHT_CANCEL

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


leqLEFT_CANCEL

⊢ ∀x a. x ≤ a + x


ordlt_EXISTS_ADD

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


ordle_EXISTS_ADD

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


ordle_CANCEL_ADDR

⊢ x ≤ x + a


dclose_BIGUNION

⊢ dclose s = BIGUNION (IMAGE preds s)


countableOrds_uncountable

⊢ ¬countable {a | countableOrd a}


dclose_cardleq_univinf

⊢ s ≼ 𝕌(:α inf) ⇒ dclose s ≼ 𝕌(:α inf)


sup_lt_implies

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


sup_eq_max

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


sup_eq_SUC

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


generic_continuity

⊢ (∀a. 0 < a ∧ islimit a ⇒ f a = sup (IMAGE f (preds a))) ∧
  (∀x y. x ≤ y ⇒ f x ≤ f y) ⇒
  ∀s. s ≼ 𝕌(:α inf) ∧ s ≠ ∅ ⇒ f (sup s) = sup (IMAGE f s)


ord_CASES

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


islimit_0

⊢ islimit 0


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⁺


ordADD_continuous

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


ordADD_ASSOC

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


ADD1R

⊢ a + 1 = a⁺


ordADD_weak_MONO

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


ordMULT_0L

⊢ ∀a. 0 * a = 0


ordMULT_0R

⊢ ∀a. a * 0 = 0


ordMULT_1L

⊢ ∀a. 1 * a = a


ordMULT_1R

⊢ ∀a. a * 1 = a


ordMULT_2R

⊢ a * 2 = a + a


islimit_SUC_lt

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


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_lt_MONO_R_EQN

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


ordADD_le_MONO_L

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


ordMULT_le_MONO_L

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


ordMULT_CANCEL_R

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


ordMULT_continuous

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


ordMULT_fromNat

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


omega_MUL_fromNat

⊢ 0 < n ⇒ &n * ω = ω


ordMULT_LDISTRIB

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


ordMULT_ASSOC

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


ordDIV_UNIQUE

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


ordMOD_UNIQUE

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


ordEXP_1R

⊢ a ** 1 = a


ordEXP_1L

⊢ ∀a. 1 ** a = 1


ordEXP_2R

⊢ a ** 2 = a * a


ordEXP_fromNat

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


ordEXP_le_MONO_L

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


IFF_ZERO_lt

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


islimit_SUC

⊢ islimit x⁺ ⇔ F


islimit_fromNat

⊢ islimit (&x) ⇔ x = 0


ordEXP_ZERO_limit

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


ordEXP_ZERO_nonlimit

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


sup_EQ_0

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


ordADD_EQ_0

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


IMAGE_EQ_SING

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


ordMULT_EQ_0

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


ordEXP_EQ_0

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


ZERO_lt_ordEXP_I

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


ZERO_lt_ordEXP

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


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_continuous

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


ordEXP_ADD

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


ordEXP_MUL

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


fixpoints_exist

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


x_le_ordEXP_x

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


epsilon0_fixpoint

⊢ ω ** ε₀ = ε₀


epsilon0_least_fixpoint

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


omega_lt_epsilon0

⊢ ω < ε₀


fromNat_lt_epsilon0

⊢ &n < ε₀


add_nat_islimit

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


strict_continuity_preserves_islimit

⊢ (∀s. s ≼ 𝕌(:α inf) ∧ s ≠ ∅ ⇒ f (sup s) = sup (IMAGE f s)) ∧
  (∀x y. x < y ⇒ f x < f y) ∧ islimit a ∧ a ≠ 0 ⇒
  islimit (f a)


add_omega_islimit

⊢ islimit (a + ω)


islimit_mul_R

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


mul_omega_islimit

⊢ islimit (ω * a)


omega_exp_islimit

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


expbound_add

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


addL_fixpoint_iff

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


ordADD_under_epsilon0

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


ordMUL_under_epsilon0

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


ordEXP_under_epsilon0

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


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


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_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_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


polyform_exists

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


CNF_thm

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


polyform_0

⊢ 1 < a ⇒ polyform a 0 = []


polyform_EQ_NIL

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


is_polyform_CONS_E

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


is_polyform_head_dominates_tail

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


cx_lt_x

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


polyform_UNIQUE

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


polyform_eval_poly

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


CNF_nat

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


ordLOG_correct

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


olog_correct

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