Basic

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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 ⊧ₘ* 𝐈Sg1] (z : V) : z < qqBvar z

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LO.Arith.nth_lt_qqFunc_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {z z' : V} : qqBvar z = qqBvar z' ↔ z = z'

@[simp]

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

@[simp]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

def LO.FirstOrder.Arith.qqFvarDef : Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

def LO.FirstOrder.Arith.qqFuncDef : Sg0.Semisentence 4

Imported declaration from the Incompleteness formalization.

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 ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₃ qqFunc via FirstOrder.Arith.qqFuncDef

@[simp]

theorem LO.Arith.eval_qqFuncDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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 ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) (C : Set V) (t : V) : Prop

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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 ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Fixpoint.Construction V (blueprint pL)

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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 ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : V → Prop

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

theorem LO.Arith.eval_isUTermDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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 ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : FirstOrder.Arith.Dlt1-Predicate L.IsUTerm

instance LO.Arith.isUTermDef_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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 ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n w : V) : Prop

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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) : Dlt1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

theorem LO.Arith.eval_isUTermVecDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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 ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : FirstOrder.Arith.Dlt1-Relation L.IsUTermVec

instance LO.Arith.Language.isUTermVecDef_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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

Imported declaration from the Incompleteness formalization.

• bvar : FirstOrder.Arith.Sg1.Semisentence (arity + 2)

  Imported declaration from the Incompleteness formalization.

• fvar : FirstOrder.Arith.Sg1.Semisentence (arity + 2)

  Imported declaration from the Incompleteness formalization.

• func : FirstOrder.Arith.Sg1.Semisentence (arity + 5)

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

• bvar : (Fin k → V) → V → V

  Imported declaration from the Incompleteness formalization.

• fvar : (Fin k → V) → V → V

  Imported declaration from the Incompleteness formalization.

• func : (Fin k → V) → V → V → V → V → V

  Imported declaration from the Incompleteness formalization.

• 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 ⊧ₘ* 𝐈Sg1] {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

Imported declaration from the Incompleteness formalization.

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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {arity : ℕ} {β : Blueprint pL arity} (c : Construction V L β) : Fixpoint.Construction V β.blueprint

Imported declaration from the Incompleteness formalization.

Equations

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

instance LO.Arith.Language.TermRec.Construction.instFiniteConstruction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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

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

theorem LO.Arith.Language.TermRec.Construction.graph_dom_isUTerm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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)

noncomputable def LO.Arith.Language.TermRec.Construction.result {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.Language.TermRec.Construction.result_prop {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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)

Imported declaration from the Incompleteness formalization.

theorem LO.Arith.Language.TermRec.Construction.result_prop_not {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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

Imported declaration from the Incompleteness formalization.

theorem LO.Arith.Language.TermRec.Construction.result_eq_of_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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)

noncomputable def LO.Arith.Language.TermRec.Construction.resultVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Arith.Language.TermRec.Construction.resultVec_lh {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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]

theorem LO.Arith.Language.TermRec.Construction.resultVec_of_not {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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

Imported declaration from the Incompleteness formalization.

@[simp]

theorem LO.Arith.Language.TermRec.Construction.resultVec_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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

theorem LO.Arith.Language.TermRec.Construction.result_graphDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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) : Sg1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

instance LO.Arith.Language.termBVVec_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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 ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n t : V) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (t : V) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• L.IsTerm t = L.IsSemiterm 0 t

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.Language.IsSemiterm.isUTerm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n t : V} (h : L.IsSemiterm n t) : L.termBV t ≤ n

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

theorem LO.Arith.Language.IsSemitermVec.empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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) : Dlt1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

instance LO.Arith.Language.isSemiterm_defined' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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) : Dlt1.Semisentence 3

Imported declaration from the Incompleteness formalization.

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

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

instance LO.Arith.Language.isSemitermVec_defined' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (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 ⊧ₘ* 𝐈Sg1] {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.mk {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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.case {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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.induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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 ⊧ₘ* 𝐈Sg1] {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)