Vec

instance LO.Arith.instCons_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Cons V V

Equations

• LO.Arith.instCons_arithmetization = { cons := fun (x x_1 : V) => ⟪x, x_1⟫ + 1 }

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

Equations

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

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

Equations

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

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

Equations

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

theorem LO.Arith.cons_def {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : cons x v = ⟪x, v⟫ + 1

@[simp]

theorem LO.Arith.fstIdx_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : LO.Arith.fstIdx (cons x v) = x

@[simp]

theorem LO.Arith.sndIdx_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : LO.Arith.sndIdx (cons x v) = v

theorem LO.Arith.succ_eq_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : x + 1 = cons (π₁ x) (π₂ x)

@[simp]

theorem LO.Arith.lt_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : x < cons x v

@[simp]

theorem LO.Arith.lt_cons' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : v < cons x v

@[simp]

theorem LO.Arith.zero_lt_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : 0 < cons x v

@[simp]

theorem LO.Arith.cons_ne_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : cons x v ≠ 0

@[simp]

theorem LO.Arith.zero_ne_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : 0 ≠ cons x v

theorem LO.Arith.nil_or_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (z : V) : z = 0 ∨ ∃ (x : V) (v : V), z = cons x v

@[simp]

theorem LO.Arith.cons_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x₁ : V) (x₂ : V) (v₁ : V) (v₂ : V) : cons x₁ v₁ = cons x₂ v₂ ↔ x₁ = x₂ ∧ v₁ = v₂

theorem LO.Arith.cons_le_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x₁ : V} {x₂ : V} {v₁ : V} {v₂ : V} (hx : x₁ ≤ x₂) (hv : v₁ ≤ v₂) : cons x₁ v₁ ≤ cons x₂ v₂

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.mkVec₂_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ fun (x y : V) => ?[x, y]

Equations

• ⋯ = ⋯

N-th element of List

def LO.Arith.Nth.Phi {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (C : Set V) (pr : V) : Prop

Equations

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

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

Equations

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

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

Equations

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

Instances For

• LO.Arith.Nth.instFiniteConstruction

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

Equations

• LO.Arith.Nth.instFiniteConstruction = { finite := ⋯ }

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

Equations

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

Instances For

• LO.Arith.Nth.graph_definable
• LO.Arith.Nth.graph_definable'

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

Equations

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Nth.zero_ne_add_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : 0 ≠ x + 1

TODO: move

theorem LO.Arith.Nth.graph_case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {pr : V} : LO.Arith.Nth.Graph pr ↔ (∃ (v : V), pr = ⟪v, ⟪0, LO.Arith.fstIdx v⟫⟫) ∨ ∃ (v : V) (i : V) (x : V), pr = ⟪v, ⟪i + 1, x⟫⟫ ∧ LO.Arith.Nth.Graph ⟪LO.Arith.sndIdx v, ⟪i, x⟫⟫

theorem LO.Arith.Nth.graph_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {x : V} : LO.Arith.Nth.Graph ⟪v, ⟪0, x⟫⟫ ↔ x = LO.Arith.fstIdx v

theorem LO.Arith.Nth.graph_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} {x : V} : LO.Arith.Nth.Graph ⟪v, ⟪i + 1, x⟫⟫ ↔ LO.Arith.Nth.Graph ⟪LO.Arith.sndIdx v, ⟪i, x⟫⟫

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

theorem LO.Arith.Nth.graph_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} {x₁ : V} {x₂ : V} : LO.Arith.Nth.Graph ⟪v, ⟪i, x₁⟫⟫ → LO.Arith.Nth.Graph ⟪v, ⟪i, x₂⟫⟫ → x₁ = x₂

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

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

Equations

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

Instances For

• LO.Arith.nth_definable
• LO.Arith.nth_definable'

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

Equations

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

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

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

theorem LO.Arith.nth_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) : LO.Arith.nth v 0 = LO.Arith.fstIdx v

