def LO.Arith.TermSubst.blueprint (pL : LO.FirstOrder.Arith.LDef) : LO.Arith.Language.TermRec.Blueprint pL 1

Equations

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

def LO.Arith.TermSubst.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.TermSubst.blueprint pL)

Equations

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

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

Equations

• L.termSubst w t = (LO.Arith.TermSubst.construction L).result ![w] t

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

Equations

• L.termSubstVec k w v = (LO.Arith.TermSubst.construction L).resultVec ![w] k v

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

def LO.FirstOrder.Arith.LDef.termSubstVecDef (pL : LO.FirstOrder.Arith.LDef) : 𝚺₁.Semisentence 4

Equations

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

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.Language.termSubst_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.termSubst

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.Language.termSubstVec_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.termSubstVec

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.len_termSubstVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {k : V} {ts : V} (hts : L.IsUTermVec k ts) : LO.Arith.len (L.termSubstVec k w ts) = k

@[simp]

theorem LO.Arith.nth_termSubstVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {k : V} {ts : V} {i : V} (hts : L.IsUTermVec k ts) (hi : i < k) : LO.Arith.nth (L.termSubstVec k w ts) i = L.termSubst w (LO.Arith.nth ts i)

@[simp]

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

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

@[simp]

theorem LO.Arith.termSubstVec_cons₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {t : V} (ht : L.IsUTerm t) : L.termSubstVec 1 w ?[t] = ?[L.termSubst w t]

@[simp]

theorem LO.Arith.termSubstVec_cons₂ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {t₁ : V} {t₂ : V} (ht₁ : L.IsUTerm t₁) (ht₂ : L.IsUTerm t₂) : L.termSubstVec 2 w ?[t₁, t₂] = ?[L.termSubst w t₁, L.termSubst w t₂]

@[simp]

theorem LO.Arith.Language.IsSemitermVec.termSubst {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} (hw : L.IsSemitermVec n m w) (ht : L.IsSemiterm n t) : L.IsSemiterm m (L.termSubst w t)

@[simp]

theorem LO.Arith.Language.IsUTermVec.termSubst {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} (hw : L.IsUTermVec n w) (ht : L.IsSemiterm n t) : L.IsUTerm (L.termSubst w t)

@[simp]

theorem LO.Arith.Language.IsSemitermVec.termSubstVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {k : V} {n : V} {m : V} {v : V} (hw : L.IsSemitermVec n m w) (hv : L.IsSemitermVec k n v) : L.IsSemitermVec k m (L.termSubstVec k w v)

@[simp]

theorem LO.Arith.substs_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t : V} (ht : L.IsSemiterm 0 t) : L.termSubst 0 t = t

theorem LO.Arith.termSubst_termSubst {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {l : V} {n : V} {w : V} {v : V} {t : V} (hv : L.IsSemitermVec l n v) (ht : L.IsSemiterm l t) : L.termSubst w (L.termSubst v t) = L.termSubst (L.termSubstVec l w v) t

theorem LO.Arith.termSubst_eq_self {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} (ht : L.IsSemiterm n t) (H : ∀ i < n, LO.Arith.nth w i = LO.Arith.qqBvar i) : L.termSubst w t = t

def LO.Arith.TermShift.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.TermShift.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.TermShift.blueprint pL)

Equations

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

