@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedBy {V : Type u_2} [ORingStructure V] {k : ℕ} (R : (Fin k → V) → Prop) {ℌ : HierarchySymbol} : ℌ.Semisentence k → Prop

Equations

• LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedBy R φ = LO.FirstOrder.IsDefinedBy R ↑φ
• LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedBy R φ = LO.FirstOrder.IsDefinedBy R ↑φ
• LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedBy R φ = (LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn V φ ∧ LO.FirstOrder.IsDefinedBy R ↑φ)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedByWithParam {V : Type u_2} [ORingStructure V] {k : ℕ} (R : (Fin k → V) → Prop) {ℌ : HierarchySymbol} : HierarchySymbol.Semiformula V k ℌ → Prop

Equations

• LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedByWithParam R φ = LO.FirstOrder.IsDefinedByWithParam R ↑φ
• LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedByWithParam R φ = LO.FirstOrder.IsDefinedByWithParam R ↑φ
• LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedByWithParam R φ = (LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn V φ ∧ LO.FirstOrder.IsDefinedByWithParam R ↑φ)

class LO.FirstOrder.Arithmetic.HierarchySymbol.Defined {V : Type u_2} [ORingStructure V] {k : ℕ} (R : outParam ((Fin k → V) → Prop)) {ℌ : HierarchySymbol} (φ : ℌ.Semisentence k) : Prop

• defined : IsDefinedBy R φ

class LO.FirstOrder.Arithmetic.HierarchySymbol.Definable {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) {k : ℕ} (P : (Fin k → V) → Prop) : Prop