theorem LO.Arith.nth_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (i : V) : LO.Arith.nth v (i + 1) = LO.Arith.nth (LO.Arith.sndIdx v) i

@[simp]

theorem LO.Arith.nth_cons_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : LO.Arith.nth (cons x v) 0 = x

@[simp]

theorem LO.Arith.nth_cons_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) (i : V) : LO.Arith.nth (cons x v) (i + 1) = LO.Arith.nth v i

@[simp]

theorem LO.Arith.nth_cons_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : LO.Arith.nth (cons x v) 1 = LO.Arith.nth v 0

@[simp]

theorem LO.Arith.nth_cons_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : LO.Arith.nth (cons x v) 2 = LO.Arith.nth v 1

theorem LO.Arith.cons_cases {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : x = 0 ∨ ∃ (y : V) (v : V), x = cons y v

theorem LO.Arith.cons_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P v → P (Cons.cons x v)) (v : V) : P v

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

theorem LO.Arith.cons_induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {P : V → Prop} (hP : 𝚷₁-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P v → P (Cons.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.Arith.nth_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ LO.Arith.nth via LO.FirstOrder.Arith.nthDef

@[simp]

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.nth_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.nth

Equations

• ⋯ = ⋯

theorem LO.Arith.cons_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : ℕ) (v : ℕ) : ↑(cons a v) = cons ↑a ↑v

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

TODO: move

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

@[simp]

theorem LO.Arith.nth_zero_idx {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) : LO.Arith.nth 0 i = 0

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

@[simp]

theorem LO.Arith.nth_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (i : V) : LO.Arith.nth v i ≤ v

Inductivly Construction of Function on List

structure LO.Arith.VecRec.Blueprint (arity : ℕ) : Type

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

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

Equations

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

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

Equations

• β.graphDef = β.blueprint.fixpointDef

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

Equations

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

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

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

theorem LO.Arith.VecRec.Construction.nil_defined {V : Type u_1} [LO.ORingStruc V] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (self : LO.Arith.VecRec.Construction V β) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction self.nil β.nil

theorem LO.Arith.VecRec.Construction.cons_defined {V : Type u_1} [LO.ORingStruc V] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (self : LO.Arith.VecRec.Construction V β) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin arity.succ.succ.succ → V) => self.cons (fun (x : Fin arity) => v x.succ.succ.succ) (v 0) (v 1) (v 2)) β.cons

def LO.Arith.VecRec.Construction.Phi {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin 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.Arith.VecRec.Construction.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) : LO.Arith.Fixpoint.Construction V β.blueprint

Equations

• c.construction = { Φ := c.Phi, defined := ⋯, monotone := ⋯ }

Instances For

• LO.Arith.VecRec.Construction.instFiniteConstruction

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

Equations

• c.instFiniteConstruction = { finite := ⋯ }

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

Equations

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

Instances For

• LO.Arith.VecRec.Construction.graph_definable'
• LO.Arith.VecRec.Construction.graph_definable''

theorem LO.Arith.VecRec.Construction.graph_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin arity.succ → V) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)) β.graphDef

instance LO.Arith.VecRec.Construction.graph_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) : 𝚺₁.Boldface fun (v : Fin arity.succ → V) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)

Equations

• ⋯ = ⋯

instance LO.Arith.VecRec.Construction.graph_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arity → V) : 𝚺₁-Predicate c.Graph param

Equations

• ⋯ = ⋯

instance LO.Arith.VecRec.Construction.graph_definable'' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arity → V) : { Γ := 𝚺, rank := 0 + 1 }-Predicate c.Graph param

Equations

• ⋯ = ⋯

theorem LO.Arith.VecRec.Construction.graph_case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) {param : Fin arity → V} {pr : V} : c.Graph param pr ↔ pr = ⟪0, c.nil param⟫ ∨ ∃ (x : V) (xs : V) (ih : V), pr = ⟪cons x xs, c.cons param x xs ih⟫ ∧ c.Graph param ⟪xs, ih⟫

