Vec

noncomputable instance LO.ISigma1.instCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Cons V V

Equations

• LO.ISigma1.instCons = { cons := fun (x1 x2 : V) => ⟪x1, x2⟫ + 1 }

def LO.ISigma1.«term_∷_» : Lean.TrailingParserDescr

Equations

• LO.ISigma1.«term_∷_» = Lean.ParserDescr.trailingNode `LO.ISigma1.«term_∷_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∷ ") (Lean.ParserDescr.cat `term 67))

def LO.ISigma1.«term?[_]» : Lean.ParserDescr

Equations

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

def LO.ISigma1.consUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

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₂

def LO.FirstOrder.Arith.consDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.ISigma1.cons_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ cons via FirstOrder.Arith.consDef

@[simp]

theorem LO.ISigma1.eval_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.consDef) ↔ v 0 = cons (v 1) (v 2)

instance LO.ISigma1.cons_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ cons

instance LO.ISigma1.cons_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ cons

def LO.FirstOrder.Arith.mkVec₁Def : 𝚺₀.Semisentence 2

Equations

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

theorem LO.ISigma1.mkVec₁_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ fun (x : V) => ?[x] via FirstOrder.Arith.mkVec₁Def

@[simp]

theorem LO.ISigma1.eval_mkVec₁Def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.mkVec₁Def) ↔ v 0 = ?[v 1]

instance LO.ISigma1.mkVec₁_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ fun (x : V) => ?[x]

instance LO.ISigma1.mkVec₁_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : FirstOrder.Arith.HierarchySymbol) : ℌ-Function₁ fun (x : V) => ?[x]

def LO.FirstOrder.Arith.mkVec₂Def : 𝚺₁.Semisentence 3

Equations

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

theorem LO.ISigma1.mkVec₂_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ fun (x y : V) => ?[x, y] via FirstOrder.Arith.mkVec₂Def

@[simp]

theorem LO.ISigma1.eval_mkVec₂Def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.mkVec₂Def) ↔ v 0 = ?[v 1, v 2]

instance LO.ISigma1.mkVec₂_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ fun (x y : V) => ?[x, y]

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

Equations

• LO.ISigma1.Nth.Phi C pr = ((∃ (v : V), pr = ⟪v, ⟪0, LO.ISigma1.fstIdx v⟫⟫) ∨ ∃ (v : V) (i : V) (x : V), pr = ⟪v, ⟪i + 1, x⟫⟫ ∧ ⟪LO.ISigma1.sndIdx v, ⟪i, x⟫⟫ ∈ C)

def LO.ISigma1.Nth.blueprint : Fixpoint.Blueprint 0

Equations

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

def LO.ISigma1.Nth.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Fixpoint.Construction V blueprint

Equations

• LO.ISigma1.Nth.construction = { Φ := fun (x : Fin 0 → V) => LO.ISigma1.Nth.Phi, defined := ⋯, monotone := ⋯ }

Instances For

• LO.ISigma1.Nth.instFiniteConstruction

instance LO.ISigma1.Nth.instFiniteConstruction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Fixpoint.Construction.Finite V construction

def LO.ISigma1.Nth.Graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : V → Prop

Equations

• LO.ISigma1.Nth.Graph = LO.ISigma1.Nth.construction.Fixpoint ![]

Instances For

• LO.ISigma1.Nth.graph_definable
• LO.ISigma1.Nth.graph_definable'

def LO.ISigma1.Nth.graphDef : 𝚺₁.Semisentence 1

Equations

• LO.ISigma1.Nth.graphDef = LO.ISigma1.Nth.blueprint.fixpointDef

theorem LO.ISigma1.Nth.graph_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Predicate Graph via graphDef

instance LO.ISigma1.Nth.graph_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Predicate Graph

instance LO.ISigma1.Nth.graph_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : { Γ := 𝚺, rank := 0 + 1 }-Predicate Graph

@[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_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v x : V} : Graph ⟪v, ⟪0, x⟫⟫ ↔ x = fstIdx v

theorem LO.ISigma1.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.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₂

theorem LO.ISigma1.Nth.graph_existsUnique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v i : V) : ∃! x : V, Graph ⟪v, ⟪i, x⟫⟫

noncomputable def LO.ISigma1.nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v i : V) : V

Equations

• LO.ISigma1.nth v i = Classical.choose! ⋯

Instances For

• LO.ISigma1.nth_definable
• LO.ISigma1.nth_definable'

def LO.ISigma1.«term_.[_]» : Lean.TrailingParserDescr

Equations

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

