Documentation

Arithmetization.ISigmaOne.HFS.Vec

Vec #

Equations
  • LO.Arith.instCons_arithmetization = { cons := fun (x x_1 : V) => x, x_1 + 1 }
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem LO.Arith.cons_def {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
      cons x v = x, v + 1
      @[simp]
      theorem LO.Arith.fstIdx_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
      @[simp]
      theorem LO.Arith.sndIdx_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
      theorem LO.Arith.succ_eq_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
      x + 1 = cons (π₁ x) (π₂ x)
      @[simp]
      theorem LO.Arith.lt_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
      x < cons x v
      @[simp]
      theorem LO.Arith.lt_cons' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
      v < cons x v
      @[simp]
      theorem LO.Arith.zero_lt_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
      0 < cons x v
      @[simp]
      theorem LO.Arith.cons_ne_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
      cons x v 0
      @[simp]
      theorem LO.Arith.zero_ne_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
      0 cons x v
      theorem LO.Arith.nil_or_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (z : V) :
      z = 0 ∃ (x : V) (v : V), z = cons x v
      @[simp]
      theorem LO.Arith.cons_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x₁ : V) (x₂ : V) (v₁ : V) (v₂ : V) :
      cons x₁ v₁ = cons x₂ v₂ x₁ = x₂ v₁ = v₂
      theorem LO.Arith.cons_le_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x₁ : V} {x₂ : V} {v₁ : V} {v₂ : V} (hx : x₁ x₂) (hv : v₁ v₂) :
      cons x₁ v₁ cons x₂ v₂
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • =
          Equations
          • =
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            instance LO.Arith.mkVec₂_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
            𝚺₁-Function₂ fun (x y : V) => ?[x, y]
            Equations
            • =
            instance LO.Arith.mkVec₂_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
            { Γ := Γ, rank := m + 1 }-Function₂ fun (x y : V) => ?[x, y]
            Equations
            • =

            N-th element of List #

            def LO.Arith.Nth.Phi {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (C : Set V) (pr : V) :
            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • LO.Arith.Nth.construction = { Φ := fun (x : Fin 0V) => LO.Arith.Nth.Phi, defined := , monotone := }
                Instances For
                  Equations
                  • LO.Arith.Nth.instFiniteConstruction = { finite := }
                  Equations
                  • LO.Arith.Nth.Graph = LO.Arith.Nth.construction.Fixpoint ![]
                  Instances For
                    def LO.Arith.Nth.graphDef :
                    𝚺₁.Semisentence 1
                    Equations
                    Instances For
                      Equations
                      • =
                      instance LO.Arith.Nth.graph_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
                      { Γ := 𝚺, rank := 0 + 1 }-Predicate LO.Arith.Nth.Graph
                      Equations
                      • =
                      @[simp]
                      theorem LO.Arith.Nth.zero_ne_add_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
                      0 x + 1

                      TODO: move

                      theorem LO.Arith.Nth.graph_case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {pr : V} :
                      LO.Arith.Nth.Graph pr (∃ (v : V), pr = v, 0, LO.Arith.fstIdx v) ∃ (v : V) (i : V) (x : V), pr = v, i + 1, x LO.Arith.Nth.Graph LO.Arith.sndIdx v, i, x
                      theorem LO.Arith.Nth.graph_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {x : V} :
                      LO.Arith.Nth.Graph v, 0, x x = LO.Arith.fstIdx v
                      theorem LO.Arith.Nth.graph_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} {x : V} :
                      LO.Arith.Nth.Graph v, i + 1, x LO.Arith.Nth.Graph LO.Arith.sndIdx v, i, x
                      theorem LO.Arith.Nth.graph_exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (i : V) :
                      ∃ (x : V), LO.Arith.Nth.Graph v, i, x
                      theorem LO.Arith.Nth.graph_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} {x₁ : V} {x₂ : V} :
                      LO.Arith.Nth.Graph v, i, x₁LO.Arith.Nth.Graph v, i, x₂x₁ = x₂
                      theorem LO.Arith.Nth.graph_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (i : V) :
                      ∃! x : V, LO.Arith.Nth.Graph v, i, x
                      def LO.Arith.nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (i : V) :
                      V
                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem LO.Arith.nth_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (i : V) :
                          LO.Arith.Nth.Graph v, i, LO.Arith.nth v i
                          theorem LO.Arith.nth_eq_of_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} {x : V} (h : LO.Arith.Nth.Graph v, i, x) :
                          theorem LO.Arith.nth_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (i : V) :
                          @[simp]
                          theorem LO.Arith.nth_cons_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
                          LO.Arith.nth (cons x v) 0 = x
                          @[simp]
                          theorem LO.Arith.nth_cons_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) (i : V) :
                          LO.Arith.nth (cons x v) (i + 1) = LO.Arith.nth v i
                          @[simp]
                          theorem LO.Arith.nth_cons_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
                          @[simp]
                          theorem LO.Arith.nth_cons_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
                          theorem LO.Arith.cons_cases {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
                          x = 0 ∃ (y : V) (v : V), x = cons y v
                          theorem LO.Arith.cons_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P vP (Cons.cons x v)) (v : V) :
                          P v
                          theorem LO.Arith.cons_induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚺₁-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P vP (Cons.cons x v)) (v : V) :
                          P v
                          theorem LO.Arith.cons_induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : VProp} (hP : 𝚷₁-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P vP (Cons.cons x v)) (v : V) :
                          P v
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • =
                            instance LO.Arith.nth_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                            { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.nth
                            Equations
                            • =
                            theorem LO.Arith.cons_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : ) (v : ) :
                            (cons a v) = cons a v

                            TODO: move

                            @[simp]
                            theorem LO.Arith.nth_zero_idx {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) :
                            theorem LO.Arith.nth_lt_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} (hv : 0 < v) (i : V) :
                            @[simp]
                            theorem LO.Arith.nth_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (i : V) :

                            Inductivly Construction of Function on List #

                            structure LO.Arith.VecRec.Blueprint (arity : ) :
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def LO.Arith.VecRec.Blueprint.graphDef {arity : } (β : LO.Arith.VecRec.Blueprint arity) :
                                𝚺₁.Semisentence (arity + 1)
                                Equations
                                • β.graphDef = β.blueprint.fixpointDef
                                Instances For
                                  def LO.Arith.VecRec.Blueprint.resultDef {arity : } (β : LO.Arith.VecRec.Blueprint arity) :
                                  𝚺₁.Semisentence (arity + 2)
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    structure LO.Arith.VecRec.Construction (V : Type u_1) [LO.ORingStruc V] {arity : } (β : LO.Arith.VecRec.Blueprint arity) :
                                    Type u_1
                                    Instances For
                                      theorem LO.Arith.VecRec.Construction.cons_defined {V : Type u_1} [LO.ORingStruc V] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (self : LO.Arith.VecRec.Construction V β) :
                                      LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin arity.succ.succ.succV) => self.cons (fun (x : Fin arity) => v x.succ.succ.succ) (v 0) (v 1) (v 2)) β.cons
                                      def LO.Arith.VecRec.Construction.Phi {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) (C : Set V) (pr : V) :
                                      Equations
                                      • c.Phi param C pr = (pr = 0, c.nil param ∃ (x : V) (xs : V) (ih : V), pr = cons x xs, c.cons param x xs ih xs, ih C)
                                      Instances For
                                        Equations
                                        • c.construction = { Φ := c.Phi, defined := , monotone := }
                                        Instances For
                                          Equations
                                          • c.instFiniteConstruction = { finite := }
                                          def LO.Arith.VecRec.Construction.Graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) :
                                          VProp
                                          Equations
                                          • c.Graph param = c.construction.Fixpoint param
                                          Instances For
                                            theorem LO.Arith.VecRec.Construction.graph_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) :
                                            LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin arity.succV) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)) β.graphDef
                                            instance LO.Arith.VecRec.Construction.graph_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) :
                                            𝚺₁.Boldface fun (v : Fin arity.succV) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)
                                            Equations
                                            • =
                                            instance LO.Arith.VecRec.Construction.graph_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) :
                                            𝚺₁-Predicate c.Graph param
                                            Equations
                                            • =
                                            instance LO.Arith.VecRec.Construction.graph_definable'' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) :
                                            { Γ := 𝚺, rank := 0 + 1 }-Predicate c.Graph param
                                            Equations
                                            • =
                                            theorem LO.Arith.VecRec.Construction.graph_case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) {param : Fin arityV} {pr : V} :
                                            c.Graph param pr pr = 0, c.nil param ∃ (x : V) (xs : V) (ih : V), pr = cons x xs, c.cons param x xs ih c.Graph param xs, ih
                                            theorem LO.Arith.VecRec.Construction.graph_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) {param : Fin arityV} {l : V} :
                                            c.Graph param 0, l l = c.nil param
                                            theorem LO.Arith.VecRec.Construction.graph_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) {param : Fin arityV} {x : V} {xs : V} {y : V} :
                                            c.Graph param cons x xs, y ∃ (y' : V), y = c.cons param x xs y' c.Graph param xs, y'
                                            theorem LO.Arith.VecRec.Construction.graph_exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) (xs : V) :
                                            ∃ (y : V), c.Graph param xs, y
                                            theorem LO.Arith.VecRec.Construction.graph_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) {param : Fin arityV} {xs : V} {y₁ : V} {y₂ : V} :
                                            c.Graph param xs, y₁c.Graph param xs, y₂y₁ = y₂
                                            theorem LO.Arith.VecRec.Construction.graph_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) (xs : V) :
                                            ∃! y : V, c.Graph param xs, y
                                            def LO.Arith.VecRec.Construction.result {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) (xs : V) :
                                            V
                                            Equations
                                            Instances For
                                              theorem LO.Arith.VecRec.Construction.result_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) (xs : V) :
                                              c.Graph param xs, c.result param xs
                                              theorem LO.Arith.VecRec.Construction.result_eq_of_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) {xs : V} {y : V} (h : c.Graph param xs, y) :
                                              c.result param xs = y
                                              @[simp]
                                              theorem LO.Arith.VecRec.Construction.result_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) :
                                              c.result param 0 = c.nil param
                                              @[simp]
                                              theorem LO.Arith.VecRec.Construction.result_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arityV) (x : V) (xs : V) :
                                              c.result param (cons x xs) = c.cons param x xs (c.result param xs)
                                              theorem LO.Arith.VecRec.Construction.result_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) :
                                              LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin arity.succV) => c.result (fun (x : Fin arity) => v x.succ) (v 0)) β.resultDef
                                              @[simp]
                                              theorem LO.Arith.VecRec.Construction.eval_resultDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (v : Fin (arity + 2)V) :
                                              V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val β.resultDef) v 0 = c.result (fun (x : Fin arity) => v x.succ.succ) (v 1)
                                              instance LO.Arith.VecRec.Construction.result_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) :
                                              𝚺₁.BoldfaceFunction fun (v : Fin arity.succV) => c.result (fun (x : Fin arity) => v x.succ) (v 0)
                                              Equations
                                              • =
                                              instance LO.Arith.VecRec.Construction.result_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (Γ : LO.SigmaPiDelta) (m : ) :
                                              { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin arity.succV) => c.result (fun (x : Fin arity) => v x.succ) (v 0)
                                              Equations
                                              • =

                                              Length of List #

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • LO.Arith.Len.construction = { nil := fun (x : Fin 0V) => 0, cons := fun (x : Fin 0V) (x x ih : V) => ih + 1, nil_defined := , cons_defined := }
                                                Instances For
                                                  def LO.Arith.len {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                  V
                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem LO.Arith.len_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
                                                    Equations
                                                    • =
                                                    instance LO.Arith.len_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                    { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.len
                                                    Equations
                                                    • =
                                                    @[simp]
                                                    theorem LO.Arith.nth_lt_len {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} (hl : LO.Arith.len v i) :
                                                    @[simp]
                                                    theorem LO.Arith.len_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                    theorem LO.Arith.nth_ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v₁ : V} {v₂ : V} (hl : LO.Arith.len v₁ = LO.Arith.len v₂) (H : i < LO.Arith.len v₁, LO.Arith.nth v₁ i = LO.Arith.nth v₂ i) :
                                                    v₁ = v₂
                                                    theorem LO.Arith.nth_ext' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (l : V) {v₁ : V} {v₂ : V} (hl₁ : LO.Arith.len v₁ = l) (hl₂ : LO.Arith.len v₂ = l) (H : i < l, LO.Arith.nth v₁ i = LO.Arith.nth v₂ i) :
                                                    v₁ = v₂
                                                    theorem LO.Arith.le_of_nth_le_nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v₁ : V} {v₂ : V} (hl : LO.Arith.len v₁ = LO.Arith.len v₂) (H : i < LO.Arith.len v₁, LO.Arith.nth v₁ i LO.Arith.nth v₂ i) :
                                                    v₁ v₂
                                                    theorem LO.Arith.nth_lt_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} (hi : i < LO.Arith.len v) :
                                                    theorem LO.Arith.sigmaOne_skolem_vec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : VVProp} (hP : 𝚺₁-Relation R) {l : V} (H : x < l, ∃ (y : V), R x y) :
                                                    ∃ (v : V), LO.Arith.len v = l i < l, R i (LO.Arith.nth v i)
                                                    theorem LO.Arith.eq_singleton_iff_len_eq_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} :
                                                    LO.Arith.len v = 1 ∃ (x : V), v = ?[x]
                                                    theorem LO.Arith.eq_doubleton_of_len_eq_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} :
                                                    LO.Arith.len v = 2 ∃ (x : V) (y : V), v = ?[x, y]

                                                    Maximum of List #

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      Equations
                                                      • LO.Arith.ListMax.construction = { nil := fun (x : Fin 0V) => 0, cons := fun (x : Fin 0V) (x x_1 ih : V) => max x ih, nil_defined := , cons_defined := }
                                                      Instances For
                                                        def LO.Arith.listMax {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                        V
                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem LO.Arith.listMax_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
                                                          Equations
                                                          • =
                                                          instance LO.Arith.listMax_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                          { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.listMax
                                                          Equations
                                                          • =
                                                          theorem LO.Arith.listMaxss_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {z : V} (h : i < LO.Arith.len v, LO.Arith.nth v i z) :

                                                          Take Last k-Element #

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              def LO.Arith.takeLast {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (k : V) :
                                                              V
                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem LO.Arith.takeLast_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} (x : V) (v : V) :
                                                                LO.Arith.takeLast (cons x v) k = if LO.Arith.len v < k then cons x v else LO.Arith.takeLast v k
                                                                Equations
                                                                • =
                                                                instance LO.Arith.takeLast_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                                { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.takeLast
                                                                Equations
                                                                • =
                                                                @[simp]
                                                                theorem LO.Arith.add_sub_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) (c : V) :
                                                                a + c - (b + c) = a - b

                                                                TODO: move

                                                                @[simp]

                                                                Concatation #

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • LO.Arith.Concat.construction = { nil := fun (param : Fin 1V) => ?[param 0], cons := fun (x : Fin 1V) (x x_1 ih : V) => cons x ih, nil_defined := , cons_defined := }
                                                                  Instances For
                                                                    def LO.Arith.concat {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (z : V) :
                                                                    V
                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem LO.Arith.concat_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (z : V) :
                                                                      @[simp]
                                                                      theorem LO.Arith.concat_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) (z : V) :
                                                                      Equations
                                                                      • =
                                                                      instance LO.Arith.concat_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                                      { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.concat
                                                                      Equations
                                                                      • =
                                                                      @[simp]
                                                                      theorem LO.Arith.concat_nth_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (z : V) {i : V} (hi : i < LO.Arith.len v) :
                                                                      @[simp]
                                                                      theorem LO.Arith.concat_nth_len' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (z : V) {i : V} (hi : LO.Arith.len v = i) :

                                                                      Membership #

                                                                      def LO.Arith.MemVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) :
                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem LO.Arith.memVec_insert_fst {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {v : V} :
                                                                        @[simp]
                                                                        theorem LO.Arith.memVec_cons_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {v : V} :
                                                                        theorem LO.Arith.le_of_memVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {v : V} (h : LO.Arith.MemVec x v) :
                                                                        x v
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          Equations
                                                                          • =
                                                                          instance LO.Arith.memVec_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                                          { Γ := Γ, rank := m + 1 }-Relation LO.Arith.MemVec
                                                                          Equations
                                                                          • =

                                                                          Subset #

                                                                          def LO.Arith.SubsetVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (w : V) :
                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              Equations
                                                                              • =
                                                                              instance LO.Arith.subsetVec_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ) :
                                                                              { Γ := Γ, rank := m + 1 }-Relation LO.Arith.SubsetVec
                                                                              Equations
                                                                              • =

                                                                              Repeat #

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                Equations
                                                                                • LO.Arith.repeatVec.construction = { zero := fun (x : Fin 1V) => 0, succ := fun (x : Fin 1V) (x_1 ih : V) => cons (x 0) ih, zero_defined := , succ_defined := }
                                                                                Instances For
                                                                                  def LO.Arith.repeatVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) :
                                                                                  V

                                                                                  repeatVec x k = x ∷ x ∷ x ∷ ... k times ... ∷ 0

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem LO.Arith.repeatVec_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) :
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      Equations
                                                                                      • =
                                                                                      instance LO.Arith.repeatVec_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : } (Γ : LO.SigmaPiDelta) :
                                                                                      { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.repeatVec
                                                                                      Equations
                                                                                      • =
                                                                                      @[simp]
                                                                                      @[simp]
                                                                                      theorem LO.Arith.le_repaetVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) :
                                                                                      theorem LO.Arith.nth_repeatVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) {i : V} (h : i < k) :

                                                                                      Convert to Set #

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        Equations
                                                                                        • LO.Arith.VecToSet.construction = { nil := fun (x : Fin 0V) => , cons := fun (x : Fin 0V) (x x_1 ih : V) => insert x ih, nil_defined := , cons_defined := }
                                                                                        Instances For
                                                                                          def LO.Arith.vecToSet {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                                                          V
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            Equations
                                                                                            • =
                                                                                            instance LO.Arith.vecToSet_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : } (Γ : LO.SigmaPiDelta) :
                                                                                            { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.vecToSet
                                                                                            Equations
                                                                                            • =
                                                                                            @[simp]