• definable : ∃ (φ : HierarchySymbol.Semiformula V k ℌ), IsDefinedByWithParam P φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedPred {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (P : V → Prop) (φ : ℌ.Semisentence 1) : Prop

Equations

• (ℌ-Predicate P via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.Defined (fun (v : Fin 1 → V) => P (v 0)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedRel {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (R : V → V → Prop) (φ : ℌ.Semisentence 2) : Prop

Equations

• (ℌ-Relation R via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.Defined (fun (v : Fin 2 → V) => R (v 0) (v 1)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedRel₃ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (R : V → V → V → Prop) (φ : ℌ.Semisentence 3) : Prop

Equations

• (ℌ-Relation₃ R via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.Defined (fun (v : Fin 3 → V) => R (v 0) (v 1) (v 2)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedRel₄ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (R : V → V → V → V → Prop) (φ : ℌ.Semisentence 4) : Prop

Equations

• (ℌ-Relation₄ R via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.Defined (fun (v : Fin 4 → V) => R (v 0) (v 1) (v 2) (v 3)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} (f : (Fin k → V) → V) (φ : ℌ.Semisentence (k + 1)) : Prop

Equations

• LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction f φ = LO.FirstOrder.Arithmetic.HierarchySymbol.Defined (fun (v : Fin (k + 1) → V) => v 0 = f fun (x : Fin k) => v x.succ) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction₀ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (c : V) (φ : ℌ.Semisentence 1) : Prop

Equations

• (ℌ-Function₀ c via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction (fun (x : Fin 0 → V) => c) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction₁ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V) (φ : ℌ.Semisentence 2) : Prop

Equations

• (ℌ-Function₁ f via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction (fun (v : Fin 1 → V) => f (v 0)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction₂ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V → V) (φ : ℌ.Semisentence 3) : Prop

Equations

• (ℌ-Function₂ f via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction (fun (v : Fin 2 → V) => f (v 0) (v 1)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction₃ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V → V → V) (φ : ℌ.Semisentence 4) : Prop

Equations

• (ℌ-Function₃ f via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction (fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction₄ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V → V → V → V) (φ : ℌ.Semisentence 5) : Prop

Equations

• (ℌ-Function₄ f via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction (fun (v : Fin 4 → V) => f (v 0) (v 1) (v 2) (v 3)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction₅ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V → V → V → V → V) (φ : ℌ.Semisentence 6) : Prop

Equations

• (ℌ-Function₅ f via φ) = LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction (fun (v : Fin 5 → V) => f (v 0) (v 1) (v 2) (v 3) (v 4)) φ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinablePred {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (P : V → Prop) : Prop

Equations

• (ℌ-Predicate P) = ℌ.Definable fun (v : Fin 1 → V) => P (v 0)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (P : V → V → Prop) : Prop

Equations

• (ℌ-Relation P) = ℌ.Definable fun (v : Fin 2 → V) => P (v 0) (v 1)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel₃ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (P : V → V → V → Prop) : Prop

Equations

• (ℌ-Relation₃ P) = ℌ.Definable fun (v : Fin 3 → V) => P (v 0) (v 1) (v 2)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel₄ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (P : V → V → V → V → Prop) : Prop

Equations

• (ℌ-Relation₄ P) = ℌ.Definable fun (v : Fin 4 → V) => P (v 0) (v 1) (v 2) (v 3)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel₅ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (P : V → V → V → V → V → Prop) : Prop

Equations

• (ℌ-Relation₅ P) = ℌ.Definable fun (v : Fin 5 → V) => P (v 0) (v 1) (v 2) (v 3) (v 4)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel₆ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (P : V → V → V → V → V → V → Prop) : Prop

Equations

• ℌ.DefinableRel₆ P = ℌ.Definable fun (v : Fin 6 → V) => P (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) {k : ℕ} (f : (Fin k → V) → V) : Prop

Equations

• ℌ.DefinableFunction f = ℌ.Definable fun (v : Fin (k + 1) → V) => v 0 = f fun (x : Fin k) => v x.succ

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₀ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (c : V) : Prop

Equations

• ℌ.DefinableFunction₀ c = ℌ.DefinableFunction fun (x : Fin 0 → V) => c

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₁ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V) : Prop

Equations

• (ℌ-Function₁ f) = ℌ.DefinableFunction fun (v : Fin 1 → V) => f (v 0)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V → V) : Prop

Equations

• (ℌ-Function₂ f) = ℌ.DefinableFunction fun (v : Fin 2 → V) => f (v 0) (v 1)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₃ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V → V → V) : Prop

Equations

• (ℌ-Function₃ f) = ℌ.DefinableFunction fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₄ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V → V → V → V) : Prop

Equations

• (ℌ-Function₄ f) = ℌ.DefinableFunction fun (v : Fin 4 → V) => f (v 0) (v 1) (v 2) (v 3)

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₅ {V : Type u_2} [ORingStructure V] (ℌ : HierarchySymbol) (f : V → V → V → V → V → V) : Prop

Equations

• ℌ.DefinableFunction₅ f = ℌ.DefinableFunction fun (v : Fin 5 → V) => f (v 0) (v 1) (v 2) (v 3) (v 4)

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Predicate_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₃_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₄_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₀_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₁_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₂_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₃_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₄_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₅_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Predicate_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₃_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₄_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₅_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₁_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₂_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₃_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₄_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Predicate[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₃[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₄[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₀[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₁[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₂[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₃[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₄[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₅[_]_Via_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Predicate[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₃[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₄[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Relation₅[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₁[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₂[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₃[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.HierarchySymbol.«term_-Function₄[_]_» : Lean.TrailingParserDescr

Equations

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

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.df {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : ℌ.Semisentence k} (h : Defined R φ) : FirstOrder.IsDefinedBy R ↑φ

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.proper {V : Type u_2} [ORingStructure V] {k : ℕ} {R : (Fin k → V) → Prop} {m : ℕ} {φ : { Γ := 𝚫, rank := m }.Semisentence k} [h : Defined R φ] : Semiformula.ProperOn V φ

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.iff {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {v : Fin k → V} {R : (Fin k → V) → Prop} {φ : ℌ.Semisentence k} [h : Defined R φ] : (Semiformula.Evalb v) ↑φ ↔ R v

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.iff_delta_pi {V : Type u_2} [ORingStructure V] {k m : ℕ} {v : Fin k → V} {R : (Fin k → V) → Prop} {φ : { Γ := 𝚫, rank := m }.Semisentence k} [h : Defined R φ] : (Semiformula.Evalb v) ↑(Semiformula.pi φ) ↔ R v

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.iff_delta_sigma {V : Type u_2} [ORingStructure V] {k m : ℕ} {v : Fin k → V} {R : (Fin k → V) → Prop} {φ : { Γ := 𝚫, rank := m }.Semisentence k} [h : Defined R φ] : (Semiformula.Evalb v) ↑(Semiformula.sigma φ) ↔ R v

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.of_zero {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : 𝚺₀.Semisentence k} (h : Defined R φ) : Defined R (Semiformula.ofZero φ ℌ)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.of_iff {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} (h : ∀ (x : Fin k → V), P x ↔ Q x) {φ : ℌ.Semisentence k} (H : Defined Q φ) : Defined P φ

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.to_definable {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} (φ : ℌ.Semisentence k) (hP : Defined P φ) : ℌ.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Defined.to_definable₀ {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} {φ : 𝚺₀.Semisentence k} (hP : Defined P φ) : ℌ.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction.of_eq {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {f g : (Fin k → V) → V} (h : ∀ (x : Fin k → V), f x = g x) {φ : ℌ.Semisentence (k + 1)} (H : DefinedFunction f φ) : DefinedFunction g φ

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction.graph_delta {V : Type u_2} [ORingStructure V] {k m : ℕ} {f : (Fin k → V) → V} {φ : { Γ := 𝚺, rank := m }.Semisentence (k + 1)} (h : DefinedFunction f φ) : DefinedFunction f (Semiformula.graphDelta φ)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedByWithParam.df {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : HierarchySymbol.Semiformula V k ℌ} (h : IsDefinedByWithParam R φ) : FirstOrder.IsDefinedByWithParam R ↑φ

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedByWithParam.iff {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : HierarchySymbol.Semiformula V k ℌ} (h : IsDefinedByWithParam R φ) {v : Fin k → V} : (Semiformula.Eval v id) ↑φ ↔ R v

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.IsDefinedByWithParam.proper {V : Type u_2} [ORingStructure V] {k : ℕ} {R : (Fin k → V) → Prop} {m : ℕ} {φ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (h : IsDefinedByWithParam R φ) : Semiformula.ProperWithParamOn V φ

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel.eq {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} : ℌ-Relation Eq

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel.lt {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} : ℌ-Relation LT.lt

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel.le {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : ℌ-Relation LE.le

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.add {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} : ℌ-Function₂ fun (x1 x2 : V) => x1 + x2

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.mul {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} : ℌ-Function₂ fun (x1 x2 : V) => x1 * x2

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.hAdd {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} : ℌ-Function₂ HAdd.hAdd

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.hMul {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} : ℌ-Function₂ HMul.hMul

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.sq {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : ℌ-Function₁ fun (x : V) => x ^ 2

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.pow3 {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : ℌ-Function₁ fun (x : V) => x ^ 3

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.pow4 {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : ℌ-Function₁ fun (x : V) => x ^ 4

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.mk' {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {ℌ : HierarchySymbol} (φ : HierarchySymbol.Semiformula V k ℌ) (H : IsDefinedByWithParam P φ) : ℌ.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.mkPolarity {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} {Γ : Polarity} (φ : ArithmeticSemiformula V k) (hp : Hierarchy Γ m φ) (hP : ∀ (v : Fin k → V), P v ↔ (Semiformula.Eval v id) φ) : { Γ := Γ.coe, rank := m }.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.of_zero {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {Γ' : SigmaPiDelta} (h : { Γ := Γ', rank := 0 }.Definable P) {ℌ : HierarchySymbol} : ℌ.Definable P

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.instOfSigmaZero {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} [𝚺₀.Definable P] (ℌ : HierarchySymbol) : ℌ.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.of_deltaOne {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {Γ : SigmaPiDelta} {m : ℕ} (h : 𝚫₁.Definable P) : { Γ := Γ, rank := m + 1 }.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.of_delta {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} (h : { Γ := 𝚫, rank := m }.Definable P) : { Γ := Γ, rank := m }.Definable P

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.instMkOfDeltaSigmaPiDelta {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} [{ Γ := 𝚫, rank := m }.Definable P] (Γ : SigmaPiDelta) : { Γ := Γ, rank := m }.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.delta_iff_sigma_and_pi {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} : { Γ := 𝚫, rank := m }.Definable P ↔ { Γ := 𝚷, rank := m }.Definable P ∧ { Γ := 𝚺, rank := m }.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.of_sigma_of_pi {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} (hσ : { Γ := 𝚺, rank := m }.Definable P) (hπ : { Γ := 𝚷, rank := m }.Definable P) : { Γ := Γ, rank := m }.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.of_iff {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} (H : ℌ.Definable Q) (h : ∀ (x : Fin k → V), P x ↔ Q x) : ℌ.Definable P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.retraction {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} {l : ℕ} (h : ℌ.Definable P) (f : Fin k → Fin l) : ℌ.Definable fun (v : Fin l → V) => P fun (i : Fin k) => v (f i)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.retractiont (n : ℕ) {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} (h : ℌ.Definable P) (f : Fin k → ArithmeticSemiterm V n) : ℌ.Definable fun (v : Fin n → V) => P fun (i : Fin k) => Semiterm.val v id (f i)

@[simp]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.const {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P : Prop} : ℌ.Definable fun (x : Fin k → V) => P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.and {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} (hP : ℌ.Definable P) (hQ : ℌ.Definable Q) : ℌ.Definable fun (x : Fin k → V) => P x ∧ Q x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.or {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} (hP : ℌ.Definable P) (hQ : ℌ.Definable Q) : ℌ.Definable fun (x : Fin k → V) => P x ∨ Q x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.notSigma {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} (h : { Γ := 𝚺, rank := m }.Definable P) : { Γ := 𝚷, rank := m }.Definable fun (x : Fin k → V) => ¬P x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.notPi {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} (h : { Γ := 𝚷, rank := m }.Definable P) : { Γ := 𝚺, rank := m }.Definable fun (x : Fin k → V) => ¬P x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.notDelta {V : Type u_2} [ORingStructure V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} (h : { Γ := 𝚫, rank := m }.Definable P) : { Γ := 𝚫, rank := m }.Definable fun (x : Fin k → V) => ¬P x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.not {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} (h : { Γ := Γ.alt, rank := m }.Definable P) : { Γ := Γ, rank := m }.Definable fun (v : Fin k → V) => ¬P v

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.impDelta {V : Type u_2} [ORingStructure V] {k : ℕ} {P Q : (Fin k → V) → Prop} {m : ℕ} (hp : { Γ := 𝚫, rank := m }.Definable P) (hq : { Γ := 𝚫, rank := m }.Definable Q) : { Γ := 𝚫, rank := m }.Definable fun (x : Fin k → V) => P x → Q x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.imp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {k : ℕ} {P Q : (Fin k → V) → Prop} {m : ℕ} (h₁ : { Γ := Γ.alt, rank := m }.Definable P) (h₂ : { Γ := Γ, rank := m }.Definable Q) : { Γ := Γ, rank := m }.Definable fun (v : Fin k → V) => P v → Q v

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.biconditional {V : Type u_2} [ORingStructure V] {k : ℕ} {P Q : (Fin k → V) → Prop} {m : ℕ} (h₁ : { Γ := 𝚫, rank := m }.Definable P) (h₂ : { Γ := 𝚫, rank := m }.Definable Q) {Γ : SigmaPiDelta} : { Γ := Γ, rank := m }.Definable fun (v : Fin k → V) => P v ↔ Q v

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → V → Prop} (h : ℌ.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) (t : ArithmeticSemiterm V k) : ℌ.Definable fun (v : Fin k → V) => ∀ x < Semiterm.val v id t, P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → V → Prop} (h : ℌ.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) (t : ArithmeticSemiterm V k) : ℌ.Definable fun (v : Fin k → V) => ∃ x < Semiterm.val v id t, P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball' {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {P : (Fin k → V) → V → Prop} (h : ℌ.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) (t : ArithmeticSemiterm V k) : ℌ.Definable fun (v : Fin k → V) => ∀ x ≤ Semiterm.val v id t, P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs' {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {P : (Fin k → V) → V → Prop} (h : ℌ.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) (t : ArithmeticSemiterm V k) : ℌ.Definable fun (v : Fin k → V) => ∃ x ≤ Semiterm.val v id t, P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.exs {V : Type u_2} [ORingStructure V] {k m : ℕ} {P : (Fin k → V) → V → Prop} (h : { Γ := 𝚺, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := 𝚺, rank := m + 1 }.Definable fun (v : Fin k → V) => ∃ (x : V), P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.all {V : Type u_2} [ORingStructure V] {k m : ℕ} {P : (Fin k → V) → V → Prop} (h : { Γ := 𝚷, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := 𝚷, rank := m + 1 }.Definable fun (v : Fin k → V) => ∀ (x : V), P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.conj₂ {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {ι : Type u_3} (Γ : List ι) {R : ι → (Fin k → V) → Prop} (hR : ∀ (i : ι), ℌ.Definable (R i)) : ℌ.Definable fun (x : Fin k → V) => ∀ i ∈ Γ, R i x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.disj₂ {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {ι : Type u_3} (Γ : List ι) {R : ι → (Fin k → V) → Prop} (hR : ∀ (i : ι), ℌ.Definable (R i)) : ℌ.Definable fun (x : Fin k → V) => ∃ i ∈ Γ, R i x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.fconj {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {ι : Type u_3} (s : Finset ι) {R : ι → (Fin k → V) → Prop} (h : ∀ (i : ι), ℌ.Definable (R i)) : ℌ.Definable fun (x : Fin k → V) => ∀ i ∈ s, R i x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.fdisj {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {ι : Type u_3} (s : Finset ι) {R : ι → (Fin k → V) → Prop} (h : ∀ (i : ι), ℌ.Definable (R i)) : ℌ.Definable fun (x : Fin k → V) => ∃ i ∈ s, R i x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.fintype_all {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {ι : Type u_3} [Fintype ι] {P : ι → (Fin k → V) → Prop} (h : ∀ (i : ι), ℌ.Definable fun (w : Fin k → V) => P i w) : ℌ.Definable fun (v : Fin k → V) => ∀ (i : ι), P i v

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.fintype_exs {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {ι : Type u_3} [Fintype ι] {P : ι → (Fin k → V) → Prop} (h : ∀ (i : ι), ℌ.Definable fun (w : Fin k → V) => P i w) : ℌ.Definable fun (v : Fin k → V) => ∃ (i : ι), P i v

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.equal' {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} (i j : Fin k) : ℌ.Definable fun (v : Fin k → V) => v i = v j

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.of_sigma {V : Type u_2} [ORingStructure V] {k m : ℕ} {f : (Fin k → V) → V} (h : { Γ := 𝚺, rank := m }.DefinableFunction f) {Γ : SigmaPiDelta} : { Γ := Γ, rank := m }.DefinableFunction f

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.exsVec {V : Type u_2} [ORingStructure V] {m k l : ℕ} {P : (Fin k → V) → (Fin l → V) → Prop} (h : { Γ := 𝚺, rank := m + 1 }.Definable fun (w : Fin (k + l) → V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) : { Γ := 𝚺, rank := m + 1 }.Definable fun (v : Fin k → V) => ∃ (ys : Fin l → V), P v ys

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.allVec {V : Type u_2} [ORingStructure V] {m k l : ℕ} {P : (Fin k → V) → (Fin l → V) → Prop} (h : { Γ := 𝚷, rank := m + 1 }.Definable fun (w : Fin (k + l) → V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) : { Γ := 𝚷, rank := m + 1 }.Definable fun (v : Fin k → V) => ∀ (ys : Fin l → V), P v ys

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.substitution {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {k : ℕ} {P : (Fin k → V) → Prop} {l m : ℕ} {f : Fin k → (Fin l → V) → V} (hP : { Γ := Γ, rank := m + 1 }.Definable P) (hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.DefinableFunction (f i)) : { Γ := Γ, rank := m + 1 }.Definable fun (z : Fin l → V) => P fun (i : Fin k) => f i z

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinablePred.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m : ℕ} {P : V → Prop} {k : ℕ} {f : (Fin k → V) → V} (hP : { Γ := Γ, rank := m + 1 }-Predicate P) (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m : ℕ} {P : V → V → Prop} {k : ℕ} {f g : (Fin k → V) → V} (hP : { Γ := Γ, rank := m + 1 }-Relation P) (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (hg : { Γ := 𝚺, rank := m + 1 }.DefinableFunction g) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f v) (g v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel₃.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → Prop} {f₁ f₂ f₃ : (Fin k → V) → V} (hP : { Γ := Γ, rank := m + 1 }-Relation₃ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f₁ v) (f₂ v) (f₃ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel₄.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → V → Prop} {f₁ f₂ f₃ f₄ : (Fin k → V) → V} (hP : { Γ := Γ, rank := m + 1 }-Relation₄ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₄) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableRel₅.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → V → V → Prop} {f₁ f₂ f₃ f₄ f₅ : (Fin k → V) → V} (hP : { Γ := Γ, rank := m + 1 }-Relation₅ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₅) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.comp₁ {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → Prop} {f : (Fin k → V) → V} [{ Γ := Γ, rank := m + 1 }-Predicate P] (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.comp₂ {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → Prop} {f g : (Fin k → V) → V} [{ Γ := Γ, rank := m + 1 }-Relation P] (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (hg : { Γ := 𝚺, rank := m + 1 }.DefinableFunction g) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f v) (g v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.comp₃ {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → Prop} {f₁ f₂ f₃ : (Fin k → V) → V} [{ Γ := Γ, rank := m + 1 }-Relation₃ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f₁ v) (f₂ v) (f₃ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.comp₄ {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → V → Prop} {f₁ f₂ f₃ f₄ : (Fin k → V) → V} [{ Γ := Γ, rank := m + 1 }-Relation₄ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₄) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.comp₅ {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → V → V → Prop} {f₁ f₂ f₃ f₄ f₅ : (Fin k → V) → V} [{ Γ := Γ, rank := m + 1 }-Relation₅ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₅) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinablePred.of_iff {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {P Q : V → Prop} (H : ℌ-Predicate Q) (h : ∀ (x : V), P x ↔ Q x) : ℌ-Predicate P

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.graph {V : Type u_2} [ORingStructure V] {k : ℕ} {ℌ : HierarchySymbol} {f : (Fin k → V) → V} (h : ℌ.DefinableFunction f) : ℌ.Definable fun (v : Fin (k + 1) → V) => v 0 = f fun (x : Fin k) => v x.succ

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₁.graph {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {f : V → V} [h : ℌ-Function₁ f] : ℌ-Relation Function.Graph f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.graph {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {f : V → V → V} [h : ℌ-Function₂ f] : ℌ-Relation₃ Function.Graph₂ f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₃.graph {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {f : V → V → V → V} [h : ℌ-Function₃ f] : ℌ-Relation₄ Function.Graph₃ f

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.graph_delta {V : Type u_2} [ORingStructure V] {k : ℕ} {f : (Fin k → V) → V} {m : ℕ} (h : { Γ := 𝚺, rank := m }.DefinableFunction f) : { Γ := 𝚫, rank := m }.DefinableFunction f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.instMkDeltaSigmaPiDeltaOfSigma {V : Type u_2} [ORingStructure V] {k : ℕ} {f : (Fin k → V) → V} {m : ℕ} [h : { Γ := 𝚺, rank := m }.DefinableFunction f] : { Γ := 𝚫, rank := m }.DefinableFunction f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.instOfSigmaZero {V : Type u_2} [ORingStructure V] {k : ℕ} {ℌ : HierarchySymbol} {f : (Fin k → V) → V} [𝚺₀.DefinableFunction f] : ℌ.DefinableFunction f

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.of_sigmaOne {V : Type u_2} [ORingStructure V] {k : ℕ} {f : (Fin k → V) → V} (h : 𝚺₁.DefinableFunction f) {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }.DefinableFunction f

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.var {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} (i : Fin k) : ℌ.DefinableFunction fun (v : Fin k → V) => v i

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.const {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} (c : V) : ℌ.DefinableFunction fun (x : Fin k → V) => c

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.term_retraction (n : ℕ) {V : Type u_2} [ORingStructure V] {k : ℕ} {ℌ : HierarchySymbol} (t : ArithmeticSemiterm V n) (e : Fin n → Fin k) : ℌ.DefinableFunction fun (v : Fin k → V) => Semiterm.val (fun (x : Fin n) => v (e x)) id t

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.term {V : Type u_2} [ORingStructure V] {k : ℕ} {ℌ : HierarchySymbol} (t : ArithmeticSemiterm V k) : ℌ.DefinableFunction fun (v : Fin k → V) => Semiterm.val v id t

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.of_eq {V : Type u_2} [ORingStructure V] {k : ℕ} {ℌ : HierarchySymbol} {f : (Fin k → V) → V} (g : (Fin k → V) → V) (h : ∀ (v : Fin k → V), f v = g v) (H : ℌ.DefinableFunction f) : ℌ.DefinableFunction g

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.retraction {V : Type u_2} [ORingStructure V] {k : ℕ} {ℌ : HierarchySymbol} {f : (Fin k → V) → V} {n : ℕ} (hf : ℌ.DefinableFunction f) (e : Fin k → Fin n) : ℌ.DefinableFunction fun (v : Fin n → V) => f fun (i : Fin k) => v (e i)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.retractiont {V : Type u_2} [ORingStructure V] {k : ℕ} {ℌ : HierarchySymbol} {f : (Fin k → V) → V} {n : ℕ} (hf : ℌ.DefinableFunction f) (t : Fin k → ArithmeticSemiterm V n) : ℌ.DefinableFunction fun (v : Fin n → V) => f fun (i : Fin k) => Semiterm.val v id (t i)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.rel {V : Type u_2} [ORingStructure V] {k : ℕ} {ℌ : HierarchySymbol} {f : (Fin k → V) → V} (h : ℌ.DefinableFunction f) : ℌ.Definable fun (v : Fin (k + 1) → V) => v 0 = f fun (x : Fin k) => v x.succ

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.nth {V : Type u_2} [ORingStructure V] {k : ℕ} (ℌ : HierarchySymbol) (i : Fin k) : ℌ.DefinableFunction fun (w : Fin k → V) => w i

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.substitution {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {k l m : ℕ} {F : (Fin k → V) → V} {f : Fin k → (Fin l → V) → V} (hF : { Γ := Γ, rank := m + 1 }.DefinableFunction F) (hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.DefinableFunction (f i)) : { Γ := Γ, rank := m + 1 }.DefinableFunction fun (z : Fin l → V) => F fun (i : Fin k) => f i z

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₁.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V} {f : (Fin k → V) → V} [hF : { Γ := Γ, rank := m + 1 }-Function₁ F] (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) : { Γ := Γ, rank := m + 1 }.DefinableFunction fun (v : Fin k → V) => F (f v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V → V} {f₁ f₂ : (Fin k → V) → V} [hF : { Γ := Γ, rank := m + 1 }-Function₂ F] (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) : { Γ := Γ, rank := m + 1 }.DefinableFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₃.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V → V → V} {f₁ f₂ f₃ : (Fin k → V) → V} [hF : { Γ := Γ, rank := m + 1 }-Function₃ F] (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) : { Γ := Γ, rank := m + 1 }.DefinableFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₄.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V → V → V → V} {f₁ f₂ f₃ f₄ : (Fin k → V) → V} [hF : { Γ := Γ, rank := m + 1 }-Function₄ F] (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₄) : { Γ := Γ, rank := m + 1 }.DefinableFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₅.comp {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V → V → V → V → V} {f₁ f₂ f₃ f₄ f₅ : (Fin k → V) → V} [hF : { Γ := Γ, rank := m + 1 }.DefinableFunction₅ F] (hf₁ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f₅) : { Γ := Γ, rank := m + 1 }.DefinableFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_lt {V : Type u_2} [ORingStructure V] {k m : ℕ} {Γ : SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (h : { Γ := Γ, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => ∀ x < f v, P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs_lt {V : Type u_2} [ORingStructure V] {k m : ℕ} {Γ : SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (h : { Γ := Γ, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => ∃ x < f v, P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_le {V : Type u_2} [ORingStructure V] {k m : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {Γ : SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (h : { Γ := Γ, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => ∀ x ≤ f v, P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs_le {V : Type u_2} [ORingStructure V] {k m : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {Γ : SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (h : { Γ := Γ, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => ∃ x ≤ f v, P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_lt' {V : Type u_2} [ORingStructure V] {k m : ℕ} {Γ : SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (h : { Γ := Γ, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => ∀ {x : V}, x < f v → P v x

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_le' {V : Type u_2} [ORingStructure V] {k m : ℕ} [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {Γ : SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (h : { Γ := Γ, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => ∀ {x : V}, x ≤ f v → P v x

Auxiliary lemmata for aesop

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableMkSigmaSigmaPiDeltaHAddNatOfNat {V : Type u_2} [ORingStructure V] {k : ℕ} (P : (Fin k → V) → Prop) [𝚺₁.Definable P] : { Γ := 𝚺, rank := 0 + 1 }.Definable P

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableMkPiSigmaPiDeltaHAddNatOfNat {V : Type u_2} [ORingStructure V] {k : ℕ} (P : (Fin k → V) → Prop) [𝚷₁.Definable P] : { Γ := 𝚷, rank := 0 + 1 }.Definable P

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableMkDeltaSigmaPiDeltaHAddNatOfNat {V : Type u_2} [ORingStructure V] {k : ℕ} (P : (Fin k → V) → Prop) [𝚫₁.Definable P] : { Γ := 𝚫, rank := 0 + 1 }.Definable P

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableFunctionMkSigmaSigmaPiDeltaHAddNatOfNat {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) [𝚺₁.DefinableFunction f] : { Γ := 𝚺, rank := 0 + 1 }.DefinableFunction f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableFunctionMkPiSigmaPiDeltaHAddNatOfNat {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) [𝚷₁.DefinableFunction f] : { Γ := 𝚷, rank := 0 + 1 }.DefinableFunction f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableFunctionMkDeltaSigmaPiDeltaHAddNatOfNat {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) [𝚫₁.DefinableFunction f] : { Γ := 𝚫, rank := 0 + 1 }.DefinableFunction f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableMkSigmaSigmaPiDeltaHAddNatOfNat_1 {V : Type u_2} [ORingStructure V] {k : ℕ} (P : (Fin k → V) → Prop) [{ Γ := 𝚺, rank := 2 }.Definable P] : { Γ := 𝚺, rank := 0 + 1 + 1 }.Definable P

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableMkPiSigmaPiDeltaHAddNatOfNat_1 {V : Type u_2} [ORingStructure V] {k : ℕ} (P : (Fin k → V) → Prop) [{ Γ := 𝚷, rank := 2 }.Definable P] : { Γ := 𝚷, rank := 0 + 1 + 1 }.Definable P

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableMkDeltaSigmaPiDeltaHAddNatOfNat_1 {V : Type u_2} [ORingStructure V] {k : ℕ} (P : (Fin k → V) → Prop) [{ Γ := 𝚫, rank := 2 }.Definable P] : { Γ := 𝚫, rank := 0 + 1 + 1 }.Definable P

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableFunctionMkSigmaSigmaPiDeltaHAddNatOfNat_1 {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) [{ Γ := 𝚺, rank := 2 }.DefinableFunction f] : { Γ := 𝚺, rank := 0 + 1 + 1 }.DefinableFunction f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableFunctionMkPiSigmaPiDeltaHAddNatOfNat_1 {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) [{ Γ := 𝚷, rank := 2 }.DefinableFunction f] : { Γ := 𝚷, rank := 0 + 1 + 1 }.DefinableFunction f

instance LO.FirstOrder.Arithmetic.HierarchySymbol.instDefinableFunctionMkDeltaSigmaPiDeltaHAddNatOfNat_1 {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) [{ Γ := 𝚫, rank := 2 }.DefinableFunction f] : { Γ := 𝚫, rank := 0 + 1 + 1 }.DefinableFunction f