theorem LO.ISigma1.nth_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v i : V) : Nth.Graph ⟪v, ⟪i, nth v i⟫⟫

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 : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P v → P (cons x v)) (v : V) : P v

theorem LO.ISigma1.cons_ISigma1.sigma1_succ_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : V → Prop} (hP : 𝚺₁-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P v → P (cons x v)) (v : V) : P v

theorem LO.ISigma1.cons_ISigma1.pi1_succ_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : V → Prop} (hP : 𝚷₁-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P v → P (cons x v)) (v : V) : P v

def LO.FirstOrder.Arith.nthDef : 𝚺₁.Semisentence 3

Equations

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

theorem LO.ISigma1.nth_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ nth via FirstOrder.Arith.nthDef

@[simp]

theorem LO.ISigma1.eval_nthDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.nthDef) ↔ v 0 = nth (v 1) (v 2)

instance LO.ISigma1.nth_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ nth

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

theorem LO.ISigma1.pi₁_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : π₁ 0 = 0

TODO: move

theorem LO.ISigma1.pi₂_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : π₂ 0 = 0

@[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 : ℕ) : Type

• nil : 𝚺₁.Semisentence (arity + 1)
• cons : 𝚺₁.Semisentence (arity + 4)

def LO.ISigma1.VecRec.Blueprint.blueprint {arity : ℕ} (β : Blueprint arity) : Fixpoint.Blueprint arity

Equations

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

def LO.ISigma1.VecRec.Blueprint.graphDef {arity : ℕ} (β : Blueprint arity) : 𝚺₁.Semisentence (arity + 1)

Equations

• β.graphDef = β.blueprint.fixpointDef

def LO.ISigma1.VecRec.Blueprint.resultDef {arity : ℕ} (β : Blueprint arity) : 𝚺₁.Semisentence (arity + 2)

Equations

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

structure LO.ISigma1.VecRec.Construction (V : Type u_1) [ORingStruc V] {arity : ℕ} (β : Blueprint arity) : Type u_1

• nil (param : Fin arity → V) : V
• cons (param : Fin arity → V) (x xs ih : V) : V
• nil_defined : FirstOrder.Arith.HierarchySymbol.DefinedFunction self.nil β.nil
• cons_defined : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1 + 1 + 1) → V) => self.cons (fun (x : Fin arity) => v x.succ.succ.succ) (v 0) (v 1) (v 2)) β.cons

def LO.ISigma1.VecRec.Construction.Phi {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (C : Set V) (pr : V) : Prop

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)

def LO.ISigma1.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

• LO.ISigma1.VecRec.Construction.instFiniteConstruction

instance LO.ISigma1.VecRec.Construction.instFiniteConstruction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : Fixpoint.Construction.Finite V c.construction

def LO.ISigma1.VecRec.Construction.Graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) : V → Prop

Equations

• c.Graph param = c.construction.Fixpoint param

Instances For

• LO.ISigma1.VecRec.Construction.graph_definable'
• LO.ISigma1.VecRec.Construction.graph_definable''

theorem LO.ISigma1.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.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 arity → V) : 𝚺₁-Predicate c.Graph param

instance LO.ISigma1.VecRec.Construction.graph_definable'' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) : { Γ := 𝚺, 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 arity → V} {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 arity → V} {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 arity → V} {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 arity → V) (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 arity → V} {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 arity → V) (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 arity → V) (xs : V) : V

Equations

• c.result param xs = Classical.choose! ⋯