theorem LO.Arith.VecRec.Construction.graph_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) {param : Fin arity → V} {l : V} : c.Graph param ⟪0, l⟫ ↔ l = c.nil param

theorem LO.Arith.VecRec.Construction.graph_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) {param : Fin arity → V} {x : V} {xs : V} {y : V} : c.Graph param ⟪cons x xs, y⟫ ↔ ∃ (y' : V), y = c.cons param x xs y' ∧ c.Graph param ⟪xs, y'⟫

theorem LO.Arith.VecRec.Construction.graph_exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arity → V) (xs : V) : ∃ (y : V), c.Graph param ⟪xs, y⟫

theorem LO.Arith.VecRec.Construction.graph_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) {param : Fin arity → V} {xs : V} {y₁ : V} {y₂ : V} : c.Graph param ⟪xs, y₁⟫ → c.Graph param ⟪xs, y₂⟫ → y₁ = y₂

theorem LO.Arith.VecRec.Construction.graph_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arity → V) (xs : V) : ∃! y : V, c.Graph param ⟪xs, y⟫

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

Equations

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

theorem LO.Arith.VecRec.Construction.result_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arity → V) (xs : V) : c.Graph param ⟪xs, c.result param xs⟫

theorem LO.Arith.VecRec.Construction.result_eq_of_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arity → V) {xs : V} {y : V} (h : c.Graph param ⟪xs, y⟫) : c.result param xs = y

@[simp]

theorem LO.Arith.VecRec.Construction.result_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arity → V) : c.result param 0 = c.nil param

@[simp]

theorem LO.Arith.VecRec.Construction.result_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (param : Fin arity → V) (x : V) (xs : V) : c.result param (cons x xs) = c.cons param x xs (c.result param xs)

theorem LO.Arith.VecRec.Construction.result_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin arity.succ → 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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (v : Fin (arity + 2) → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val β.resultDef) ↔ v 0 = c.result (fun (x : Fin arity) => v x.succ.succ) (v 1)

instance LO.Arith.VecRec.Construction.result_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) : 𝚺₁.BoldfaceFunction fun (v : Fin arity.succ → V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)

Equations

• ⋯ = ⋯

instance LO.Arith.VecRec.Construction.result_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {arity : ℕ} {β : LO.Arith.VecRec.Blueprint arity} (c : LO.Arith.VecRec.Construction V β) (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin arity.succ → V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)

Equations

• ⋯ = ⋯

Length of List

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

Equations

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

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

Equations

• LO.Arith.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 := ⋯ }

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

Equations

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

Instances For

• LO.Arith.len_definable
• LO.Arith.len_definable'

@[simp]

theorem LO.Arith.len_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.len 0 = 0

@[simp]

theorem LO.Arith.len_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : LO.Arith.len (cons x v) = LO.Arith.len v + 1

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.len_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.len

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.len_zero_iff_eq_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} : LO.Arith.len v = 0 ↔ v = 0

theorem LO.Arith.nth_lt_len {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} (hl : LO.Arith.len v ≤ i) : LO.Arith.nth v i = 0

@[simp]

theorem LO.Arith.len_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) : LO.Arith.len v ≤ v

theorem LO.Arith.nth_ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v₁ : V} {v₂ : V} (hl : LO.Arith.len v₁ = LO.Arith.len v₂) (H : ∀ i < LO.Arith.len v₁, LO.Arith.nth v₁ i = LO.Arith.nth v₂ i) : v₁ = v₂

theorem LO.Arith.nth_ext' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (l : V) {v₁ : V} {v₂ : V} (hl₁ : LO.Arith.len v₁ = l) (hl₂ : LO.Arith.len v₂ = l) (H : ∀ i < l, LO.Arith.nth v₁ i = LO.Arith.nth v₂ i) : v₁ = v₂

