Documentation

Mathlib.SetTheory.Ordinal.Notation

Ordinal notation #

Constructive ordinal arithmetic for ordinals below ε₀.

We define a type ONote, with constructors 0 : ONote and ONote.oadd e n a representing ω ^ e * n + a. We say that o is in Cantor normal form - ONote.NF o - if either o = 0 or o = ω ^ e * n + a with a < ω ^ e and a in Cantor normal form.

The type NONote is the type of ordinals below ε₀ in Cantor normal form. Various operations (addition, subtraction, multiplication, power function) are defined on ONote and NONote.

inductive ONote :

Recursive definition of an ordinal notation. zero denotes the ordinal 0, and oadd e n a is intended to refer to ω^e * n + a. For this to be valid Cantor normal form, we must have the exponents decrease to the right, but we can't state this condition until we've defined repr, so it is a separate definition NF.

Instances For

    Notation for 0

    Equations
    @[simp]

    Notation for 1

    Equations

    Notation for ω

    Equations
    Instances For
      noncomputable def ONote.repr :

      The ordinal denoted by a notation

      Equations
      Instances For
        def ONote.toStringAux1 (e : ONote) (n : ) (s : String) :

        Auxiliary definition to print an ordinal notation

        Equations
        Instances For

          Print an ordinal notation

          Equations
          • ONote.zero.toString = "0"
          • (e.oadd n ONote.zero).toString = e.toStringAux1 (n) e.toString
          • (e.oadd n a).toString = e.toStringAux1 (n) e.toString ++ " + " ++ a.toString
          Instances For
            def ONote.repr' (prec : ) :

            Print an ordinal notation

            Equations
            Instances For
              Equations
              theorem ONote.lt_def {x : ONote} {y : ONote} :
              x < y x.repr < y.repr
              theorem ONote.le_def {x : ONote} {y : ONote} :
              x y x.repr y.repr

              Convert a Nat into an ordinal

              Equations
              • x = match x with | 0 => 0 | n.succ => ONote.oadd 0 n.succPNat 0
              Instances For
                @[simp]
                theorem ONote.ofNat_zero :
                0 = 0
                @[simp]
                theorem ONote.ofNat_succ (n : ) :
                n.succ = ONote.oadd 0 n.succPNat 0
                instance ONote.nat (n : ) :
                Equations
                @[simp]
                theorem ONote.ofNat_one :
                1 = 1
                @[simp]
                theorem ONote.repr_ofNat (n : ) :
                (n).repr = n
                theorem ONote.repr_one :
                (1).repr = 1
                theorem ONote.omega_le_oadd (e : ONote) (n : ℕ+) (a : ONote) :
                Ordinal.omega ^ e.repr (e.oadd n a).repr
                theorem ONote.oadd_pos (e : ONote) (n : ℕ+) (a : ONote) :
                0 < e.oadd n a

                Compare ordinal notations

                Equations
                Instances For
                  theorem ONote.eq_of_cmp_eq {o₁ : ONote} {o₂ : ONote} :
                  o₁.cmp o₂ = Ordering.eqo₁ = o₂
                  inductive ONote.NFBelow :

                  NFBelow o b says that o is a normal form ordinal notation satisfying repr o < ω ^ b.

                  Instances For
                    class ONote.NF (o : ONote) :

                    A normal form ordinal notation has the form

                    ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ... ω ^ aₖ * nₖ where a₁ > a₂ > ... > aₖ and all the aᵢ are also in normal form.

                    We will essentially only be interested in normal form ordinal notations, but to avoid complicating the algorithms we define everything over general ordinal notations and only prove correctness with normal form as an invariant.

                    Instances
                      theorem ONote.NF.out {o : ONote} [self : o.NF] :
                      Exists o.NFBelow
                      theorem ONote.NFBelow.oadd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} :
                      e.NFa.NFBelow e.repre.repr < b(e.oadd n a).NFBelow b
                      theorem ONote.NFBelow.fst {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : (e.oadd n a).NFBelow b) :
                      e.NF
                      theorem ONote.NF.fst {e : ONote} {n : ℕ+} {a : ONote} :
                      (e.oadd n a).NFe.NF
                      theorem ONote.NFBelow.snd {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : (e.oadd n a).NFBelow b) :
                      a.NFBelow e.repr
                      theorem ONote.NF.snd' {e : ONote} {n : ℕ+} {a : ONote} :
                      (e.oadd n a).NFa.NFBelow e.repr
                      theorem ONote.NF.snd {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) :
                      a.NF
                      theorem ONote.NF.oadd {e : ONote} {a : ONote} (h₁ : e.NF) (n : ℕ+) (h₂ : a.NFBelow e.repr) :
                      (e.oadd n a).NF
                      instance ONote.NF.oadd_zero (e : ONote) (n : ℕ+) [h : e.NF] :
                      (e.oadd n 0).NF
                      Equations
                      • =
                      theorem ONote.NFBelow.lt {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (h : (e.oadd n a).NFBelow b) :
                      e.repr < b
                      theorem ONote.NFBelow_zero {o : ONote} :
                      o.NFBelow 0 o = 0
                      theorem ONote.NF.zero_of_zero {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) (e0 : e = 0) :
                      a = 0
                      theorem ONote.NFBelow.repr_lt {o : ONote} {b : Ordinal.{0}} (h : o.NFBelow b) :
                      o.repr < Ordinal.omega ^ b
                      theorem ONote.NFBelow.mono {o : ONote} {b₁ : Ordinal.{0}} {b₂ : Ordinal.{0}} (bb : b₁ b₂) (h : o.NFBelow b₁) :
                      o.NFBelow b₂
                      theorem ONote.NF.below_of_lt {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}} (H : e.repr < b) :
                      (e.oadd n a).NF(e.oadd n a).NFBelow b
                      theorem ONote.NF.below_of_lt' {o : ONote} {b : Ordinal.{0}} :
                      o.repr < Ordinal.omega ^ bo.NFo.NFBelow b
                      theorem ONote.nfBelow_ofNat (n : ) :
                      (n).NFBelow 1
                      instance ONote.nf_ofNat (n : ) :
                      (n).NF
                      Equations
                      • =
                      Equations
                      theorem ONote.oadd_lt_oadd_1 {e₁ : ONote} {n₁ : ℕ+} {o₁ : ONote} {e₂ : ONote} {n₂ : ℕ+} {o₂ : ONote} (h₁ : (e₁.oadd n₁ o₁).NF) (h : e₁ < e₂) :
                      e₁.oadd n₁ o₁ < e₂.oadd n₂ o₂
                      theorem ONote.oadd_lt_oadd_2 {e : ONote} {o₁ : ONote} {o₂ : ONote} {n₁ : ℕ+} {n₂ : ℕ+} (h₁ : (e.oadd n₁ o₁).NF) (h : n₁ < n₂) :
                      e.oadd n₁ o₁ < e.oadd n₂ o₂
                      theorem ONote.oadd_lt_oadd_3 {e : ONote} {n : ℕ+} {a₁ : ONote} {a₂ : ONote} (h : a₁ < a₂) :
                      e.oadd n a₁ < e.oadd n a₂
                      theorem ONote.cmp_compares (a : ONote) (b : ONote) [a.NF] [b.NF] :
                      (a.cmp b).Compares a b
                      theorem ONote.repr_inj {a : ONote} {b : ONote} [a.NF] [b.NF] :
                      a.repr = b.repr a = b
                      theorem ONote.NF.of_dvd_omega_opow {b : Ordinal.{0}} {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) (d : Ordinal.omega ^ b (e.oadd n a).repr) :
                      b e.repr Ordinal.omega ^ b a.repr
                      theorem ONote.NF.of_dvd_omega {e : ONote} {n : ℕ+} {a : ONote} (h : (e.oadd n a).NF) :
                      Ordinal.omega (e.oadd n a).repre.repr 0 Ordinal.omega a.repr

                      TopBelow b o asserts that the largest exponent in o, if it exists, is less than b. This is an auxiliary definition for decidability of NF.

                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        theorem ONote.nfBelow_iff_topBelow {b : ONote} [b.NF] {o : ONote} :
                        o.NFBelow b.repr o.NF b.TopBelow o
                        Equations
                        def ONote.addAux (e : ONote) (n : ℕ+) (o : ONote) :

                        Auxiliary definition for add

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def ONote.add :
                          ONoteONoteONote

                          Addition of ordinal notations (correct only for normal input)

                          Equations
                          • ONote.zero.add x = x
                          • (e.oadd n a).add x = e.addAux n (a.add x)
                          Instances For
                            Equations
                            @[simp]
                            theorem ONote.zero_add (o : ONote) :
                            0 + o = o
                            theorem ONote.oadd_add (e : ONote) (n : ℕ+) (a : ONote) (o : ONote) :
                            e.oadd n a + o = e.addAux n (a + o)
                            def ONote.sub :
                            ONoteONoteONote

                            Subtraction of ordinal notations (correct only for normal input)

                            Equations
                            Instances For
                              Equations
                              theorem ONote.add_nfBelow {b : Ordinal.{0}} {o₁ : ONote} {o₂ : ONote} :
                              o₁.NFBelow bo₂.NFBelow b(o₁ + o₂).NFBelow b
                              instance ONote.add_nf (o₁ : ONote) (o₂ : ONote) [o₁.NF] [o₂.NF] :
                              (o₁ + o₂).NF
                              Equations
                              • =
                              @[simp]
                              theorem ONote.repr_add (o₁ : ONote) (o₂ : ONote) [o₁.NF] [o₂.NF] :
                              (o₁ + o₂).repr = o₁.repr + o₂.repr
                              theorem ONote.sub_nfBelow {o₁ : ONote} {o₂ : ONote} {b : Ordinal.{0}} :
                              o₁.NFBelow bo₂.NF(o₁ - o₂).NFBelow b
                              instance ONote.sub_nf (o₁ : ONote) (o₂ : ONote) [o₁.NF] [o₂.NF] :
                              (o₁ - o₂).NF
                              Equations
                              • =
                              @[simp]
                              theorem ONote.repr_sub (o₁ : ONote) (o₂ : ONote) [o₁.NF] [o₂.NF] :
                              (o₁ - o₂).repr = o₁.repr - o₂.repr
                              def ONote.mul :
                              ONoteONoteONote

                              Multiplication of ordinal notations (correct only for normal input)

                              Equations
                              • ONote.zero.mul x = 0
                              • x.mul ONote.zero = 0
                              • (e₁.oadd n₁ a₁).mul (e₂.oadd n₂ a₂) = if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ ((e₁.oadd n₁ a₁).mul a₂)
                              Instances For
                                Equations
                                theorem ONote.oadd_mul (e₁ : ONote) (n₁ : ℕ+) (a₁ : ONote) (e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote) :
                                e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂ = if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)
                                theorem ONote.oadd_mul_nfBelow {e₁ : ONote} {n₁ : ℕ+} {a₁ : ONote} {b₁ : Ordinal.{0}} (h₁ : (e₁.oadd n₁ a₁).NFBelow b₁) {o₂ : ONote} {b₂ : Ordinal.{0}} :
                                o₂.NFBelow b₂(e₁.oadd n₁ a₁ * o₂).NFBelow (e₁.repr + b₂)
                                instance ONote.mul_nf (o₁ : ONote) (o₂ : ONote) [o₁.NF] [o₂.NF] :
                                (o₁ * o₂).NF
                                Equations
                                • =
                                @[simp]
                                theorem ONote.repr_mul (o₁ : ONote) (o₂ : ONote) [o₁.NF] [o₂.NF] :
                                (o₁ * o₂).repr = o₁.repr * o₂.repr

                                Calculate division and remainder of o mod ω. split' o = (a, n) means o = ω * a + n.

                                Equations
                                • ONote.zero.split' = (0, 0)
                                • (e.oadd n a).split' = if e = 0 then (0, n) else match a.split' with | (a', m) => ((e - 1).oadd n a', m)
                                Instances For

                                  Calculate division and remainder of o mod ω. split o = (a, n) means o = a + n, where ω ∣ a.

                                  Equations
                                  • ONote.zero.split = (0, 0)
                                  • (e.oadd n a).split = if e = 0 then (0, n) else match a.split with | (a', m) => (e.oadd n a', m)
                                  Instances For
                                    def ONote.scale (x : ONote) :

                                    scale x o is the ordinal notation for ω ^ x * o.

                                    Equations
                                    • x.scale ONote.zero = 0
                                    • x.scale (e.oadd n a) = (x + e).oadd n (x.scale a)
                                    Instances For

                                      mulNat o n is the ordinal notation for o * n.

                                      Equations
                                      • x✝.mulNat x = match x✝, x with | ONote.zero, x => 0 | x, 0 => 0 | e.oadd n a, m.succ => e.oadd (n * m.succPNat) a
                                      Instances For
                                        def ONote.opowAux (e : ONote) (a0 : ONote) (a : ONote) :
                                        ONote

                                        Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in opow

                                        Equations
                                        • e.opowAux a0 a x 0 = 0
                                        • e.opowAux a0 a 0 m.succ = e.oadd m.succPNat 0
                                        • e.opowAux a0 a k.succ x = (e + a0.mulNat k).scale a + e.opowAux a0 a k x
                                        Instances For
                                          def ONote.opowAux2 (o₂ : ONote) (o₁ : ONote × ) :

                                          Auxiliary definition to compute the ordinal notation for the ordinal exponentiation in opow

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def ONote.opow (o₁ : ONote) (o₂ : ONote) :

                                            opow o₁ o₂ calculates the ordinal notation for the ordinal exponential o₁ ^ o₂.

                                            Equations
                                            • o₁.opow o₂ = o₂.opowAux2 o₁.split
                                            Instances For
                                              theorem ONote.opow_def (o₁ : ONote) (o₂ : ONote) :
                                              o₁ ^ o₂ = o₂.opowAux2 o₁.split
                                              theorem ONote.split_eq_scale_split' {o : ONote} {o' : ONote} {m : } [o.NF] :
                                              o.split' = (o', m)o.split = (ONote.scale 1 o', m)
                                              theorem ONote.nf_repr_split' {o : ONote} {o' : ONote} {m : } [o.NF] :
                                              o.split' = (o', m)o'.NF o.repr = Ordinal.omega * o'.repr + m
                                              theorem ONote.scale_eq_mul (x : ONote) [x.NF] (o : ONote) [o.NF] :
                                              x.scale o = x.oadd 1 0 * o
                                              instance ONote.nf_scale (x : ONote) [x.NF] (o : ONote) [o.NF] :
                                              (x.scale o).NF
                                              Equations
                                              • =
                                              @[simp]
                                              theorem ONote.repr_scale (x : ONote) [x.NF] (o : ONote) [o.NF] :
                                              (x.scale o).repr = Ordinal.omega ^ x.repr * o.repr
                                              theorem ONote.nf_repr_split {o : ONote} {o' : ONote} {m : } [o.NF] (h : o.split = (o', m)) :
                                              o'.NF o.repr = o'.repr + m
                                              theorem ONote.split_dvd {o : ONote} {o' : ONote} {m : } [o.NF] (h : o.split = (o', m)) :
                                              theorem ONote.split_add_lt {o : ONote} {e : ONote} {n : ℕ+} {a : ONote} {m : } [o.NF] (h : o.split = (e.oadd n a, m)) :
                                              a.repr + m < Ordinal.omega ^ e.repr
                                              @[simp]
                                              theorem ONote.mulNat_eq_mul (n : ) (o : ONote) :
                                              o.mulNat n = o * n
                                              instance ONote.nf_mulNat (o : ONote) [o.NF] (n : ) :
                                              (o.mulNat n).NF
                                              Equations
                                              • =
                                              @[irreducible]
                                              instance ONote.nf_opowAux (e : ONote) (a0 : ONote) (a : ONote) [e.NF] [a0.NF] [a.NF] (k : ) (m : ) :
                                              (e.opowAux a0 a k m).NF
                                              Equations
                                              • =
                                              instance ONote.nf_opow (o₁ : ONote) (o₂ : ONote) [o₁.NF] [o₂.NF] :
                                              (o₁ ^ o₂).NF
                                              Equations
                                              • =
                                              theorem ONote.scale_opowAux (e : ONote) (a0 : ONote) (a : ONote) [e.NF] [a0.NF] [a.NF] (k : ) (m : ) :
                                              (e.opowAux a0 a k m).repr = Ordinal.omega ^ e.repr * (ONote.opowAux 0 a0 a k m).repr
                                              theorem ONote.repr_opow_aux₁ {e : ONote} {a : ONote} [Ne : e.NF] [Na : a.NF] {a' : Ordinal.{0}} (e0 : e.repr 0) (h : a' < Ordinal.omega ^ e.repr) (aa : a.repr = a') (n : ℕ+) :
                                              theorem ONote.repr_opow_aux₂ {a0 : ONote} {a' : ONote} [N0 : a0.NF] [Na' : a'.NF] (m : ) (d : Ordinal.omega a'.repr) (e0 : a0.repr 0) (h : a'.repr + m < Ordinal.omega ^ a0.repr) (n : ℕ+) (k : ) :
                                              let R := (ONote.opowAux 0 a0 (a0.oadd n a' * m) k m).repr; (k 0R < (Ordinal.omega ^ a0.repr) ^ Order.succ k) (Ordinal.omega ^ a0.repr) ^ k * (Ordinal.omega ^ a0.repr * n + a'.repr) + R = (Ordinal.omega ^ a0.repr * n + a'.repr + m) ^ Order.succ k
                                              theorem ONote.repr_opow (o₁ : ONote) (o₂ : ONote) [o₁.NF] [o₂.NF] :
                                              (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

                                              Given an ordinal, returns inl none for 0, inl (some a) for a+1, and inr f for a limit ordinal a, where f i is a sequence converging to a.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              • ONote.zero.fundamentalSequence = Sum.inl none
                                              Instances For

                                                The property satisfied by fundamentalSequence o:

                                                • inl none means o = 0
                                                • inl (some a) means o = succ a
                                                • inr f means o is a limit ordinal and f is a strictly increasing sequence which converges to o
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  theorem ONote.fundamentalSequenceProp_inl_none (o : ONote) :
                                                  o.FundamentalSequenceProp (Sum.inl none) o = 0
                                                  theorem ONote.fundamentalSequenceProp_inl_some (o : ONote) (a : ONote) :
                                                  o.FundamentalSequenceProp (Sum.inl (some a)) o.repr = Order.succ a.repr (o.NFa.NF)
                                                  theorem ONote.fundamentalSequenceProp_inr (o : ONote) (f : ONote) :
                                                  o.FundamentalSequenceProp (Sum.inr f) o.repr.IsLimit (∀ (i : ), f i < f (i + 1) f i < o (o.NF(f i).NF)) a < o.repr, ∃ (i : ), a < (f i).repr
                                                  theorem ONote.fundamentalSequence_has_prop (o : ONote) :
                                                  o.FundamentalSequenceProp o.fundamentalSequence
                                                  @[irreducible]

                                                  The fast growing hierarchy for ordinal notations < ε₀. This is a sequence of functions ℕ → ℕ indexed by ordinals, with the definition:

                                                  • f_0(n) = n + 1
                                                  • f_(α+1)(n) = f_α^[n](n)
                                                  • f_α(n) = f_(α[n])(n) where α is a limit ordinal and α[i] is the fundamental sequence converging to α
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    theorem ONote.fastGrowing_def {o : ONote} {x : Option ONote (ONote)} (e : o.fundamentalSequence = x) :
                                                    o.fastGrowing = match (motive := (x : Option ONote (ONote)) → o.FundamentalSequenceProp x) x, with | Sum.inl none, x => Nat.succ | Sum.inl (some a), x => fun (i : ) => a.fastGrowing^[i] i | Sum.inr f, x => fun (i : ) => (f i).fastGrowing i
                                                    theorem ONote.fastGrowing_zero' (o : ONote) (h : o.fundamentalSequence = Sum.inl none) :
                                                    o.fastGrowing = Nat.succ
                                                    theorem ONote.fastGrowing_succ (o : ONote) {a : ONote} (h : o.fundamentalSequence = Sum.inl (some a)) :
                                                    o.fastGrowing = fun (i : ) => a.fastGrowing^[i] i
                                                    theorem ONote.fastGrowing_limit (o : ONote) {f : ONote} (h : o.fundamentalSequence = Sum.inr f) :
                                                    o.fastGrowing = fun (i : ) => (f i).fastGrowing i
                                                    @[simp]
                                                    theorem ONote.fastGrowing_one :
                                                    ONote.fastGrowing 1 = fun (n : ) => 2 * n
                                                    @[simp]
                                                    theorem ONote.fastGrowing_two :
                                                    ONote.fastGrowing 2 = fun (n : ) => 2 ^ n * n

                                                    We can extend the fast growing hierarchy one more step to ε₀ itself, using ω^(ω^...^ω^0) as the fundamental sequence converging to ε₀ (which is not an ONote). Extending the fast growing hierarchy beyond this requires a definition of fundamental sequence for larger ordinals.

                                                    Equations
                                                    Instances For

                                                      The type of normal ordinal notations. (It would have been nicer to define this right in the inductive type, but NF o requires repr which requires ONote, so all these things would have to be defined at once, which messes up the VM representation.)

                                                      Equations
                                                      Instances For
                                                        instance NONote.NF (o : NONote) :
                                                        (o).NF
                                                        Equations
                                                        • =
                                                        def NONote.mk (o : ONote) [h : o.NF] :

                                                        Construct a NONote from an ordinal notation (and infer normality)

                                                        Equations
                                                        Instances For
                                                          noncomputable def NONote.repr (o : NONote) :

                                                          The ordinal represented by an ordinal notation. (This function is noncomputable because ordinal arithmetic is noncomputable. In computational applications NONote can be used exclusively without reference to Ordinal, but this function allows for correctness results to be stated.)

                                                          Equations
                                                          • o.repr = (o).repr
                                                          Instances For
                                                            Equations
                                                            Equations
                                                            Equations
                                                            theorem NONote.lt_wf :
                                                            WellFounded fun (x x_1 : NONote) => x < x_1

                                                            Convert a natural number to an ordinal notation

                                                            Equations
                                                            Instances For
                                                              def NONote.cmp (a : NONote) (b : NONote) :

                                                              Compare ordinal notations

                                                              Equations
                                                              • a.cmp b = (a).cmp b
                                                              Instances For
                                                                theorem NONote.cmp_compares (a : NONote) (b : NONote) :
                                                                (a.cmp b).Compares a b
                                                                def NONote.below (a : NONote) (b : NONote) :

                                                                Asserts that repr a < ω ^ repr b. Used in NONote.recOn

                                                                Equations
                                                                • a.below b = (a).NFBelow b.repr
                                                                Instances For
                                                                  def NONote.oadd (e : NONote) (n : ℕ+) (a : NONote) (h : a.below e) :

                                                                  The oadd pseudo-constructor for NONote

                                                                  Equations
                                                                  • e.oadd n a h = (e).oadd n a,
                                                                  Instances For
                                                                    def NONote.recOn {C : NONoteSort u_1} (o : NONote) (H0 : C 0) (H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C eC aC (e.oadd n a h)) :
                                                                    C o

                                                                    This is a recursor-like theorem for NONote suggesting an inductive definition, which can't actually be defined this way due to conflicting dependencies.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For

                                                                      Addition of ordinal notations

                                                                      Equations
                                                                      theorem NONote.repr_add (a : NONote) (b : NONote) :
                                                                      (a + b).repr = a.repr + b.repr

                                                                      Subtraction of ordinal notations

                                                                      Equations
                                                                      theorem NONote.repr_sub (a : NONote) (b : NONote) :
                                                                      (a - b).repr = a.repr - b.repr

                                                                      Multiplication of ordinal notations

                                                                      Equations
                                                                      theorem NONote.repr_mul (a : NONote) (b : NONote) :
                                                                      (a * b).repr = a.repr * b.repr
                                                                      def NONote.opow (x : NONote) (y : NONote) :

                                                                      Exponentiation of ordinal notations

                                                                      Equations
                                                                      Instances For
                                                                        theorem NONote.repr_opow (a : NONote) (b : NONote) :
                                                                        (a.opow b).repr = a.repr ^ b.repr