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

Equations

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

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

Equations

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

def LO.Arith.qqFunc {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k f 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (z : V) : z < qqBvar z

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Arith.qqFunc_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k f v k' f' w : V} : qqFunc k f v = 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ qqBvar via FirstOrder.Arith.qqBvarDef

@[simp]

theorem LO.Arith.eval_qqBvarDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqBvarDef) ↔ v 0 = 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ qqFvar via FirstOrder.Arith.qqFvarDef

@[simp]

theorem LO.Arith.eval_qqFvarDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqFvarDef) ↔ v 0 = 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₃ qqFunc via FirstOrder.Arith.qqFuncDef

@[simp]

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

def LO.Arith.FormalizedTerm.Phi {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : 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 : FirstOrder.Arith.LDef) : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Fixpoint.Construction V (blueprint pL)

Equations

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

Instances For

• LO.Arith.FormalizedTerm.instStrongFiniteConstruction

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

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

Equations

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

Instances For

• LO.Arith.Language.isUTerm_definable
• LO.Arith.isUTermDef_definable'

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

Equations

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

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

@[simp]

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

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

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

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

Equations

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

Instances For

• LO.Arith.Language.isUTermVecDef_definable
• LO.Arith.Language.isUTermVecDef_definable'

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

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

@[simp]

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

@[simp]

theorem LO.Arith.Language.IsUTermVec.empty_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n w t : V} (h : L.IsUTermVec n w) (ht : L.IsUTerm t) : L.IsUTermVec (n + 1) (Cons.cons t w)

@[simp]

theorem LO.Arith.Language.IsUTermVec.cons₁_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {t₁ t₂ : V} : L.IsUTermVec 2 ?[t₁, t₂] ↔ L.IsUTerm t₁ ∧ L.IsUTerm t₂

def LO.FirstOrder.Arith.LDef.isUTermVecDef (pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation L.IsUTermVec via pL.isUTermVecDef

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

structure LO.Arith.Language.TermRec.Blueprint (pL : 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 : FirstOrder.Arith.LDef} (β : Blueprint pL arity) : 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 : FirstOrder.Arith.LDef} (β : 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 : FirstOrder.Arith.LDef} (β : 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 : FirstOrder.Arith.LDef} (β : 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) [ORingStruc V] {pL : FirstOrder.Arith.LDef} (L : Arith.Language V) {k : ℕ} (φ : 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 : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (k + 1) → V) => self.bvar (fun (x : Fin k) => v x.succ) (v 0)) φ.bvar
• fvar_defined : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (k + 1) → V) => self.fvar (fun (x : Fin k) => v x.succ) (v 0)) φ.fvar
• func_defined : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (k + 1 + 1 + 1 + 1) → 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k s m : V} (Ss : Seq s) (hk : k = 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) : Fixpoint.Construction V β.blueprint

Equations

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

Instances For

• LO.Arith.Language.TermRec.Construction.instFiniteConstruction

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

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

Equations

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

Instances For

• LO.Arith.Language.TermRec.Construction.graph_definable₂

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

theorem LO.Arith.Language.TermRec.Construction.graph_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) : FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin (arity + 1 + 1) → 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) (v : Fin (arity + 2) → V) : V ⊧/v (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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) : 𝚺₁.Boldface fun (v : Fin (arity + 1 + 1) → V) => 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) (param : Fin arity → V) : { Γ := 𝚺, rank := 0 + 1 }-Relation c.Graph param

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

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

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

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

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

theorem LO.Arith.Language.TermRec.Construction.graph_exists {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} {c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} {c : Construction V L β} (param : Fin arity → V) {t y₁ 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} {c : Construction V L β} {param : Fin arity → V} {t 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} {c : Construction V L β} {param : Fin arity → V} (z : V) : c.result param (qqBvar z) = c.bvar param z

@[simp]

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

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

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

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

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

Equations

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

@[simp]

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

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

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

@[simp]

def LO.Arith.Language.TermRec.Construction.resultVec_of_not {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) (param : Fin arity → V) {k 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) (param : Fin arity → V) {k w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) {param : Fin arity → V} {k f v : V} (hkf : L.Func k f) (hv : L.IsUTermVec k v) : c.result param (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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1) → 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) (v : Fin (arity + 2) → V) : V ⊧/v (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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1 + 1) → 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) (v : Fin (arity + 3) → V) : V ⊧/v (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 : FirstOrder.Arith.LDef) : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} : Language.TermRec.Construction V L (blueprint pL)

Equations

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

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

Equations

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

Instances For

• LO.Arith.Language.termBV_definable
• LO.Arith.Language.termBV_definable'

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

Equations

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

Instances For

• LO.Arith.Language.termBVVec_definable
• LO.Arith.Language.termBVVec_definable'

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LO.Arith.Language.termBVVec_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k t 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 : LDef) : 𝚺₁.Semisentence 2

Equations

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

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

Equations

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

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

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

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

theorem LO.Arith.Language.termBVVec_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₁-Function₂ L.termBVVec

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

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

Equations

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

Instances For

• LO.Arith.Language.isSemiterm_definable
• LO.Arith.Language.isSemiterm_defined'

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

Equations

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

Instances For

• LO.Arith.Language.isSemitermVec_definable
• LO.Arith.Language.isSemitermVec_defined'

@[reducible, inline]

abbrev LO.Arith.Language.IsTerm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (k v : V) : Prop

Equations

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

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

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

@[simp]

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

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

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

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

theorem LO.Arith.Language.IsUTerm.isSemiterm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k v : V} (h : L.IsUTermVec k v) : L.IsSemitermVec k (listMax (L.termBVVec k v)) v

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Arith.Language.IsSemitermVec.empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {v n : V} : L.IsSemitermVec 0 n v ↔ v = 0

@[simp]

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

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Arith.LDef.isSemitermDef (pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation L.IsSemiterm via pL.isSemitermDef

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

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

def LO.FirstOrder.Arith.LDef.isSemitermVecDef (pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation₃ L.IsSemitermVec via pL.isSemitermVecDef

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

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

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

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

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

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

@[simp]

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

@[simp]

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