theorem LO.Arith.le_of_nth_le_nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v₁ : V} {v₂ : V} (hl : LO.Arith.len v₁ = LO.Arith.len v₂) (H : ∀ i < LO.Arith.len v₁, LO.Arith.nth v₁ i ≤ LO.Arith.nth v₂ i) : v₁ ≤ v₂

theorem LO.Arith.nth_lt_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} (hi : i < LO.Arith.len v) : LO.Arith.nth v i < v

theorem LO.Arith.sigmaOne_skolem_vec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : V → V → Prop} (hP : 𝚺₁-Relation R) {l : V} (H : ∀ x < l, ∃ (y : V), R x y) : ∃ (v : V), LO.Arith.len v = l ∧ ∀ i < l, R i (LO.Arith.nth v i)

theorem LO.Arith.eq_singleton_iff_len_eq_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} : LO.Arith.len v = 1 ↔ ∃ (x : V), v = ?[x]

theorem LO.Arith.eq_doubleton_of_len_eq_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} : LO.Arith.len v = 2 ↔ ∃ (x : V) (y : V), v = ?[x, y]

Maximum of List

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

Equations

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

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

Equations

• LO.Arith.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 := ⋯ }

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

Equations

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

Instances For

• LO.Arith.listMax_definable
• LO.Arith.listMax_definable'

@[simp]

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

@[simp]

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

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.listMax_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.listMax

Equations

• ⋯ = ⋯

theorem LO.Arith.nth_le_listMax {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {v : V} (h : i < LO.Arith.len v) : LO.Arith.nth v i ≤ LO.Arith.listMax v

theorem LO.Arith.listMaxss_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {z : V} (h : ∀ i < LO.Arith.len v, LO.Arith.nth v i ≤ z) : LO.Arith.listMax v ≤ z

theorem LO.Arith.listMaxss_le_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {z : V} : LO.Arith.listMax v ≤ z ↔ ∀ i < LO.Arith.len v, LO.Arith.nth v i ≤ z

Take Last k-Element

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

Equations

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

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

Equations

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

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

Equations

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

Instances For

• LO.Arith.takeLast_definable
• LO.Arith.takeLast_definable'

@[simp]

theorem LO.Arith.takeLast_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} : LO.Arith.takeLast 0 k = 0

theorem LO.Arith.takeLast_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} (x : V) (v : V) : LO.Arith.takeLast (cons x v) k = if LO.Arith.len v < k then cons x v else LO.Arith.takeLast v k

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.takeLast_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.takeLast

Equations

• ⋯ = ⋯

theorem LO.Arith.len_takeLast {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {k : V} (h : k ≤ LO.Arith.len v) : LO.Arith.len (LO.Arith.takeLast v k) = k

@[simp]

theorem LO.Arith.takeLast_len_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) : LO.Arith.takeLast v (LO.Arith.len v) = v

@[simp]

theorem LO.Arith.add_sub_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) (c : V) : a + c - (b + c) = a - b

TODO: move

@[simp]

theorem LO.Arith.takeLast_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) : LO.Arith.takeLast v 0 = 0

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

Concatation

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

Equations

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

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

Equations

• LO.Arith.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 := ⋯ }

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

Equations

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

Instances For

• LO.Arith.concat_definable
• LO.Arith.concat_definable'

@[simp]

theorem LO.Arith.concat_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (z : V) : LO.Arith.concat 0 z = ?[z]

@[simp]

