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

Equations

• LO.Arith.qqBvar z = ⟪0, z⟫ + 1

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

Equations

• LO.Arith.qqFvar x = ⟪1, x⟫ + 1

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

Equations

• LO.Arith.qqFunc k f v = ⟪2, ⟪k, ⟪f, v⟫⟫⟫ + 1

def LO.Arith.«term^#_» : Lean.ParserDescr

Equations

• LO.Arith.«term^#_» = Lean.ParserDescr.node `LO.Arith.term^#_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^#") (Lean.ParserDescr.cat `term 1024))

def LO.Arith.«term^&_» : Lean.ParserDescr

Equations

• LO.Arith.«term^&_» = Lean.ParserDescr.node `LO.Arith.term^&_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^&") (Lean.ParserDescr.cat `term 1024))

def LO.Arith.«term^func_» : Lean.ParserDescr

Equations

• LO.Arith.«term^func_» = Lean.ParserDescr.node `LO.Arith.term^func_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^func ") (Lean.ParserDescr.cat `term 1024))

@[simp]

theorem LO.Arith.var_lt_qqBvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (z : V) : z < LO.Arith.qqBvar z

@[simp]

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

@[simp]

theorem LO.Arith.arity_lt_qqFunc {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (f : V) (v : V) : k < LO.Arith.qqFunc k f v

@[simp]

theorem LO.Arith.func_lt_qqFunc {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (f : V) (v : V) : f < LO.Arith.qqFunc k f v

@[simp]

theorem LO.Arith.terms_lt_qqFunc {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (f : V) (v : V) : v < LO.Arith.qqFunc k f v

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

@[simp]

theorem LO.Arith.qqBvar_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {z : V} {z' : V} : LO.Arith.qqBvar z = LO.Arith.qqBvar z' ↔ z = z'

@[simp]

theorem LO.Arith.qqFvar_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {x' : V} : LO.Arith.qqFvar x = LO.Arith.qqFvar x' ↔ x = x'

@[simp]

theorem LO.Arith.qqFunc_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} {f : V} {v : V} {k' : V} {f' : V} {w : V} : LO.Arith.qqFunc k f v = LO.Arith.qqFunc k' f' w ↔ k = k' ∧ f = f' ∧ v = w

def LO.FirstOrder.Arith.qqBvarDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.qqBvar_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.qqBvar via LO.FirstOrder.Arith.qqBvarDef

@[simp]

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

def LO.FirstOrder.Arith.qqFvarDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.qqFvar_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.qqFvar via LO.FirstOrder.Arith.qqFvarDef

@[simp]

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

def LO.FirstOrder.Arith.qqFuncDef : 𝚺₀.Semisentence 4

Equations

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

theorem LO.Arith.qqFunc_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₃ LO.Arith.qqFunc via LO.FirstOrder.Arith.qqFuncDef

@[simp]

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

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

Equations

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

def LO.Arith.FormalizedTerm.blueprint (pL : LO.FirstOrder.Arith.LDef) : LO.Arith.Fixpoint.Blueprint 0

Equations

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

def LO.Arith.FormalizedTerm.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : LO.Arith.Fixpoint.Construction V (LO.Arith.FormalizedTerm.blueprint pL)

Equations

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

instance LO.Arith.FormalizedTerm.instStrongFiniteConstruction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : LO.Arith.Fixpoint.Construction.StrongFinite V (LO.Arith.FormalizedTerm.construction L)

Equations

• LO.Arith.FormalizedTerm.instStrongFiniteConstruction L = { strong_finite := ⋯ }

def LO.Arith.Language.IsUTerm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : V → Prop

Equations

• L.IsUTerm = (LO.Arith.FormalizedTerm.construction L).Fixpoint ![]

def LO.FirstOrder.Arith.LDef.isUTermDef (pL : LO.FirstOrder.Arith.LDef) : 𝚫₁.Semisentence 1

Equations

• pL.isUTermDef = (LO.Arith.FormalizedTerm.blueprint pL).fixpointDefΔ₁

theorem LO.Arith.Language.isUTerm_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Predicate L.IsUTerm via pL.isUTermDef

@[simp]

theorem LO.Arith.eval_isUTermDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (v : Fin 1 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val pL.isUTermDef) ↔ L.IsUTerm (v 0)

instance LO.Arith.Language.isUTerm_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Predicate L.IsUTerm

Equations

• ⋯ = ⋯

instance LO.Arith.isUTermDef_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : ℕ} (Γ : LO.SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Predicate L.IsUTerm

Equations

• ⋯ = ⋯

def LO.Arith.Language.IsUTermVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) (w : V) : Prop

Equations

• L.IsUTermVec n w = (n = LO.Arith.len w ∧ ∀ i < n, L.IsUTerm (LO.Arith.nth w i))

theorem LO.Arith.Language.IsUTermVec.lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {w : V} (h : L.IsUTermVec n w) : n = LO.Arith.len w

theorem LO.Arith.Language.IsUTermVec.nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {w : V} (h : L.IsUTermVec n w) {i : V} : i < n → L.IsUTerm (LO.Arith.nth w i)

@[simp]

theorem LO.Arith.Language.IsUTermVec.empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : L.IsUTermVec 0 0

@[simp]

theorem LO.Arith.Language.IsUTermVec.empty_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {v : V} : L.IsUTermVec 0 v ↔ v = 0

theorem LO.Arith.Language.IsUTermVec.two_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {v : V} : L.IsUTermVec 2 v ↔ ∃ (t₁ : V) (t₂ : V), L.IsUTerm t₁ ∧ L.IsUTerm t₂ ∧ v = ?[t₁, t₂]

@[simp]

theorem LO.Arith.Language.IsUTermVec.cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {w : V} {t : V} (h : L.IsUTermVec n w) (ht : L.IsUTerm t) : L.IsUTermVec (n + 1) (cons t w)

@[simp]

theorem LO.Arith.Language.IsUTermVec.cons₁_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t : V} : L.IsUTermVec 1 ?[t] ↔ L.IsUTerm t

@[simp]

theorem LO.Arith.Language.IsUTermVec.mkSeq₂_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t₁ : V} {t₂ : V} : L.IsUTermVec 2 ?[t₁, t₂] ↔ L.IsUTerm t₁ ∧ L.IsUTerm t₂

def LO.FirstOrder.Arith.LDef.isUTermVecDef (pL : LO.FirstOrder.Arith.LDef) : 𝚫₁.Semisentence 2

Equations

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

theorem LO.Arith.Language.isUTermVec_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation L.IsUTermVec via pL.isUTermVecDef

@[simp]

theorem LO.Arith.eval_isUTermVecDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val pL.isUTermVecDef) ↔ L.IsUTermVec (v 0) (v 1)