theorem LO.ISigma1.VecRec.Construction.result_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (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 arity → V) {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 arity → V) : 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 arity → V) (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.Arith.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 (FirstOrder.Arith.HierarchySymbol.Semiformula.val β.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

def LO.ISigma1.Len.blueprint : VecRec.Blueprint 0

Equations

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

def LO.ISigma1.Len.construction {V : Type u_1} [ORingStruc V] : VecRec.Construction V blueprint

Equations

• LO.ISigma1.Len.construction = { nil := fun (x : Fin 0 → V) => 0, cons := fun (x : Fin 0 → V) (x x ih : V) => ih + 1, nil_defined := ⋯, cons_defined := ⋯ }

noncomputable def LO.ISigma1.len {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) : V

Equations

• LO.ISigma1.len v = LO.ISigma1.Len.construction.result ![] v

Instances For

• LO.ISigma1.len_definable
• LO.ISigma1.len_definable'

@[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

def LO.FirstOrder.Arith.lenDef : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arith.lenDef = LO.ISigma1.Len.blueprint.resultDef

theorem LO.ISigma1.len_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ len via FirstOrder.Arith.lenDef

@[simp]

theorem LO.ISigma1.eval_lenDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.lenDef) ↔ v 0 = len (v 1)

instance LO.ISigma1.len_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ len

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 : V → V → Prop} (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

def LO.ISigma1.ListMax.blueprint : VecRec.Blueprint 0

Equations

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

noncomputable def LO.ISigma1.ListMax.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : VecRec.Construction V blueprint

Equations

• LO.ISigma1.ListMax.construction = { nil := fun (x : Fin 0 → V) => 0, cons := fun (x : Fin 0 → V) (x x_1 ih : V) => max x ih, nil_defined := ⋯, cons_defined := ⋯ }

noncomputable def LO.ISigma1.listMax {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) : V

Equations

• LO.ISigma1.listMax v = LO.ISigma1.ListMax.construction.result ![] v

Instances For

• LO.ISigma1.listMax_definable
• LO.ISigma1.listMax_definable'

@[simp]

theorem LO.ISigma1.listMax_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : listMax 0 = 0

@[simp]

theorem LO.ISigma1.listMax_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) : listMax (cons x v) = max x (listMax v)

def LO.FirstOrder.Arith.listMaxDef : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arith.listMaxDef = LO.ISigma1.ListMax.blueprint.resultDef

theorem LO.ISigma1.listMax_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ listMax via FirstOrder.Arith.listMaxDef

@[simp]

theorem LO.ISigma1.eval_listMaxDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.listMaxDef) ↔ v 0 = listMax (v 1)

instance LO.ISigma1.listMax_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ listMax

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) : nth v i ≤ listMax v

theorem LO.ISigma1.listMaxss_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v z : V} (h : ∀ i < len v, nth v i ≤ z) : listMax v ≤ 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

def LO.ISigma1.TakeLast.blueprint : VecRec.Blueprint 1

Equations

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

noncomputable def LO.ISigma1.TakeLast.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : VecRec.Construction V blueprint

Equations

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

noncomputable def LO.ISigma1.takeLast {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v k : V) : V

Equations

• LO.ISigma1.takeLast v k = LO.ISigma1.TakeLast.construction.result ![k] v

Instances For

• LO.ISigma1.takeLast_definable
• LO.ISigma1.takeLast_definable'

@[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

def LO.FirstOrder.Arith.takeLastDef : 𝚺₁.Semisentence 3

Equations

• LO.FirstOrder.Arith.takeLastDef = LO.ISigma1.TakeLast.blueprint.resultDef

theorem LO.ISigma1.takeLast_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ takeLast via FirstOrder.Arith.takeLastDef

@[simp]

theorem LO.ISigma1.eval_takeLastDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.takeLastDef) ↔ v 0 = takeLast (v 1) (v 2)

instance LO.ISigma1.takeLast_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ takeLast

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

def LO.ISigma1.Concat.blueprint : VecRec.Blueprint 1

Equations

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

noncomputable def LO.ISigma1.Concat.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : VecRec.Construction V blueprint

Equations

• LO.ISigma1.Concat.construction = { nil := fun (param : Fin 1 → V) => ?[param 0], cons := fun (x : Fin 1 → V) (x x_1 ih : V) => cons x ih, nil_defined := ⋯, cons_defined := ⋯ }

noncomputable def LO.ISigma1.concat {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v z : V) : V

Equations

• LO.ISigma1.concat v z = LO.ISigma1.Concat.construction.result ![z] v

Instances For

• LO.ISigma1.concat_definable
• LO.ISigma1.concat_definable'

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

def LO.FirstOrder.Arith.concatDef : 𝚺₁.Semisentence 3

Equations

• LO.FirstOrder.Arith.concatDef = LO.ISigma1.Concat.blueprint.resultDef

theorem LO.ISigma1.concat_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ concat via FirstOrder.Arith.concatDef

@[simp]

theorem LO.ISigma1.eval_concatDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.concatDef) ↔ v 0 = concat (v 1) (v 2)

instance LO.ISigma1.concat_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ concat

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

Equations

• LO.ISigma1.MemVec x v = ∃ i < LO.ISigma1.len v, x = LO.ISigma1.nth v i

Instances For

• LO.ISigma1.memVec_definable
• LO.ISigma1.memVec_definable'

def LO.ISigma1.«term_∈ᵥ_» : Lean.TrailingParserDescr

Equations

• LO.ISigma1.«term_∈ᵥ_» = Lean.ParserDescr.trailingNode `LO.ISigma1.«term_∈ᵥ_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ᵥ ") (Lean.ParserDescr.cat `term 41))

