Documentation

Arithmetization.ISigmaOne.HFS.Vec

Vec #

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

            N-th element of List #

            def LO.Arith.Nth.Phi {V : Type u_1} [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
                Instances For
                  Equations
                  Instances For
                    def LO.Arith.Nth.graphDef :
                    𝚺₁.Semisentence 1
                    Equations
                    Instances For
                      instance LO.Arith.Nth.graph_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
                      { Γ := 𝚺, rank := 0 + 1 }-Predicate Graph
                      @[simp]
                      theorem LO.Arith.Nth.zero_ne_add_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
                      0 x + 1

                      TODO: move

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

                            TODO: move

                            @[simp]
                            theorem LO.Arith.nth_zero_idx {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) :
                            nth 0 i = 0
                            theorem LO.Arith.nth_lt_of_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} (hv : 0 < v) (i : V) :
                            nth v i < v
                            @[simp]
                            theorem LO.Arith.nth_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v i : V) :
                            nth 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 : } (β : Blueprint arity) :
                                𝚺₁.Semisentence (arity + 1)
                                Equations
                                • β.graphDef = β.blueprint.fixpointDef
                                Instances For
                                  def LO.Arith.VecRec.Blueprint.resultDef {arity : } (β : 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) [ORingStruc V] {arity : } (β : Blueprint arity) :
                                    Type u_1
                                    Instances For
                                      def LO.Arith.VecRec.Construction.Phi {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : 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
                                        def LO.Arith.VecRec.Construction.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) :
                                        Fixpoint.Construction V β.blueprint
                                        Equations
                                        • c.construction = { Φ := c.Phi, defined := , monotone := }
                                        Instances For
                                          def LO.Arith.VecRec.Construction.Graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) :
                                            FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin (arity + 1)V) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)) β.graphDef
                                            instance LO.Arith.VecRec.Construction.graph_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) :
                                            𝚺₁.Boldface fun (v : Fin (arity + 1)V) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)
                                            instance LO.Arith.VecRec.Construction.graph_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) :
                                            𝚺₁-Predicate c.Graph param
                                            instance LO.Arith.VecRec.Construction.graph_definable'' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) :
                                            { Γ := 𝚺, rank := 0 + 1 }-Predicate c.Graph param
                                            theorem LO.Arith.VecRec.Construction.graph_case {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) {param : Fin arityV} {pr : V} :
                                            c.Graph param pr pr = 0, c.nil param ∃ (x : V) (xs : V) (ih : V), pr = Cons.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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) {param : Fin arityV} {x xs y : V} :
                                            c.Graph param Cons.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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) {param : Fin arityV} {xs y₁ 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) (xs : V) :
                                            ∃! y : V, c.Graph param xs, y
                                            def LO.Arith.VecRec.Construction.result {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) (xs : V) :
                                            V
                                            Equations
                                            Instances For
                                              theorem LO.Arith.VecRec.Construction.result_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) {xs 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) :
                                              c.result param 0 = c.nil param
                                              @[simp]
                                              theorem LO.Arith.VecRec.Construction.result_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) (x xs : V) :
                                              c.result param (Cons.cons x xs) = c.cons param x xs (c.result param xs)
                                              theorem LO.Arith.VecRec.Construction.result_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) :
                                              FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1)V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)) β.resultDef
                                              @[simp]
                                              theorem LO.Arith.VecRec.Construction.eval_resultDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (v : Fin (arity + 2)V) :
                                              V ⊧/v (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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) :
                                              𝚺₁.BoldfaceFunction fun (v : Fin (arity + 1)V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)
                                              instance LO.Arith.VecRec.Construction.result_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (Γ : SigmaPiDelta) (m : ) :
                                              { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin (arity + 1)V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)

                                              Length of List #

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                Instances For
                                                  def LO.Arith.len {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                  V
                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem LO.Arith.len_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
                                                    len 0 = 0
                                                    @[simp]
                                                    theorem LO.Arith.len_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                                                    len (cons x v) = len v + 1
                                                    instance LO.Arith.len_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                                                    { Γ := Γ, rank := m + 1 }-Function₁ len
                                                    @[simp]
                                                    theorem LO.Arith.len_zero_iff_eq_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} :
                                                    len v = 0 v = 0
                                                    theorem LO.Arith.nth_lt_len {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v i : V} (hl : len v i) :
                                                    nth v i = 0
                                                    @[simp]
                                                    theorem LO.Arith.len_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                    len v v
                                                    theorem LO.Arith.nth_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v₁ v₂ : V} (hl : len v₁ = len v₂) (H : i < len v₁, nth v₁ i = nth v₂ i) :
                                                    v₁ = v₂
                                                    theorem LO.Arith.nth_ext' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (l : V) {v₁ v₂ : V} (hl₁ : len v₁ = l) (hl₂ : len v₂ = l) (H : i < l, nth v₁ i = nth v₂ i) :
                                                    v₁ = v₂
                                                    theorem LO.Arith.le_of_nth_le_nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v₁ v₂ : V} (hl : len v₁ = len v₂) (H : i < len v₁, nth v₁ i nth v₂ i) :
                                                    v₁ v₂
                                                    theorem LO.Arith.nth_lt_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v i : V} (hi : i < len v) :
                                                    nth v i < v
                                                    theorem LO.Arith.sigmaOne_skolem_vec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : VVProp} (hP : 𝚺₁-Relation R) {l : V} (H : x < l, ∃ (y : V), R x y) :
                                                    ∃ (v : V), len v = l i < l, R i (nth v i)
                                                    theorem LO.Arith.eq_singleton_iff_len_eq_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} :
                                                    len v = 1 ∃ (x : V), v = ?[x]
                                                    theorem LO.Arith.eq_doubleton_of_len_eq_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} :
                                                    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
                                                      Instances For
                                                        def LO.Arith.listMax {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                        V
                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          @[simp]
                                                          theorem LO.Arith.listMax_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                                                          instance LO.Arith.listMax_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                                                          { Γ := Γ, rank := m + 1 }-Function₁ listMax
                                                          theorem LO.Arith.nth_le_listMax {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i v : V} (h : i < len v) :
                                                          theorem LO.Arith.listMaxss_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v z : V} (h : i < len v, nth v i z) :
                                                          theorem LO.Arith.listMaxss_le_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v z : V} :
                                                          listMax v z i < len v, 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v k : V) :
                                                              V
                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem LO.Arith.takeLast_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} :
                                                                takeLast 0 k = 0
                                                                theorem LO.Arith.takeLast_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} (x v : V) :
                                                                takeLast (cons x v) k = if len v < k then cons x v else takeLast v k
                                                                instance LO.Arith.takeLast_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                                                                { Γ := Γ, rank := m + 1 }-Function₂ takeLast
                                                                theorem LO.Arith.len_takeLast {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v k : V} (h : k len v) :
                                                                len (takeLast v k) = k
                                                                @[simp]
                                                                theorem LO.Arith.takeLast_len_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                                takeLast v (len v) = v
                                                                @[simp]
                                                                theorem LO.Arith.add_sub_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a b c : V) :
                                                                a + c - (b + c) = a - b

                                                                TODO: move

                                                                @[simp]
                                                                theorem LO.Arith.takeLast_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                                takeLast v 0 = 0
                                                                theorem LO.Arith.takeLast_succ_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i v : V} (h : i < len v) :
                                                                takeLast v (i + 1) = cons (nth v (len v - (i + 1))) (takeLast v i)

                                                                Concatation #

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

                                                                      Membership #

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

                                                                          Subset #

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

                                                                              Repeat #

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                Equations
                                                                                Instances For
                                                                                  def LO.Arith.repeatVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x k : V) :
                                                                                  V

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

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

                                                                                      Convert to Set #

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        Equations
                                                                                        Instances For
                                                                                          def LO.Arith.vecToSet {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                                                          V
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            theorem LO.Arith.vecToSet_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                                                                                            instance LO.Arith.vecToSet_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : } (Γ : SigmaPiDelta) :
                                                                                            { Γ := Γ, rank := m + 1 }-Function₁ vecToSet
                                                                                            theorem LO.Arith.mem_vecToSet_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v x : V} :
                                                                                            x vecToSet v i < len v, x = nth v i
                                                                                            @[simp]
                                                                                            theorem LO.Arith.nth_mem_vecToSet {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v i : V} (h : i < len v) :