instance LO.Arith.Language.isUTermVecDef_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation L.IsUTermVec

Equations

• ⋯ = ⋯

instance LO.Arith.Language.isUTermVecDef_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : ℕ} (Γ : LO.SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Relation L.IsUTermVec

Equations

• ⋯ = ⋯

theorem LO.Arith.Language.IsUTerm.case_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t : V} : L.IsUTerm t ↔ (∃ (z : V), t = LO.Arith.qqBvar z) ∨ (∃ (x : V), t = LO.Arith.qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.Func k f ∧ L.IsUTermVec k v ∧ t = LO.Arith.qqFunc k f v

theorem LO.Arith.Language.IsUTerm.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t : V} : L.IsUTerm t → (∃ (z : V), t = LO.Arith.qqBvar z) ∨ (∃ (x : V), t = LO.Arith.qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.Func k f ∧ L.IsUTermVec k v ∧ t = LO.Arith.qqFunc k f v

Alias of the forward direction of LO.Arith.Language.IsUTerm.case_iff.

theorem LO.Arith.Language.IsUTerm.mk {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t : V} : ((∃ (z : V), t = LO.Arith.qqBvar z) ∨ (∃ (x : V), t = LO.Arith.qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.Func k f ∧ L.IsUTermVec k v ∧ t = LO.Arith.qqFunc k f v) → L.IsUTerm t

Alias of the reverse direction of LO.Arith.Language.IsUTerm.case_iff.

@[simp]

theorem LO.Arith.Language.IsUTerm.bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {z : V} : L.IsUTerm (LO.Arith.qqBvar z)

@[simp]

theorem LO.Arith.Language.IsUTerm.fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (x : V) : L.IsUTerm (LO.Arith.qqFvar x)

@[simp]

theorem LO.Arith.Language.IsUTerm.func_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {f : V} {v : V} : L.IsUTerm (LO.Arith.qqFunc k f v) ↔ L.Func k f ∧ L.IsUTermVec k v

theorem LO.Arith.Language.IsUTerm.func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {f : V} {v : V} (hkf : L.Func k f) (hv : L.IsUTermVec k v) : L.IsUTerm (LO.Arith.qqFunc k f v)

theorem LO.Arith.Language.IsUTerm.induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : LO.SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hbvar : ∀ (z : V), P (LO.Arith.qqBvar z)) (hfvar : ∀ (x : V), P (LO.Arith.qqFvar x)) (hfunc : ∀ (k f v : V), L.Func k f → L.IsUTermVec k v → (∀ i < k, P (LO.Arith.nth v i)) → P (LO.Arith.qqFunc k f v)) (t : V) : L.IsUTerm t → P t

structure LO.Arith.Language.TermRec.Blueprint (pL : LO.FirstOrder.Arith.LDef) (arity : ℕ) : Type

• bvar : 𝚺₁.Semisentence (arity + 2)
• fvar : 𝚺₁.Semisentence (arity + 2)
• func : 𝚺₁.Semisentence (arity + 5)

def LO.Arith.Language.TermRec.Blueprint.blueprint {arity : ℕ} {pL : LO.FirstOrder.Arith.LDef} (β : LO.Arith.Language.TermRec.Blueprint pL arity) : LO.Arith.Fixpoint.Blueprint arity

Equations

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

def LO.Arith.Language.TermRec.Blueprint.graph {arity : ℕ} {pL : LO.FirstOrder.Arith.LDef} (β : LO.Arith.Language.TermRec.Blueprint pL arity) : 𝚺₁.Semisentence (arity + 2)

Equations

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

def LO.Arith.Language.TermRec.Blueprint.result {arity : ℕ} {pL : LO.FirstOrder.Arith.LDef} (β : LO.Arith.Language.TermRec.Blueprint pL arity) : 𝚺₁.Semisentence (arity + 2)

Equations

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

def LO.Arith.Language.TermRec.Blueprint.resultVec {arity : ℕ} {pL : LO.FirstOrder.Arith.LDef} (β : LO.Arith.Language.TermRec.Blueprint pL arity) : 𝚺₁.Semisentence (arity + 3)

Equations

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

structure LO.Arith.Language.TermRec.Construction (V : Type u_1) [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} (L : LO.Arith.Language V) {k : ℕ} (φ : LO.Arith.Language.TermRec.Blueprint pL k) : Type u_1

• bvar : (Fin k → V) → V → V
• fvar : (Fin k → V) → V → V
• func : (Fin k → V) → V → V → V → V → V
• bvar_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ → V) => self.bvar (fun (x : Fin k) => v x.succ) (v 0)) φ.bvar
• fvar_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ → V) => self.fvar (fun (x : Fin k) => v x.succ) (v 0)) φ.fvar
• func_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ.succ.succ.succ → V) => self.func (fun (x : Fin k) => v x.succ.succ.succ.succ) (v 0) (v 1) (v 2) (v 3)) φ.func