def LO.Arith.Language.termShift {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.termShift t = (LO.Arith.TermShift.construction L).result ![] t

def LO.Arith.Language.termShiftVec {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.termShiftVec k v = (LO.Arith.TermShift.construction L).resultVec ![] k v

@[simp]

theorem LO.Arith.Language.termShift_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.termShift (LO.Arith.qqBvar z) = LO.Arith.qqBvar z

@[simp]

theorem LO.Arith.Language.termShift_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.termShift (LO.Arith.qqFvar x) = LO.Arith.qqFvar (x + 1)

@[simp]

theorem LO.Arith.Language.termShift_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.termShift (LO.Arith.qqFunc k f v) = LO.Arith.qqFunc k f (L.termShiftVec k v)

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

Equations

• pL.termShiftDef = (LO.Arith.TermShift.blueprint pL).result

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

Equations

• pL.termShiftVecDef = (LO.Arith.TermShift.blueprint pL).resultVec

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.Language.termShift_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.termShift

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.Language.termShiftVec_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.termShiftVec

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.len_termShiftVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {ts : V} (hts : L.IsUTermVec k ts) : LO.Arith.len (L.termShiftVec k ts) = k

@[simp]

theorem LO.Arith.nth_termShiftVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {ts : V} {i : V} (hts : L.IsUTermVec k ts) (hi : i < k) : LO.Arith.nth (L.termShiftVec k ts) i = L.termShift (LO.Arith.nth ts i)

@[simp]

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

theorem LO.Arith.termShiftVec_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.termShiftVec (k + 1) (cons t ts) = cons (L.termShift t) (L.termShiftVec k ts)

@[simp]

theorem LO.Arith.termShiftVec_cons₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t₁ : V} (ht₁ : L.IsUTerm t₁) : L.termShiftVec 1 ?[t₁] = ?[L.termShift t₁]

@[simp]

theorem LO.Arith.termShiftVec_cons₂ {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} (ht₁ : L.IsUTerm t₁) (ht₂ : L.IsUTerm t₂) : L.termShiftVec 2 ?[t₁, t₂] = ?[L.termShift t₁, L.termShift t₂]

@[simp]

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

@[simp]

theorem LO.Arith.Language.IsSemiterm.termShift {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} (ht : L.IsSemiterm n t) : L.IsSemiterm n (L.termShift t)

@[simp]

theorem LO.Arith.Language.IsUTermVec.termShiftVec {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) : L.IsUTermVec k (L.termShiftVec k v)

@[simp]

theorem LO.Arith.Language.IsSemitermVec.termShiftVec {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} (hv : L.IsSemitermVec k n v) : L.IsSemitermVec k n (L.termShiftVec k v)

@[simp]

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

@[simp]

theorem LO.Arith.Language.IsUTermVec.termBVVectermShiftVec {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) : L.termBVVec k (L.termShiftVec k v) = L.termBVVec k v

def LO.Arith.TermBShift.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.TermBShift.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.TermBShift.blueprint pL)

Equations

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