theorem LO.Arith.concat_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) (z : V) : LO.Arith.concat (cons x v) z = cons x (LO.Arith.concat v z)

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.concat_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.concat

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.len_concat {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (z : V) : LO.Arith.len (LO.Arith.concat v z) = LO.Arith.len v + 1

theorem LO.Arith.concat_nth_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (z : V) {i : V} (hi : i < LO.Arith.len v) : LO.Arith.nth (LO.Arith.concat v z) i = LO.Arith.nth v i

@[simp]

theorem LO.Arith.concat_nth_len {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (z : V) : LO.Arith.nth (LO.Arith.concat v z) (LO.Arith.len v) = z

theorem LO.Arith.concat_nth_len' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (z : V) {i : V} (hi : LO.Arith.len v = i) : LO.Arith.nth (LO.Arith.concat v z) i = z

Membership

def LO.Arith.MemVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : Prop

Equations

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

Instances For

• LO.Arith.memVec_definable
• LO.Arith.memVec_definable'

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

Equations

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

@[simp]

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

theorem LO.Arith.nth_mem_memVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {v : V} (h : i < LO.Arith.len v) : LO.Arith.MemVec (LO.Arith.nth v i) v

@[simp]

theorem LO.Arith.memVec_insert_fst {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {v : V} : LO.Arith.MemVec x (cons x v)

@[simp]

theorem LO.Arith.memVec_cons_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {v : V} : LO.Arith.MemVec x (cons y v) ↔ x = y ∨ LO.Arith.MemVec x v

theorem LO.Arith.le_of_memVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {v : V} (h : LO.Arith.MemVec x v) : x ≤ v

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

Subset

def LO.Arith.SubsetVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : V) (w : V) : Prop

Equations

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

Instances For

• LO.Arith.subsetVec_definable
• LO.Arith.subsetVec_definable'

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

Equations

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

@[simp]

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

@[simp]

theorem LO.Arith.subsetVec_insert_tail {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (v : V) : LO.Arith.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.Arith.subsetVec_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚫₁-Relation LO.Arith.SubsetVec via LO.FirstOrder.Arith.subsetVecDef

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

Repeat

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

Equations

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

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

Equations

• LO.Arith.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 := ⋯ }

def LO.Arith.repeatVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) : V

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

Equations

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

Instances For

• LO.Arith.repeatVec_definable
• LO.Arith.repeatVec_definable'

@[simp]

theorem LO.Arith.repeatVec_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : LO.Arith.repeatVec x 0 = 0

@[simp]

theorem LO.Arith.repeatVec_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) : LO.Arith.repeatVec x (k + 1) = cons x (LO.Arith.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.Arith.repeatVec_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ LO.Arith.repeatVec via LO.FirstOrder.Arith.repeatVecDef

@[simp]

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.repeatVec_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : ℕ} (Γ : LO.SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.repeatVec

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.len_repeatVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) : LO.Arith.len (LO.Arith.repeatVec x k) = k

@[simp]

theorem LO.Arith.le_repaetVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) : k ≤ LO.Arith.repeatVec x k

theorem LO.Arith.nth_repeatVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (k : V) {i : V} (h : i < k) : LO.Arith.nth (LO.Arith.repeatVec x k) i = x

theorem LO.Arith.len_repeatVec_of_nth_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {m : V} (H : ∀ i < LO.Arith.len v, LO.Arith.nth v i ≤ m) : v ≤ LO.Arith.repeatVec m (LO.Arith.len v)

Convert to Set

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

Equations

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

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

Equations

• LO.Arith.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 := ⋯ }

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

Equations

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

Instances For

• LO.Arith.vecToSet_definable
• LO.Arith.vecToSet_definable'

@[simp]

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

@[simp]

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

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

Equations

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

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

@[simp]

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.vecToSet_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : ℕ} (Γ : LO.SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.vecToSet

Equations

• ⋯ = ⋯

theorem LO.Arith.mem_vecToSet_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {x : V} : x ∈ LO.Arith.vecToSet v ↔ ∃ i < LO.Arith.len v, x = LO.Arith.nth v i

@[simp]

theorem LO.Arith.nth_mem_vecToSet {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {i : V} (h : i < LO.Arith.len v) : LO.Arith.nth v i ∈ LO.Arith.vecToSet v