theorem LO.Arith.Language.TermRec.Construction.bvar_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {k : ℕ} {φ : LO.Arith.Language.TermRec.Blueprint pL k} (self : LO.Arith.Language.TermRec.Construction V L φ) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ → V) => self.bvar (fun (x : Fin k) => v x.succ) (v 0)) φ.bvar

theorem LO.Arith.Language.TermRec.Construction.fvar_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {k : ℕ} {φ : LO.Arith.Language.TermRec.Blueprint pL k} (self : LO.Arith.Language.TermRec.Construction V L φ) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ → V) => self.fvar (fun (x : Fin k) => v x.succ) (v 0)) φ.fvar

theorem LO.Arith.Language.TermRec.Construction.func_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {k : ℕ} {φ : LO.Arith.Language.TermRec.Blueprint pL k} (self : LO.Arith.Language.TermRec.Construction V L φ) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ.succ.succ.succ → V) => self.func (fun (x : Fin k) => v x.succ.succ.succ.succ) (v 0) (v 1) (v 2) (v 3)) φ.func

def LO.Arith.Language.TermRec.Construction.Phi {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) (C : Set V) (pr : V) : Prop

Equations

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

theorem LO.Arith.Language.TermRec.Construction.seq_bound {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : V} {s : V} {m : V} (Ss : LO.Arith.Seq s) (hk : k = LO.Arith.lh s) (hs : ∀ (i z : V), ⟪i, z⟫ ∈ s → z < m) : s < exp ((k + m + 1) ^ 2)