def LO.Arith.Language.termBShift {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.termBShift t = (LO.Arith.TermBShift.construction L).result ![] t

def LO.Arith.Language.termBShiftVec {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.termBShiftVec k v = (LO.Arith.TermBShift.construction L).resultVec ![] k v

@[simp]

theorem LO.Arith.Language.termBShift_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.termBShift (LO.Arith.qqBvar z) = LO.Arith.qqBvar (z + 1)

@[simp]

theorem LO.Arith.Language.termBShift_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.termBShift (LO.Arith.qqFvar x) = LO.Arith.qqFvar x

@[simp]

theorem LO.Arith.Language.termBShift_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.termBShift (LO.Arith.qqFunc k f v) = LO.Arith.qqFunc k f (L.termBShiftVec k v)

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

Equations

• pL.termBShiftDef = (LO.Arith.TermBShift.blueprint pL).result

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

Equations

• pL.termBShiftVecDef = (LO.Arith.TermBShift.blueprint pL).resultVec

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.Language.termBShift_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.termBShift

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

instance LO.Arith.Language.termBShiftVec_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.termBShiftVec

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.len_termBShiftVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {ts : V} (hts : L.IsUTermVec k ts) : LO.Arith.len (L.termBShiftVec k ts) = k

@[simp]

theorem LO.Arith.nth_termBShiftVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {ts : V} {i : V} (hts : L.IsUTermVec k ts) (hi : i < k) : LO.Arith.nth (L.termBShiftVec k ts) i = L.termBShift (LO.Arith.nth ts i)

@[simp]

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

theorem LO.Arith.termBShiftVec_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.termBShiftVec (k + 1) (cons t ts) = cons (L.termBShift t) (L.termBShiftVec k ts)

@[simp]

theorem LO.Arith.termBShiftVec_cons₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {t₁ : V} (ht₁ : L.IsUTerm t₁) : L.termBShiftVec 1 ?[t₁] = ?[L.termBShift t₁]

@[simp]

theorem LO.Arith.termBShiftVec_cons₂ {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} (ht₁ : L.IsUTerm t₁) (ht₂ : L.IsUTerm t₂) : L.termBShiftVec 2 ?[t₁, t₂] = ?[L.termBShift t₁, L.termBShift t₂]

@[simp]

theorem LO.Arith.Language.IsSemiterm.termBShift {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} (ht : L.IsSemiterm n t) : L.IsSemiterm (n + 1) (L.termBShift t)

@[simp]

theorem LO.Arith.Language.IsSemitermVec.termBShiftVec {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} (hv : L.IsSemitermVec k n v) : L.IsSemitermVec k (n + 1) (L.termBShiftVec k v)

theorem LO.Arith.termBShift_termShift {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} (ht : L.IsSemiterm n t) : L.termBShift (L.termShift t) = L.termShift (L.termBShift t)

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

Equations

• L.qVec w = cons (LO.Arith.qqBvar 0) (L.termBShiftVec (LO.Arith.len w) w)

@[simp]

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

theorem LO.Arith.Language.IsSemitermVec.qVec {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} (h : L.IsSemitermVec k n w) : L.IsSemitermVec (k + 1) (n + 1) (L.qVec w)

theorem LO.Arith.substs_cons_bShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {u : V} {t : V} {w : V} (ht : L.IsSemiterm n t) : L.termSubst (cons u w) (L.termBShift t) = L.termSubst w t

theorem LO.Arith.termShift_termSubsts {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} (ht : L.IsSemiterm n t) (hw : L.IsSemitermVec n m w) : L.termShift (L.termSubst w t) = L.termSubst (L.termShiftVec n w) (L.termShift t)

theorem LO.Arith.bShift_substs {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} (ht : L.IsSemiterm n t) (hw : L.IsSemitermVec n m w) : L.termBShift (L.termSubst w t) = L.termSubst (L.termBShiftVec n w) t

theorem LO.Arith.substs_qVec_bShift {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} {m : V} {w : V} (ht : L.IsSemiterm n t) (hw : L.IsSemitermVec n m w) : L.termSubst (L.qVec w) (L.termBShift t) = L.termBShift (L.termSubst w t)

theorem LO.Arith.termSubstVec_qVec_qVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {v : V} {w : V} {l : V} {n : V} {m : V} (hv : L.IsSemitermVec l n v) (hw : L.IsSemitermVec n m w) : L.termSubstVec (l + 1) (L.qVec w) (L.qVec v) = L.qVec (L.termSubstVec l w v)

theorem LO.Arith.termShift_qVec {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} (hw : L.IsSemitermVec n m w) : L.termShiftVec (n + 1) (L.qVec w) = L.qVec (L.termShiftVec n w)

def LO.Arith.Language.IsTermFVFree {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.IsTermFVFree n t = (L.IsSemiterm n t ∧ L.termShift t = t)

@[simp]

theorem LO.Arith.Language.IsTermFVFree.bvar {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.IsTermFVFree n (LO.Arith.qqBvar x) ↔ x < n

@[simp]

theorem LO.Arith.Language.IsTermFVFree.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.IsTermFVFree n (LO.Arith.qqFvar x)

def LO.Arith.Formalized.zero : ℕ

Equations

• 𝟎 = LO.Arith.qqFunc 0 LO.Arith.Formalized.zeroIndex 0

def LO.Arith.Formalized.one : ℕ

Equations

• 𝟏 = LO.Arith.qqFunc 0 LO.Arith.Formalized.oneIndex 0

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

Equations

• x ^+ y = LO.Arith.qqFunc 2 ↑LO.Arith.Formalized.addIndex ?[x, y]

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

Equations

• x ^* y = LO.Arith.qqFunc 2 ↑LO.Arith.Formalized.mulIndex ?[x, y]

def LO.Arith.Formalized.«term𝟎» : Lean.ParserDescr

Equations

• LO.Arith.Formalized.«term𝟎» = Lean.ParserDescr.node `LO.Arith.Formalized.term𝟎 1024 (Lean.ParserDescr.symbol "𝟎")

def LO.Arith.Formalized.«term𝟏» : Lean.ParserDescr

Equations

• LO.Arith.Formalized.«term𝟏» = Lean.ParserDescr.node `LO.Arith.Formalized.term𝟏 1024 (Lean.ParserDescr.symbol "𝟏")

def LO.Arith.Formalized.«term_^+_» : Lean.TrailingParserDescr

Equations

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

def LO.Arith.Formalized.«term_^*_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arith.qqAddDef : 𝚺₁.Semisentence 3

Equations

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

def LO.FirstOrder.Arith.qqMulDef : 𝚺₁.Semisentence 3

Equations

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

theorem LO.Arith.Formalized.qqAdd_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ LO.Arith.Formalized.qqAdd via LO.FirstOrder.Arith.qqAddDef

theorem LO.Arith.Formalized.qqMul_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ LO.Arith.Formalized.qqMul via LO.FirstOrder.Arith.qqMulDef

instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqAdd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqAdd

Equations

• ⋯ = ⋯

instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqMul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqMul

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Formalized.eval_qqAddDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqAddDef) ↔ v 0 = v 1 ^+ v 2

@[simp]

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

@[simp]

theorem LO.Arith.Formalized.lt_qqAdd_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) : x < x ^+ y

@[simp]

theorem LO.Arith.Formalized.lt_qqAdd_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) : y < x ^+ y

@[simp]

theorem LO.Arith.Formalized.lt_qqMul_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) : x < x ^* y

@[simp]

theorem LO.Arith.Formalized.lt_qqMul_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) : y < x ^* y

theorem LO.Arith.Formalized.qqFunc_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : ℕ) (f : ℕ) (v : ℕ) : ↑(LO.Arith.qqFunc k f v) = LO.Arith.qqFunc ↑k ↑f ↑v

@[simp]

theorem LO.Arith.Formalized.zero_semiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} : ⌜ℒₒᵣ⌝.IsSemiterm n ↑𝟎

