Documentation

Arithmetization.ISigmaOne.Metamath.Term.Functions

source
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.
source
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.
source
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
Instances For
source
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
Instances For
source
@[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
source
@[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
source
@[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)
source
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.
source
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.
source
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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
@[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
source
@[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)
source
@[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
source
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)
source
@[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]
source
@[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₂]
source
@[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)
source
@[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)
source
@[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)
source
@[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
source
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
source
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
source
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.
source
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.
source
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
Instances For
source
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
Instances For
source
@[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
source
@[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)
source
@[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)
source
def LO.FirstOrder.Arith.LDef.termShiftDef (pL : LO.FirstOrder.Arith.LDef) :
𝚺₁.Semisentence 2
Equations
source
def LO.FirstOrder.Arith.LDef.termShiftVecDef (pL : LO.FirstOrder.Arith.LDef) :
𝚺₁.Semisentence 3
Equations
source
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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
@[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
source
@[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)
source
@[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
source
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)
source
@[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₁]
source
@[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₂]
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[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
source
@[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
source
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.
source
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.
source
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
Instances For
source
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
Instances For
source
@[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)
source
@[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
source
@[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)
source
def LO.FirstOrder.Arith.LDef.termBShiftDef (pL : LO.FirstOrder.Arith.LDef) :
𝚺₁.Semisentence 2
Equations
source
def LO.FirstOrder.Arith.LDef.termBShiftVecDef (pL : LO.FirstOrder.Arith.LDef) :
𝚺₁.Semisentence 3
Equations
source
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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
@[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
source
@[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)
source
@[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
source
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)
source
@[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₁]
source
@[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₂]
source
@[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)
source
@[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)
source
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)
source
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
Instances For
source
@[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
source
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)
source
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
source
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)
source
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
source
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)
source
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)
source
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)
source
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)
source
@[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
source
@[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)
source
def LO.Arith.Formalized.zero :
ℕ
Equations
source
def LO.Arith.Formalized.one :
ℕ
Equations
source
def LO.Arith.Formalized.qqAdd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
V
Equations
Instances For
source
def LO.Arith.Formalized.qqMul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
V
Equations
Instances For
source
def LO.Arith.Formalized.«term𝟎» :
Lean.ParserDescr
Equations
source
def LO.Arith.Formalized.«term𝟏» :
Lean.ParserDescr
Equations
source
def LO.Arith.Formalized.«term_^+_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Formalized.«term_^*_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.FirstOrder.Arith.qqAddDef :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.FirstOrder.Arith.qqMulDef :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Formalized.qqAdd_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₂ LO.Arith.Formalized.qqAdd via LO.FirstOrder.Arith.qqAddDef
source
theorem LO.Arith.Formalized.qqMul_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₂ LO.Arith.Formalized.qqMul via LO.FirstOrder.Arith.qqMulDef
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
@[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
source
@[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
source
@[simp]
theorem LO.Arith.Formalized.lt_qqAdd_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
x < x ^+ y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqAdd_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
y < x ^+ y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqMul_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
x < x ^* y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqMul_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :
y < x ^* y
source
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
source
@[simp]
theorem LO.Arith.Formalized.zero_semiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} :
⌜ℒₒᵣ⌝.IsSemiterm n ↑𝟎
source
@[simp]
theorem LO.Arith.Formalized.one_semiterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} :
⌜ℒₒᵣ⌝.IsSemiterm n ↑𝟏
source
def LO.Arith.Formalized.Numeral.blueprint :
LO.Arith.PR.Blueprint 0
Equations
  • One or more equations did not get rendered due to their size.
source
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 := ⋯ }
source
def LO.Arith.Formalized.Numeral.numeralAux {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
V
Equations
Instances For
source
@[simp]
theorem LO.Arith.Formalized.Numeral.numeralAux_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
LO.Arith.Formalized.Numeral.numeralAux 0 = ↑𝟏
source
@[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 ^+ ↑𝟏
source
def LO.Arith.Formalized.Numeral.numeralAuxDef :
𝚺₁.Semisentence 2
Equations
source
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
source
@[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)
source
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
  • ⋯ = ⋯
source
@[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
source
@[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)
source
def LO.Arith.Formalized.numeral {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
V
Equations
Instances For
source
@[simp]
theorem LO.Arith.Formalized.numeral_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
LO.Arith.Formalized.numeral 0 = ↑𝟎
source
@[simp]
theorem LO.Arith.Formalized.numeral_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
LO.Arith.Formalized.numeral 1 = ↑𝟏
source
@[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) ^+ ↑𝟏
source
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 ^+ ↑𝟏
source
@[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)
source
@[simp]
theorem LO.Arith.Formalized.numeral_uterm {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :
⌜ℒₒᵣ⌝.IsUTerm (LO.Arith.Formalized.numeral x)
source
@[simp]
theorem LO.Arith.Formalized.le_numeral_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) :
n ≤ LO.Arith.Formalized.numeral n
source
def LO.FirstOrder.Arith.numeralDef :
𝚺₁.Semisentence 2
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Formalized.numeral_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₁ LO.Arith.Formalized.numeral via LO.FirstOrder.Arith.numeralDef
source
@[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)
source
instance LO.Arith.Formalized.numeral_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₁ LO.Arith.Formalized.numeral
Equations
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
@[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
source
@[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
source
@[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