@[simp]

theorem LO.Arith.Language.TermRec.Construction.cons_app_9 {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 9 = s 8

TODO: move

@[simp]

theorem LO.Arith.Language.TermRec.Construction.cons_app_10 {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 10 = s 9

@[simp]

theorem LO.Arith.Language.TermRec.Construction.cons_app_11 {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 11 = s 10

def LO.Arith.Language.TermRec.Construction.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) : LO.Arith.Fixpoint.Construction V β.blueprint

Equations

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

instance LO.Arith.Language.TermRec.Construction.instFiniteConstruction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) : LO.Arith.Fixpoint.Construction.Finite V c.construction

Equations

• c.instFiniteConstruction = { finite := ⋯ }

def LO.Arith.Language.TermRec.Construction.Graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) (x : V) (y : V) : Prop

Equations

• c.Graph param x y = c.construction.Fixpoint param ⟪x, y⟫

theorem LO.Arith.Language.TermRec.Construction.Graph.case_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} {c : LO.Arith.Language.TermRec.Construction V L β} {param : Fin arity → V} {t : V} {y : V} : c.Graph param t y ↔ L.IsUTerm t ∧ ((∃ (z : V), t = LO.Arith.qqBvar z ∧ y = c.bvar param z) ∨ (∃ (x : V), t = LO.Arith.qqFvar x ∧ y = c.fvar param x) ∨ ∃ (k : V) (f : V) (v : V) (w : V), (k = LO.Arith.len w ∧ ∀ i < k, c.Graph param (LO.Arith.nth v i) (LO.Arith.nth w i)) ∧ t = LO.Arith.qqFunc k f v ∧ y = c.func param k f v w)

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

@[simp]

theorem LO.Arith.Language.TermRec.Construction.eval_graphDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (v : Fin (arity + 2) → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val β.graph) ↔ c.Graph (fun (x : Fin arity) => v x.succ.succ) (v 0) (v 1)

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

Equations

• ⋯ = ⋯

instance LO.Arith.Language.TermRec.Construction.graph_definable₂ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) : { Γ := 𝚺, rank := 0 + 1 }-Relation c.Graph param

Equations

• ⋯ = ⋯

theorem LO.Arith.Language.TermRec.Construction.graph_dom_isUTerm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) {param : Fin arity → V} {t : V} {y : V} : c.Graph param t y → L.IsUTerm t

theorem LO.Arith.Language.TermRec.Construction.graph_bvar_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) {param : Fin arity → V} {y : V} {z : V} : c.Graph param (LO.Arith.qqBvar z) y ↔ y = c.bvar param z

theorem LO.Arith.Language.TermRec.Construction.graph_fvar_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) {param : Fin arity → V} {y : V} (x : V) : c.Graph param (LO.Arith.qqFvar x) y ↔ y = c.fvar param x

theorem LO.Arith.Language.TermRec.Construction.graph_func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) {param : Fin arity → V} {k : V} {f : V} {v : V} {w : V} (hkr : L.Func k f) (hv : L.IsUTermVec k v) (hkw : k = LO.Arith.len w) (hw : ∀ i < k, c.Graph param (LO.Arith.nth v i) (LO.Arith.nth w i)) : c.Graph param (LO.Arith.qqFunc k f v) (c.func param k f v w)

theorem LO.Arith.Language.TermRec.Construction.graph_func_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) {param : Fin arity → V} {k : V} {f : V} {v : V} {y : V} : c.Graph param (LO.Arith.qqFunc k f v) y → ∃ (w : V), (k = LO.Arith.len w ∧ ∀ i < k, c.Graph param (LO.Arith.nth v i) (LO.Arith.nth w i)) ∧ y = c.func param k f v w

theorem LO.Arith.Language.TermRec.Construction.graph_exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} {c : LO.Arith.Language.TermRec.Construction V L β} (param : Fin arity → V) {t : V} : L.IsUTerm t → ∃ (y : V), c.Graph param t y

