Documentation

Foundation.FirstOrder.ISigma1.HFS.Vec

Vec #

noncomputable instance LO.ISigma1.instCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
Cons V V
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.ISigma1.cons_def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
      cons x v = x, v + 1
      @[simp]
      theorem LO.ISigma1.fstIdx_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
      fstIdx (cons x v) = x
      @[simp]
      theorem LO.ISigma1.sndIdx_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
      sndIdx (cons x v) = v
      theorem LO.ISigma1.succ_eq_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
      x + 1 = cons (π₁ x) (π₂ x)
      @[simp]
      theorem LO.ISigma1.lt_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
      x < cons x v
      @[simp]
      theorem LO.ISigma1.lt_cons' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
      v < cons x v
      @[simp]
      theorem LO.ISigma1.zero_lt_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
      0 < cons x v
      @[simp]
      theorem LO.ISigma1.cons_ne_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
      cons x v 0
      @[simp]
      theorem LO.ISigma1.zero_ne_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
      0 cons x v
      theorem LO.ISigma1.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.ISigma1.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.ISigma1.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
        @[simp]
        theorem LO.ISigma1.eval_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3V) :
        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
            @[simp]
            instance LO.ISigma1.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.ISigma1.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
                  @[simp]
                  theorem LO.ISigma1.Nth.zero_ne_add_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
                  0 x + 1

                  TODO: move

                  theorem LO.ISigma1.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.ISigma1.Nth.graph_exists {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v i : V) :
                  ∃ (x : V), Graph v, i, x
                  theorem LO.ISigma1.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₂
                  noncomputable def LO.ISigma1.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.ISigma1.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.ISigma1.nth_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                      nth v 0 = fstIdx v
                      theorem LO.ISigma1.nth_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v i : V) :
                      nth v (i + 1) = nth (sndIdx v) i
                      @[simp]
                      theorem LO.ISigma1.nth_cons_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                      nth (cons x v) 0 = x
                      @[simp]
                      theorem LO.ISigma1.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.ISigma1.nth_cons_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                      nth (cons x v) 1 = nth v 0
                      @[simp]
                      theorem LO.ISigma1.nth_cons_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                      nth (cons x v) 2 = nth v 1
                      theorem LO.ISigma1.cons_cases {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
                      x = 0 ∃ (y : V) (v : V), x = cons y v
                      theorem LO.ISigma1.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.ISigma1.cons_ISigma1.sigma1_succ_induction {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.ISigma1.cons_ISigma1.pi1_succ_induction {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
                        @[simp]
                        theorem LO.ISigma1.eval_nthDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3V) :
                        V ⊧/v FirstOrder.Arithmetic.nthDef v 0 = nth (v 1) (v 2)
                        instance LO.ISigma1.nth_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                        { Γ := Γ, rank := m + 1 }-Function₂ nth
                        theorem LO.ISigma1.cons_absolute {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a v : ) :
                        (cons a v) = cons a v

                        TODO: move

                        @[simp]
                        theorem LO.ISigma1.nth_zero_idx {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) :
                        nth 0 i = 0
                        theorem LO.ISigma1.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.ISigma1.nth_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v i : V) :
                        nth v i v

                        Inductivly Construction of Function on List #

                        structure LO.ISigma1.VecRec.Blueprint (arity : ) :
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                structure LO.ISigma1.VecRec.Construction (V : Type u_1) [ORingStruc V] {arity : } (β : Blueprint arity) :
                                Type u_1
                                Instances For
                                  def LO.ISigma1.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
                                  Instances For
                                    Equations
                                    Instances For
                                      def LO.ISigma1.VecRec.Construction.Graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) :
                                      VProp
                                      Equations
                                      Instances For
                                        theorem LO.ISigma1.VecRec.Construction.graph_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) :
                                        FirstOrder.Arithmetic.HierarchySymbol.Defined (fun (v : Fin (arity + 1)V) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)) β.graphDef
                                        instance LO.ISigma1.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.ISigma1.VecRec.Construction.graph_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (param : Fin arityV) :
                                        instance LO.ISigma1.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.ISigma1.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.ISigma1.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.ISigma1.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.ISigma1.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.ISigma1.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.ISigma1.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
                                        noncomputable def LO.ISigma1.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.ISigma1.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.ISigma1.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.ISigma1.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.ISigma1.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.ISigma1.VecRec.Construction.result_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) :
                                          FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1)V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)) β.resultDef
                                          @[simp]
                                          theorem LO.ISigma1.VecRec.Construction.eval_resultDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : } {β : Blueprint arity} (c : Construction V β) (v : Fin (arity + 2)V) :
                                          V ⊧/v β.resultDef v 0 = c.result (fun (x : Fin arity) => v x.succ.succ) (v 1)
                                          instance LO.ISigma1.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.ISigma1.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
                                              noncomputable def LO.ISigma1.len {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                              V
                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem LO.ISigma1.len_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
                                                len 0 = 0
                                                @[simp]
                                                theorem LO.ISigma1.len_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                                                len (cons x v) = len v + 1
                                                @[simp]
                                                theorem LO.ISigma1.eval_lenDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2V) :
                                                instance LO.ISigma1.len_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                                                { Γ := Γ, rank := m + 1 }-Function₁ len
                                                @[simp]
                                                theorem LO.ISigma1.len_zero_iff_eq_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} :
                                                len v = 0 v = 0
                                                theorem LO.ISigma1.nth_lt_len {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v i : V} (hl : len v i) :
                                                nth v i = 0
                                                @[simp]
                                                theorem LO.ISigma1.len_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                len v v
                                                theorem LO.ISigma1.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.ISigma1.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.ISigma1.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.ISigma1.nth_lt_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v i : V} (hi : i < len v) :
                                                nth v i < v
                                                theorem LO.ISigma1.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.ISigma1.eq_singleton_iff_len_eq_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} :
                                                len v = 1 ∃ (x : V), v = ?[x]
                                                theorem LO.ISigma1.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
                                                    noncomputable def LO.ISigma1.listMax {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                    V
                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem LO.ISigma1.listMax_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                                                      listMax (cons x v) = max x (listMax v)
                                                      instance LO.ISigma1.listMax_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                                                      { Γ := Γ, rank := m + 1 }-Function₁ listMax
                                                      theorem LO.ISigma1.nth_le_listMax {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i v : V} (h : i < len v) :
                                                      theorem LO.ISigma1.listMaxss_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v z : V} (h : i < len v, nth v i z) :
                                                      theorem LO.ISigma1.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
                                                          noncomputable def LO.ISigma1.takeLast {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v k : V) :
                                                          V
                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem LO.ISigma1.takeLast_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} :
                                                            takeLast 0 k = 0
                                                            theorem LO.ISigma1.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
                                                            @[simp]
                                                            instance LO.ISigma1.takeLast_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                                                            { Γ := Γ, rank := m + 1 }-Function₂ takeLast
                                                            theorem LO.ISigma1.len_takeLast {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v k : V} (h : k len v) :
                                                            len (takeLast v k) = k
                                                            @[simp]
                                                            theorem LO.ISigma1.takeLast_len_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                            takeLast v (len v) = v
                                                            @[simp]
                                                            theorem LO.ISigma1.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.ISigma1.takeLast_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                            takeLast v 0 = 0
                                                            theorem LO.ISigma1.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
                                                                noncomputable def LO.ISigma1.concat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v z : V) :
                                                                V
                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem LO.ISigma1.concat_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (z : V) :
                                                                  concat 0 z = ?[z]
                                                                  @[simp]
                                                                  theorem LO.ISigma1.concat_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v z : V) :
                                                                  concat (cons x v) z = cons x (concat v z)
                                                                  @[simp]
                                                                  theorem LO.ISigma1.eval_concatDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3V) :
                                                                  instance LO.ISigma1.concat_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                                                                  { Γ := Γ, rank := m + 1 }-Function₂ concat
                                                                  @[simp]
                                                                  theorem LO.ISigma1.len_concat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v z : V) :
                                                                  len (concat v z) = len v + 1
                                                                  theorem LO.ISigma1.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.ISigma1.concat_nth_len {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v z : V) :
                                                                  nth (concat v z) (len v) = z
                                                                  theorem LO.ISigma1.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.ISigma1.MemVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem LO.ISigma1.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.ISigma1.memVec_insert_fst {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x v : V} :
                                                                    MemVec x (cons x v)
                                                                    @[simp]
                                                                    theorem LO.ISigma1.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.ISigma1.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
                                                                      @[simp]
                                                                      instance LO.ISigma1.memVec_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ) :
                                                                      { Γ := Γ, rank := m + 1 }-Relation MemVec

                                                                      Subset #

                                                                      def LO.ISigma1.SubsetVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v w : V) :
                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem LO.ISigma1.SubsetVec.refl {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                                        @[simp]
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          instance LO.ISigma1.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
                                                                              noncomputable def LO.ISigma1.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.ISigma1.repeatVec_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
                                                                                repeatVec x 0 = 0
                                                                                @[simp]
                                                                                theorem LO.ISigma1.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
                                                                                  @[simp]
                                                                                  instance LO.ISigma1.repeatVec_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : } (Γ : SigmaPiDelta) :
                                                                                  { Γ := Γ, rank := m + 1 }-Function₂ repeatVec
                                                                                  @[simp]
                                                                                  theorem LO.ISigma1.len_repeatVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x k : V) :
                                                                                  len (repeatVec x k) = k
                                                                                  @[simp]
                                                                                  theorem LO.ISigma1.le_repaetVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x k : V) :
                                                                                  theorem LO.ISigma1.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.ISigma1.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
                                                                                      noncomputable def LO.ISigma1.vecToSet {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) :
                                                                                      V
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem LO.ISigma1.vecToSet_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) :
                                                                                        instance LO.ISigma1.vecToSet_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : } (Γ : SigmaPiDelta) :
                                                                                        { Γ := Γ, rank := m + 1 }-Function₁ vecToSet
                                                                                        theorem LO.ISigma1.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.ISigma1.nth_mem_vecToSet {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v i : V} (h : i < len v) :