@[simp]

theorem LO.ISigma1.not_memVec_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : ¬MemVec x 0

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

def LO.FirstOrder.Arith.memVecDef : 𝚫₁.Semisentence 2

Equations

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

theorem LO.ISigma1.memVec_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚫₁-Relation MemVec via FirstOrder.Arith.memVecDef

@[simp]

theorem LO.ISigma1.eval_memVecDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.memVecDef) ↔ MemVec (v 0) (v 1)

instance LO.ISigma1.memVec_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚫₁-Relation MemVec

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

Equations

• LO.ISigma1.SubsetVec v w = ∀ (x : V), LO.ISigma1.MemVec x v → LO.ISigma1.MemVec x w

Instances For

• LO.ISigma1.subsetVec_definable
• LO.ISigma1.subsetVec_definable'

def LO.ISigma1.«term_⊆ᵥ_» : Lean.TrailingParserDescr

Equations

• LO.ISigma1.«term_⊆ᵥ_» = Lean.ParserDescr.trailingNode `LO.ISigma1.«term_⊆ᵥ_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ᵥ ") (Lean.ParserDescr.cat `term 31))

@[simp]

theorem LO.ISigma1.SubsetVec.refl {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) : SubsetVec v v

@[simp]

theorem LO.ISigma1.subsetVec_insert_tail {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) : SubsetVec v (cons x v)

def LO.FirstOrder.Arith.subsetVecDef : 𝚫₁.Semisentence 2

Equations

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

theorem LO.ISigma1.subsetVec_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚫₁-Relation SubsetVec via FirstOrder.Arith.subsetVecDef

@[simp]

theorem LO.ISigma1.eval_subsetVecDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.subsetVecDef) ↔ SubsetVec (v 0) (v 1)

instance LO.ISigma1.subsetVec_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚫₁-Relation SubsetVec

instance LO.ISigma1.subsetVec_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Relation SubsetVec

Repeat

def LO.ISigma1.repeatVec.blueprint : PR.Blueprint 1

Equations

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

noncomputable def LO.ISigma1.repeatVec.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : PR.Construction V blueprint

Equations

• LO.ISigma1.repeatVec.construction = { zero := fun (x : Fin 1 → V) => 0, succ := fun (x : Fin 1 → V) (x_1 ih : V) => cons (x 0) ih, zero_defined := ⋯, succ_defined := ⋯ }

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

• LO.ISigma1.repeatVec x k = LO.ISigma1.repeatVec.construction.result ![x] k

Instances For

• LO.ISigma1.repeatVec_definable
• LO.ISigma1.repeatVec_definable'

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

def LO.FirstOrder.Arith.repeatVecDef : 𝚺₁.Semisentence 3

Equations

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

theorem LO.ISigma1.repeatVec_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ repeatVec via FirstOrder.Arith.repeatVecDef

@[simp]

theorem LO.ISigma1.eval_repeatVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.repeatVecDef) ↔ v 0 = repeatVec (v 1) (v 2)

instance LO.ISigma1.repeatVec_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ repeatVec

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) : k ≤ repeatVec x k

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

def LO.ISigma1.VecToSet.blueprint : VecRec.Blueprint 0

Equations

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

noncomputable def LO.ISigma1.VecToSet.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : VecRec.Construction V blueprint

Equations

• LO.ISigma1.VecToSet.construction = { nil := fun (x : Fin 0 → V) => ∅, cons := fun (x : Fin 0 → V) (x x_1 ih : V) => insert x ih, nil_defined := ⋯, cons_defined := ⋯ }

noncomputable def LO.ISigma1.vecToSet {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) : V

Equations

• LO.ISigma1.vecToSet v = LO.ISigma1.VecToSet.construction.result ![] v

Instances For

• LO.ISigma1.vecToSet_definable
• LO.ISigma1.vecToSet_definable'

@[simp]

theorem LO.ISigma1.vecToSet_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : vecToSet 0 = ∅

@[simp]

theorem LO.ISigma1.vecToSet_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x v : V) : vecToSet (cons x v) = insert x (vecToSet v)

def LO.FirstOrder.Arith.vecToSetDef : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arith.vecToSetDef = LO.ISigma1.VecToSet.blueprint.resultDef

theorem LO.ISigma1.vecToSet_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ vecToSet via FirstOrder.Arith.vecToSetDef

@[simp]

theorem LO.ISigma1.eval_vecToSetDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.vecToSetDef) ↔ v 0 = vecToSet (v 1)

instance LO.ISigma1.vecToSet_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ vecToSet

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) : nth v i ∈ vecToSet v