theorem LO.Arith.Language.TermRec.Construction.graph_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} {c : LO.Arith.Language.TermRec.Construction V L β} (param : Fin arity → V) {t : V} {y₁ : V} {y₂ : V} : c.Graph param t y₁ → c.Graph param t y₂ → y₁ = y₂

theorem LO.Arith.Language.TermRec.Construction.graph_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) {t : V} (ht : L.IsUTerm t) : ∃! y : V, c.Graph param t y

theorem LO.Arith.Language.TermRec.Construction.graph_existsUnique_total {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) (t : V) : ∃! y : V, (L.IsUTerm t → c.Graph param t y) ∧ (¬L.IsUTerm t → y = 0)

def LO.Arith.Language.TermRec.Construction.result {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) (t : V) : V

Equations

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

def LO.Arith.Language.TermRec.Construction.result_prop {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) {t : V} (ht : L.IsUTerm t) : c.Graph param t (c.result param t)

Equations

• ⋯ = ⋯

def LO.Arith.Language.TermRec.Construction.result_prop_not {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) {t : V} (ht : ¬L.IsUTerm t) : c.result param t = 0

Equations

• ⋯ = ⋯

theorem LO.Arith.Language.TermRec.Construction.result_eq_of_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} {c : LO.Arith.Language.TermRec.Construction V L β} {param : Fin arity → V} {t : V} {y : V} (ht : L.IsUTerm t) (h : c.Graph param t y) : c.result param t = y

@[simp]

theorem LO.Arith.Language.TermRec.Construction.result_bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} {c : LO.Arith.Language.TermRec.Construction V L β} {param : Fin arity → V} (z : V) : c.result param (LO.Arith.qqBvar z) = c.bvar param z

@[simp]

theorem LO.Arith.Language.TermRec.Construction.result_fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} {c : LO.Arith.Language.TermRec.Construction V L β} {param : Fin arity → V} (x : V) : c.result param (LO.Arith.qqFvar x) = c.fvar param x

theorem LO.Arith.Language.TermRec.Construction.result_func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} {c : LO.Arith.Language.TermRec.Construction V L β} {param : Fin arity → V} {k : V} {f : V} {v : V} {w : V} (hkf : L.Func k f) (hv : L.IsUTermVec k v) (hkw : k = LO.Arith.len w) (hw : ∀ i < k, c.result param (LO.Arith.nth v i) = LO.Arith.nth w i) : c.result param (LO.Arith.qqFunc k f v) = c.func param k f v w

theorem LO.Arith.Language.TermRec.Construction.graph_existsUnique_vec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} {c : LO.Arith.Language.TermRec.Construction V L β} {param : Fin arity → V} {k : V} {w : V} (hw : L.IsUTermVec k w) : ∃! w' : V, k = LO.Arith.len w' ∧ ∀ i < k, c.Graph param (LO.Arith.nth w i) (LO.Arith.nth w' i)

theorem LO.Arith.Language.TermRec.Construction.graph_existsUnique_vec_total {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) (k : V) (w : V) : ∃! w' : V, (L.IsUTermVec k w → k = LO.Arith.len w' ∧ ∀ i < k, c.Graph param (LO.Arith.nth w i) (LO.Arith.nth w' i)) ∧ (¬L.IsUTermVec k w → w' = 0)

def LO.Arith.Language.TermRec.Construction.resultVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) (k : V) (w : V) : V

Equations

• c.resultVec param k w = Classical.choose! ⋯

@[simp]

theorem LO.Arith.Language.TermRec.Construction.resultVec_lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) {k : V} {w : V} (hw : L.IsUTermVec k w) : LO.Arith.len (c.resultVec param k w) = k

theorem LO.Arith.Language.TermRec.Construction.graph_of_mem_resultVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) {k : V} {w : V} (hw : L.IsUTermVec k w) {i : V} (hi : i < k) : c.Graph param (LO.Arith.nth w i) (LO.Arith.nth (c.resultVec param k w) i)

theorem LO.Arith.Language.TermRec.Construction.nth_resultVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) {k : V} {w : V} {i : V} (hw : L.IsUTermVec k w) (hi : i < k) : LO.Arith.nth (c.resultVec param k w) i = c.result param (LO.Arith.nth w i)

