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

Equations

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

def LO.Arith.Language.termSubst {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (k w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w : V} (z : V) : L.termSubst w (qqBvar z) = nth w z

@[simp]

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

@[simp]

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

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

Equations

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

def LO.FirstOrder.Arith.LDef.termSubstVecDef (pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₁-Function₂ L.termSubst via pL.termSubstDef

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LO.Arith.termSubstVec_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w k t 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w t₁ 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w k n m 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {l n w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n w t : V} (ht : L.IsSemiterm n t) (H : ∀ i < n, nth w i = qqBvar i) : L.termSubst w t = t

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

Equations

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

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

Equations

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

def LO.Arith.Language.termShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (k 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (z : V) : L.termShift (qqBvar z) = qqBvar z

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem LO.Arith.termShiftVec_cons₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {t₁ 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n t : V} (ht : L.IsSemiterm n t) : L.IsSemiterm n (L.termShift t)

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

def LO.Arith.Language.termBShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (k 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (z : V) : L.termBShift (qqBvar z) = qqBvar (z + 1)

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem LO.Arith.Language.IsSemitermVec.qVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k n 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n u t 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m w 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n t m 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {v w l n 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) : L.IsTermFVFree n (qqBvar x) ↔ x < n

@[simp]

theorem LO.Arith.Language.IsTermFVFree.fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (x : V) : ¬L.IsTermFVFree n (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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ qqAdd via FirstOrder.Arith.qqAddDef

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

def LO.Arith.Formalized.Numeral.blueprint : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : PR.Construction V 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} [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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : numeralAux 0 = ↑𝟏

@[simp]

theorem LO.Arith.Formalized.Numeral.numeralAux_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : numeralAux (x + 1) = 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ numeralAux via numeralAuxDef

@[simp]

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

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

@[simp]

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

@[simp]

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

def LO.Arith.Formalized.numeral {V : Type u_1} [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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : numeral 0 = ↑𝟎

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Arith.Formalized.le_numeral_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) : n ≤ 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ numeral via FirstOrder.Arith.numeralDef

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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