Vec

@[implicit_reducible]

noncomputable instance LO.Arith.instCons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : Cons V V

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

def LO.FirstOrder.Arith.consDef : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

instance LO.Arith.cons_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₂ cons

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

def LO.FirstOrder.Arith.mkVec₁Def : Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

def LO.FirstOrder.Arith.mkVec₂Def : Sg1.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

N-th element of List

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

Imported declaration from the Incompleteness formalization.

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 : Fixpoint.Blueprint 0

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Arith.Nth.graphDef : FirstOrder.Arith.Sg1.Semisentence 1

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

@[simp]

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

TODO: move

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

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

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem LO.Arith.cons_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (Γ : 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.Arith.cons_induction_sigma1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {P : V → Prop} (hP : FirstOrder.Arith.Sg1-Predicate P) (nil : P 0) (cons : ∀ (x v : V), P v → P (cons x v)) (v : V) : P v

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

def LO.FirstOrder.Arith.nthDef : Sg1.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

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

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

TODO: move

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

@[simp]

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

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

@[simp]

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

Inductivly Construction of Function on List

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

Imported declaration from the Incompleteness formalization.

• nil : FirstOrder.Arith.Sg1.Semisentence (arity + 1)

  Imported declaration from the Incompleteness formalization.

• cons : FirstOrder.Arith.Sg1.Semisentence (arity + 4)

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

• β.graphDef = β.blueprint.fixpointDef

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• nil (param : Fin arity → V) : V

  Imported declaration from the Incompleteness formalization.

• cons (param : Fin arity → V) (x xs ih : V) : V

  Imported declaration from the Incompleteness formalization.

• 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.Arith.VecRec.Construction.Phi {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (C : Set V) (pr : V) : Prop

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : Fixpoint.Construction V β.blueprint

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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

theorem LO.Arith.VecRec.Construction.graph_case {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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.Arith.VecRec.Construction.graph_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {arity : ℕ} {β : Blueprint arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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.Arith.VecRec.Construction.graph_exists {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {arity : ℕ} {β : Blueprint arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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.Arith.VecRec.Construction.graph_existsUnique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (xs : V) : ∃! y : V, c.Graph param ⟪xs, y⟫

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.VecRec.Construction.result_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {arity : ℕ} {β : Blueprint arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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.Arith.VecRec.Construction.result_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {arity : ℕ} {β : Blueprint arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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.Arith.VecRec.Construction.result_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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

theorem LO.Arith.VecRec.Construction.eval_resultDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (v : Fin (arity + 2) → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val β.resultDef) ↔ v 0 = c.result (fun (x : Fin arity) => v x.succ.succ) (v 1)

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

instance LO.Arith.VecRec.Construction.result_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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.Arith.Len.blueprint : VecRec.Blueprint 0

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Arith.lenDef : Sg1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

Maximum of List

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Arith.listMaxDef : Sg1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

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

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

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

Take Last k-Element

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

theorem LO.Arith.takeLast_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 : Sg1.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

TODO: move

@[simp]

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

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

Concatation

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Arith.concatDef : Sg1.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

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

Membership

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (x : V) : ¬MemVec x 0

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

@[simp]

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

@[simp]

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

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

def LO.FirstOrder.Arith.memVecDef : Dlt1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

instance LO.Arith.memVec_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Dlt1-Relation MemVec

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

Subset

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : V) : SubsetVec v v

@[simp]

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

def LO.FirstOrder.Arith.subsetVecDef : Dlt1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

instance LO.Arith.subsetVec_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Dlt1-Relation SubsetVec

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

Repeat

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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 := ⋯ }

noncomputable def LO.Arith.repeatVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (x 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

@[simp]

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

@[simp]

theorem LO.Arith.repeatVec_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (x k : V) : repeatVec x (k + 1) = cons x (repeatVec x k)

def LO.FirstOrder.Arith.repeatVecDef : Sg1.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

Convert to Set

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Arith.vecToSetDef : Sg1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

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

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

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

@[simp]

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