@[simp]

def LO.Arith.Language.TermRec.Construction.resultVec_of_not {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) {k : V} {w : V} (hw : ¬L.IsUTermVec k w) : c.resultVec param k w = 0

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Language.TermRec.Construction.resultVec_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) : c.resultVec param 0 0 = 0

theorem LO.Arith.Language.TermRec.Construction.resultVec_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (param : Fin arity → V) {k : V} {w : V} {t : V} (hw : L.IsUTermVec k w) (ht : L.IsUTerm t) : c.resultVec param (k + 1) (cons t w) = cons (c.result param t) (c.resultVec param k w)

@[simp]

theorem LO.Arith.Language.TermRec.Construction.result_func' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) {param : Fin arity → V} {k : V} {f : V} {v : V} (hkf : L.Func k f) (hv : L.IsUTermVec k v) : c.result param (LO.Arith.qqFunc k f v) = c.func param k f v (c.resultVec param k v)

theorem LO.Arith.Language.TermRec.Construction.result_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin arity.succ → V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)) β.result

@[simp]

theorem LO.Arith.Language.TermRec.Construction.result_graphDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (v : Fin (arity + 2) → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val β.result) ↔ v 0 = c.result (fun (x : Fin arity) => v x.succ.succ) (v 1)

theorem LO.Arith.Language.TermRec.Construction.resultVec_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin arity.succ.succ → V) => c.resultVec (fun (x : Fin arity) => v x.succ.succ) (v 0) (v 1)) β.resultVec

theorem LO.Arith.Language.TermRec.Construction.eval_resultVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : LO.Arith.Language.TermRec.Blueprint pL arity} (c : LO.Arith.Language.TermRec.Construction V L β) (v : Fin (arity + 3) → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val β.resultVec) ↔ v 0 = c.resultVec (fun (x : Fin arity) => v x.succ.succ.succ) (v 1) (v 2)

def LO.Arith.IsUTerm.BV.blueprint (pL : LO.FirstOrder.Arith.LDef) : LO.Arith.Language.TermRec.Blueprint pL 0

Equations

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

def LO.Arith.IsUTerm.BV.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} : LO.Arith.Language.TermRec.Construction V L (LO.Arith.IsUTerm.BV.blueprint pL)

Equations

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

def LO.Arith.Language.termBV {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (t : V) : V

Equations

• L.termBV t = (LO.Arith.IsUTerm.BV.construction L).result ![] t

def LO.Arith.Language.termBVVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (k : V) (v : V) : V

Equations

• L.termBVVec k v = (LO.Arith.IsUTerm.BV.construction L).resultVec ![] k v

@[simp]

theorem LO.Arith.Language.termBV_bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (z : V) : L.termBV (LO.Arith.qqBvar z) = z + 1

@[simp]

theorem LO.Arith.Language.termBV_fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (x : V) : L.termBV (LO.Arith.qqFvar x) = 0

@[simp]

theorem LO.Arith.Language.termBV_func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {f : V} {v : V} (hkf : L.Func k f) (hv : L.IsUTermVec k v) : L.termBV (LO.Arith.qqFunc k f v) = LO.Arith.listMax (L.termBVVec k v)

@[simp]

theorem LO.Arith.Language.len_termBVVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {v : V} (hv : L.IsUTermVec k v) : LO.Arith.len (L.termBVVec k v) = k

@[simp]

theorem LO.Arith.Language.nth_termBVVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {v : V} (hv : L.IsUTermVec k v) {i : V} (hi : i < k) : LO.Arith.nth (L.termBVVec k v) i = L.termBV (LO.Arith.nth v i)

@[simp]

theorem LO.Arith.Language.termBVVec_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : L.termBVVec 0 0 = 0

theorem LO.Arith.Language.termBVVec_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {t : V} {ts : V} (ht : L.IsUTerm t) (hts : L.IsUTermVec k ts) : L.termBVVec (k + 1) (cons t ts) = cons (L.termBV t) (L.termBVVec k ts)

def LO.FirstOrder.Arith.LDef.termBVDef (pL : LO.FirstOrder.Arith.LDef) : 𝚺₁.Semisentence 2

Equations

• pL.termBVDef = (LO.Arith.IsUTerm.BV.blueprint pL).result

def LO.FirstOrder.Arith.LDef.termBVVecDef (pL : LO.FirstOrder.Arith.LDef) : 𝚺₁.Semisentence 3

Equations

• pL.termBVVecDef = (LO.Arith.IsUTerm.BV.blueprint pL).resultVec

theorem LO.Arith.Language.termBV_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₁-Function₁ L.termBV via pL.termBVDef

instance LO.Arith.Language.termBV_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₁-Function₁ L.termBV

Equations

• ⋯ = ⋯

instance LO.Arith.Language.termBV_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {k : ℕ} : { Γ := Γ, rank := k + 1 }-Function₁ L.termBV

Equations

• ⋯ = ⋯

theorem LO.Arith.Language.termBVVec_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 2 → V) => L.termBVVec (v 0) (v 1)) pL.termBVVecDef