@[simp]

theorem LO.Arith.Formalized.one_semiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} : ⌜ℒₒᵣ⌝.IsSemiterm n ↑𝟏

def LO.Arith.Formalized.Numeral.blueprint : LO.Arith.PR.Blueprint 0

Equations

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

def LO.Arith.Formalized.Numeral.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.PR.Construction V LO.Arith.Formalized.Numeral.blueprint

Equations

• LO.Arith.Formalized.Numeral.construction = { zero := fun (x : Fin 0 → V) => ↑𝟏, succ := fun (x : Fin 0 → V) (x t : V) => t ^+ ↑𝟏, zero_defined := ⋯, succ_defined := ⋯ }

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

Equations

• LO.Arith.Formalized.Numeral.numeralAux x = LO.Arith.Formalized.Numeral.construction.result ![] x

@[simp]

theorem LO.Arith.Formalized.Numeral.numeralAux_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.Formalized.Numeral.numeralAux 0 = ↑𝟏

@[simp]

theorem LO.Arith.Formalized.Numeral.numeralAux_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : LO.Arith.Formalized.Numeral.numeralAux (x + 1) = LO.Arith.Formalized.Numeral.numeralAux x ^+ ↑𝟏

def LO.Arith.Formalized.Numeral.numeralAuxDef : 𝚺₁.Semisentence 2

Equations

• LO.Arith.Formalized.Numeral.numeralAuxDef = LO.Arith.Formalized.Numeral.blueprint.resultDef

theorem LO.Arith.Formalized.Numeral.numeralAux_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.Formalized.Numeral.numeralAux via LO.Arith.Formalized.Numeral.numeralAuxDef

@[simp]

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

instance LO.Arith.Formalized.Numeral.seqExp_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : { Γ := 𝚺, rank := 0 + 1 }-Function₁ LO.Arith.Formalized.Numeral.numeralAux

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Formalized.Numeral.lt_numeralAux_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) : n < LO.Arith.Formalized.Numeral.numeralAux n

@[simp]

theorem LO.Arith.Formalized.Numeral.numeralAux_semiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) (x : V) : ⌜ℒₒᵣ⌝.IsSemiterm n (LO.Arith.Formalized.Numeral.numeralAux x)

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

Equations

• LO.Arith.Formalized.numeral x = if x = 0 then ↑𝟎 else LO.Arith.Formalized.Numeral.numeralAux (x - 1)

@[simp]

theorem LO.Arith.Formalized.numeral_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.Formalized.numeral 0 = ↑𝟎

@[simp]

theorem LO.Arith.Formalized.numeral_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.Formalized.numeral 1 = ↑𝟏

@[simp]

theorem LO.Arith.Formalized.numeral_add_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} : LO.Arith.Formalized.numeral (n + 1 + 1) = LO.Arith.Formalized.numeral (n + 1) ^+ ↑𝟏

theorem LO.Arith.Formalized.numeral_succ_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (pos : 0 < n) : LO.Arith.Formalized.numeral (n + 1) = LO.Arith.Formalized.numeral n ^+ ↑𝟏

@[simp]

theorem LO.Arith.Formalized.numeral_semiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) (x : V) : ⌜ℒₒᵣ⌝.IsSemiterm n (LO.Arith.Formalized.numeral x)

@[simp]

theorem LO.Arith.Formalized.numeral_uterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : ⌜ℒₒᵣ⌝.IsUTerm (LO.Arith.Formalized.numeral x)

@[simp]

theorem LO.Arith.Formalized.le_numeral_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) : n ≤ LO.Arith.Formalized.numeral n

def LO.FirstOrder.Arith.numeralDef : 𝚺₁.Semisentence 2

Equations

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

theorem LO.Arith.Formalized.numeral_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.Formalized.numeral via LO.FirstOrder.Arith.numeralDef

@[simp]

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

instance LO.Arith.Formalized.numeral_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.Formalized.numeral

Equations

• ⋯ = ⋯

instance LO.Arith.Formalized.numeral_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.Formalized.numeral

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Formalized.numeral_substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} {w : V} (hw : ⌜ℒₒᵣ⌝.IsSemitermVec n m w) (x : V) : ⌜ℒₒᵣ⌝.termSubst w (LO.Arith.Formalized.numeral x) = LO.Arith.Formalized.numeral x

@[simp]

theorem LO.Arith.Formalized.numeral_shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : ⌜ℒₒᵣ⌝.termShift (LO.Arith.Formalized.numeral x) = LO.Arith.Formalized.numeral x

@[simp]

theorem LO.Arith.Formalized.numeral_bShift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : ⌜ℒₒᵣ⌝.termBShift (LO.Arith.Formalized.numeral x) = LO.Arith.Formalized.numeral x