instance LO.Arith.Language.termBVVec_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₁-Function₂ L.termBVVec

Equations

• ⋯ = ⋯

instance LO.Arith.Language.termBVVec_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {i : ℕ} : { Γ := Γ, rank := i + 1 }-Function₂ L.termBVVec

Equations

• ⋯ = ⋯

def LO.Arith.Language.IsSemiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) (t : V) : Prop

Equations

• L.IsSemiterm n t = (L.IsUTerm t ∧ L.termBV t ≤ n)

def LO.Arith.Language.IsSemitermVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (k : V) (n : V) (v : V) : Prop

Equations

• L.IsSemitermVec k n v = (L.IsUTermVec k v ∧ ∀ i < k, L.termBV (LO.Arith.nth v i) ≤ n)

@[reducible, inline]

abbrev LO.Arith.Language.IsTerm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (t : V) : Prop

Equations

• L.IsTerm t = L.IsSemiterm 0 t

@[reducible, inline]

abbrev LO.Arith.Language.IsTermVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (k : V) (v : V) : Prop

Equations

• L.IsTermVec k v = L.IsSemitermVec k 0 v

theorem LO.Arith.Language.IsSemiterm.isUTerm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : V} (h : L.IsSemiterm n t) : L.IsUTerm t

theorem LO.Arith.Language.IsSemiterm.bv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : V} (h : L.IsSemiterm n t) : L.termBV t ≤ n

@[simp]

theorem LO.Arith.Language.IsSemitermVec.isUTerm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {v : V} (h : L.IsSemitermVec k n v) : L.IsUTermVec k v

theorem LO.Arith.Language.IsSemitermVec.bv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {v : V} (h : L.IsSemitermVec k n v) {i : V} (hi : i < k) : L.termBV (LO.Arith.nth v i) ≤ n

theorem LO.Arith.Language.IsSemitermVec.lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {v : V} (h : L.IsSemitermVec k n v) : LO.Arith.len v = k

theorem LO.Arith.Language.IsSemitermVec.nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {v : V} (h : L.IsSemitermVec k n v) {i : V} (hi : i < k) : L.IsSemiterm n (LO.Arith.nth v i)

theorem LO.Arith.Language.IsUTerm.isSemiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t : V} (h : L.IsUTerm t) : L.IsSemiterm (L.termBV t) t

theorem LO.Arith.Language.IsUTermVec.isSemitermVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {v : V} (h : L.IsUTermVec k v) : L.IsSemitermVec k (LO.Arith.listMax (L.termBVVec k v)) v

theorem LO.Arith.Language.IsSemitermVec.iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {v : V} : L.IsSemitermVec k n v ↔ LO.Arith.len v = k ∧ ∀ i < k, L.IsSemiterm n (LO.Arith.nth v i)

@[simp]

theorem LO.Arith.Language.IsSemiterm.bvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {z : V} : L.IsSemiterm n (LO.Arith.qqBvar z) ↔ z < n

@[simp]

theorem LO.Arith.Language.IsSemiterm.fvar {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) (x : V) : L.IsSemiterm n (LO.Arith.qqFvar x)

@[simp]

theorem LO.Arith.Language.IsSemiterm.func {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} {f : V} {v : V} : L.IsSemiterm n (LO.Arith.qqFunc k f v) ↔ L.Func k f ∧ L.IsSemitermVec k n v

@[simp]

theorem LO.Arith.Language.IsSemitermVec.empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) : L.IsSemitermVec 0 n 0

@[simp]

theorem LO.Arith.Language.IsSemitermVec.empty_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {v : V} {n : V} : L.IsSemitermVec 0 n v ↔ v = 0

@[simp]

theorem LO.Arith.Language.IsSemitermVec.cons_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {w : V} {t : V} : L.IsSemitermVec (k + 1) n (cons t w) ↔ L.IsSemiterm n t ∧ L.IsSemitermVec k n w

theorem LO.Arith.Language.SemitermVec.cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} {w : V} {t : V} (h : L.IsSemitermVec n m w) (ht : L.IsSemiterm m t) : L.IsSemitermVec (n + 1) m (cons t w)

@[simp]

theorem LO.Arith.Language.IsSemitermVec.singleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : V} : L.IsSemitermVec 1 n ?[t] ↔ L.IsSemiterm n t

@[simp]

theorem LO.Arith.Language.IsSemitermVec.doubleton {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t₁ : V} {t₂ : V} : L.IsSemitermVec 2 n ?[t₁, t₂] ↔ L.IsSemiterm n t₁ ∧ L.IsSemiterm n t₂

def LO.FirstOrder.Arith.LDef.isSemitermDef (pL : LO.FirstOrder.Arith.LDef) : 𝚫₁.Semisentence 2

Equations

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

theorem LO.Arith.Language.isSemiterm_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation L.IsSemiterm via pL.isSemitermDef

instance LO.Arith.Language.isSemiterm_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation L.IsSemiterm

Equations

• ⋯ = ⋯

instance LO.Arith.Language.isSemiterm_defined' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Relation L.IsSemiterm

Equations

• ⋯ = ⋯

def LO.FirstOrder.Arith.LDef.isSemitermVecDef (pL : LO.FirstOrder.Arith.LDef) : 𝚫₁.Semisentence 3

Equations

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

theorem LO.Arith.Language.isSemitermVec_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation₃ L.IsSemitermVec via pL.isSemitermVecDef

instance LO.Arith.Language.isSemitermVec_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation₃ L.IsSemitermVec

Equations

• ⋯ = ⋯

instance LO.Arith.Language.isSemitermVec_defined' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Relation₃ L.IsSemitermVec

Equations

• ⋯ = ⋯

theorem LO.Arith.Language.IsSemiterm.case_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : V} : L.IsSemiterm n t ↔ (∃ z < n, t = LO.Arith.qqBvar z) ∨ (∃ (x : V), t = LO.Arith.qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.Func k f ∧ L.IsSemitermVec k n v ∧ t = LO.Arith.qqFunc k f v

theorem LO.Arith.Language.IsSemiterm.mk {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : V} : ((∃ z < n, t = LO.Arith.qqBvar z) ∨ (∃ (x : V), t = LO.Arith.qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.Func k f ∧ L.IsSemitermVec k n v ∧ t = LO.Arith.qqFunc k f v) → L.IsSemiterm n t

Alias of the reverse direction of LO.Arith.Language.IsSemiterm.case_iff.

theorem LO.Arith.Language.IsSemiterm.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : V} : L.IsSemiterm n t → (∃ z < n, t = LO.Arith.qqBvar z) ∨ (∃ (x : V), t = LO.Arith.qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.Func k f ∧ L.IsSemitermVec k n v ∧ t = LO.Arith.qqFunc k f v

Alias of the forward direction of LO.Arith.Language.IsSemiterm.case_iff.

theorem LO.Arith.Language.IsSemiterm.induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (Γ : LO.SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hbvar : ∀ z < n, P (LO.Arith.qqBvar z)) (hfvar : ∀ (x : V), P (LO.Arith.qqFvar x)) (hfunc : ∀ (k f v : V), L.Func k f → L.IsSemitermVec k n v → (∀ i < k, P (LO.Arith.nth v i)) → P (LO.Arith.qqFunc k f v)) (t : V) : L.IsSemiterm n t → P t

@[simp]

theorem LO.Arith.Language.IsSemitermVec.nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (k : V) : L.IsSemitermVec 0 k 0

@[simp]

theorem LO.Arith.Language.IsSemitermVec.cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {n : V} {w : V} {t : V} (h : L.IsSemitermVec n k w) (ht : L.IsSemiterm k t) : L.IsSemitermVec (n + 1) k (cons t w)