Documentation

Foundation.FirstOrder.Internal.Syntax.Term.Functions

def LO.ISigma1.Metamath.TermSubst.blueprint :

Language.TermRec.Blueprint 1

Equations

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

Instances For

noncomputable def LO.ISigma1.Metamath.TermSubst.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

Language.TermRec.Construction V blueprint

Equations

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

Instances For

noncomputable def LO.ISigma1.Metamath.termSubst {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] (w t : V) :

V

Equations

LO.ISigma1.Metamath.termSubst L w t = LO.ISigma1.Metamath.Language.TermRec.Construction.result L LO.ISigma1.Metamath.TermSubst.construction ![w] t

Instances For

noncomputable def LO.ISigma1.Metamath.termSubstVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] (k w v : V) :

V

Equations

LO.ISigma1.Metamath.termSubstVec L k w v = LO.ISigma1.Metamath.Language.TermRec.Construction.resultVec L LO.ISigma1.Metamath.TermSubst.construction ![w] k v

Instances For

def LO.ISigma1.Metamath.termSubstGraph (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] :

𝚺₁.Semisentence 3

Equations

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

Instances For

def LO.ISigma1.Metamath.termSubstVecGraph (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] :

𝚺₁.Semisentence 4

Equations

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

Instances For

@[simp]

theorem LO.ISigma1.Metamath.termSubst_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {w : V} (z : V) :

termSubst L w (qqBvar z) = nth w z

@[simp]

theorem LO.ISigma1.Metamath.termSubst_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {w : V} (x : V) :

termSubst L w (qqFvar x) = qqFvar x

@[simp]

theorem LO.ISigma1.Metamath.termSubst_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {w k f v : V} (hkf : L.IsFunc k f) (hv : IsUTermVec L k v) :

termSubst L w (qqFunc k f v) = qqFunc k f (termSubstVec L k w v)

theorem LO.ISigma1.Metamath.termSubst.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₂ termSubst L via termSubstGraph L

instance LO.ISigma1.Metamath.termSubst.definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₂ termSubst L

instance LO.ISigma1.Metamath.termSubst.definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {k : ℕ} :

{ Γ := Γ, rank := k + 1 }-Function₂ termSubst L

theorem LO.ISigma1.Metamath.termSubstVec.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₃ termSubstVec L via termSubstVecGraph L

instance LO.ISigma1.Metamath.termSubstVec.definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₃ termSubstVec L

instance LO.ISigma1.Metamath.termSubstVec.definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} :

{ Γ := Γ, rank := i + 1 }-Function₃ termSubstVec L

@[simp]

theorem LO.ISigma1.Metamath.len_termSubstVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {w k ts : V} (hts : IsUTermVec L k ts) :

len (termSubstVec L k w ts) = k

@[simp]

theorem LO.ISigma1.Metamath.nth_termSubstVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {w k ts i : V} (hts : IsUTermVec L k ts) (hi : i < k) :

nth (termSubstVec L k w ts) i = termSubst L w (nth ts i)

@[simp]

theorem LO.ISigma1.Metamath.termSubstVec_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] (w : V) :

termSubstVec L 0 w 0 = 0

theorem LO.ISigma1.Metamath.termSubstVec_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {w k t ts : V} (ht : IsUTerm L t) (hts : IsUTermVec L k ts) :

termSubstVec L (k + 1) w (cons t ts) = cons (termSubst L w t) (termSubstVec L k w ts)

@[simp]

theorem LO.ISigma1.Metamath.termSubstVec_cons₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {w t : V} (ht : IsUTerm L t) :

termSubstVec L 1 w ?[t] = ?[termSubst L w t]

@[simp]

theorem LO.ISigma1.Metamath.termSubstVec_cons₂ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {w t₁ t₂ : V} (ht₁ : IsUTerm L t₁) (ht₂ : IsUTerm L t₂) :

termSubstVec L 2 w ?[t₁, t₂] = ?[termSubst L w t₁, termSubst L w t₂]

@[simp]

theorem LO.ISigma1.Metamath.IsSemitermVec.termSubst {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n m w t : V} (hw : IsSemitermVec L n m w) (ht : IsSemiterm L n t) :

IsSemiterm L m (Metamath.termSubst L w t)

@[simp]

theorem LO.ISigma1.Metamath.IsUTermVec.termSubst {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n w t : V} (hw : IsUTermVec L n w) (ht : IsSemiterm L n t) :

IsUTerm L (Metamath.termSubst L w t)

@[simp]

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

IsSemitermVec L k m (Metamath.termSubstVec L k w v)

@[simp]

theorem LO.ISigma1.Metamath.substs_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsSemiterm L 0 t) :

termSubst L 0 t = t

theorem LO.ISigma1.Metamath.termSubst_termSubst {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {l n w v t : V} (hv : IsSemitermVec L l n v) (ht : IsSemiterm L l t) :

termSubst L w (termSubst L v t) = termSubst L (termSubstVec L l w v) t

theorem LO.ISigma1.Metamath.termSubst_eq_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n w t : V} (ht : IsSemiterm L n t) (H : ∀ i < n, nth w i = qqBvar i) :

termSubst L w t = t

def LO.ISigma1.Metamath.TermShift.blueprint :

Language.TermRec.Blueprint 0

Equations

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

Instances For

noncomputable def LO.ISigma1.Metamath.TermShift.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

Language.TermRec.Construction V blueprint

Equations

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

Instances For

noncomputable def LO.ISigma1.Metamath.termShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] (t : V) :

V

Equations

LO.ISigma1.Metamath.termShift L t = LO.ISigma1.Metamath.Language.TermRec.Construction.result L LO.ISigma1.Metamath.TermShift.construction ![] t

Instances For

noncomputable def LO.ISigma1.Metamath.termShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] (k v : V) :

V

Equations

LO.ISigma1.Metamath.termShiftVec L k v = LO.ISigma1.Metamath.Language.TermRec.Construction.resultVec L LO.ISigma1.Metamath.TermShift.construction ![] k v

Instances For

def LO.ISigma1.Metamath.termShiftGraph (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] :

𝚺₁.Semisentence 2

Equations

LO.ISigma1.Metamath.termShiftGraph L = LO.ISigma1.Metamath.Language.TermRec.Blueprint.result L LO.ISigma1.Metamath.TermShift.blueprint

Instances For

def LO.ISigma1.Metamath.termShiftVecGraph (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] :

𝚺₁.Semisentence 3

Equations

LO.ISigma1.Metamath.termShiftVecGraph L = LO.ISigma1.Metamath.Language.TermRec.Blueprint.resultVec L LO.ISigma1.Metamath.TermShift.blueprint

Instances For

@[simp]

theorem LO.ISigma1.Metamath.termShift_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] (z : V) :

termShift L (qqBvar z) = qqBvar z

@[simp]

theorem LO.ISigma1.Metamath.termShift_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] (x : V) :

termShift L (qqFvar x) = qqFvar (x + 1)

@[simp]

theorem LO.ISigma1.Metamath.termShift_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k f v : V} (hkf : L.IsFunc k f) (hv : IsUTermVec L k v) :

termShift L (qqFunc k f v) = qqFunc k f (termShiftVec L k v)

theorem LO.ISigma1.Metamath.termShift.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₁ termShift L via termShiftGraph L

instance LO.ISigma1.Metamath.termShift.definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₁ termShift L

instance LO.ISigma1.Metamath.termShift.definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} :

{ Γ := Γ, rank := i + 1 }-Function₁ termShift L

theorem LO.ISigma1.Metamath.termShiftVec.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₂ termShiftVec L via termShiftVecGraph L

instance LO.ISigma1.Metamath.termShiftVec.definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₂ termShiftVec L

instance LO.ISigma1.Metamath.termShiftVec.definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} :

{ Γ := Γ, rank := i + 1 }-Function₂ termShiftVec L

@[simp]

theorem LO.ISigma1.Metamath.len_termShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k ts : V} (hts : IsUTermVec L k ts) :

len (termShiftVec L k ts) = k

@[simp]

theorem LO.ISigma1.Metamath.nth_termShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k ts i : V} (hts : IsUTermVec L k ts) (hi : i < k) :

nth (termShiftVec L k ts) i = termShift L (nth ts i)

@[simp]

theorem LO.ISigma1.Metamath.termShiftVec_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

termShiftVec L 0 0 = 0

theorem LO.ISigma1.Metamath.termShiftVec_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k t ts : V} (ht : IsUTerm L t) (hts : IsUTermVec L k ts) :

termShiftVec L (k + 1) (cons t ts) = cons (termShift L t) (termShiftVec L k ts)

@[simp]

theorem LO.ISigma1.Metamath.termShiftVec_cons₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {t₁ : V} (ht₁ : IsUTerm L t₁) :

termShiftVec L 1 ?[t₁] = ?[termShift L t₁]

@[simp]

theorem LO.ISigma1.Metamath.termShiftVec_cons₂ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {t₁ t₂ : V} (ht₁ : IsUTerm L t₁) (ht₂ : IsUTerm L t₂) :

termShiftVec L 2 ?[t₁, t₂] = ?[termShift L t₁, termShift L t₂]

@[simp]

theorem LO.ISigma1.Metamath.IsUTerm.termShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsUTerm L t) :

IsUTerm L (Metamath.termShift L t)

@[simp]

theorem LO.ISigma1.Metamath.IsSemiterm.termShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n t : V} (ht : IsSemiterm L n t) :

IsSemiterm L n (Metamath.termShift L t)

@[simp]

theorem LO.ISigma1.Metamath.IsUTermVec.termShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k v : V} (hv : IsUTermVec L k v) :

IsUTermVec L k (Metamath.termShiftVec L k v)

@[simp]

theorem LO.ISigma1.Metamath.IsSemitermVec.termShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k n v : V} (hv : IsSemitermVec L k n v) :

IsSemitermVec L k n (Metamath.termShiftVec L k v)

@[simp]

theorem LO.ISigma1.Metamath.IsUTerm.termBVtermShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsUTerm L t) :

termBV L (Metamath.termShift L t) = termBV L t

@[simp]

theorem LO.ISigma1.Metamath.IsUTermVec.termBVVectermShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k v : V} (hv : IsUTermVec L k v) :

termBVVec L k (Metamath.termShiftVec L k v) = termBVVec L k v

def LO.ISigma1.Metamath.TermBShift.blueprint :

Language.TermRec.Blueprint 0

Equations

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

Instances For

noncomputable def LO.ISigma1.Metamath.TermBShift.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

Language.TermRec.Construction V blueprint

Equations

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

Instances For

noncomputable def LO.ISigma1.Metamath.termBShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] (t : V) :

V

Equations

LO.ISigma1.Metamath.termBShift L t = LO.ISigma1.Metamath.Language.TermRec.Construction.result L LO.ISigma1.Metamath.TermBShift.construction ![] t

Instances For

noncomputable def LO.ISigma1.Metamath.termBShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] (k v : V) :

V

Equations

LO.ISigma1.Metamath.termBShiftVec L k v = LO.ISigma1.Metamath.Language.TermRec.Construction.resultVec L LO.ISigma1.Metamath.TermBShift.construction ![] k v

Instances For

def LO.ISigma1.Metamath.termBShiftGraph (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] :

𝚺₁.Semisentence 2

Equations

LO.ISigma1.Metamath.termBShiftGraph L = LO.ISigma1.Metamath.Language.TermRec.Blueprint.result L LO.ISigma1.Metamath.TermBShift.blueprint

Instances For

def LO.ISigma1.Metamath.termBShiftVecGraph (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] :

𝚺₁.Semisentence 3

Equations

LO.ISigma1.Metamath.termBShiftVecGraph L = LO.ISigma1.Metamath.Language.TermRec.Blueprint.resultVec L LO.ISigma1.Metamath.TermBShift.blueprint

Instances For

@[simp]

theorem LO.ISigma1.Metamath.termBShift_bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] (z : V) :

termBShift L (qqBvar z) = qqBvar (z + 1)

@[simp]

theorem LO.ISigma1.Metamath.termBShift_fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] (x : V) :

termBShift L (qqFvar x) = qqFvar x

@[simp]

theorem LO.ISigma1.Metamath.termBShift_func {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k f v : V} (hkf : L.IsFunc k f) (hv : IsUTermVec L k v) :

termBShift L (qqFunc k f v) = qqFunc k f (termBShiftVec L k v)

theorem LO.ISigma1.Metamath.termBShift.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₁ termBShift L via termBShiftGraph L

instance LO.ISigma1.Metamath.termBShift.definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₁ termBShift L

instance LO.ISigma1.Metamath.termBShift.definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} :

{ Γ := Γ, rank := i + 1 }-Function₁ termBShift L

theorem LO.ISigma1.Metamath.termBShiftVec.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₂ termBShiftVec L via termBShiftVecGraph L

instance LO.ISigma1.Metamath.termBShiftVec.definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₂ termBShiftVec L

instance LO.ISigma1.Metamath.termBShiftVec.definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} :

{ Γ := Γ, rank := i + 1 }-Function₂ termBShiftVec L

@[simp]

theorem LO.ISigma1.Metamath.len_termBShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k ts : V} (hts : IsUTermVec L k ts) :

len (termBShiftVec L k ts) = k

@[simp]

theorem LO.ISigma1.Metamath.nth_termBShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k ts i : V} (hts : IsUTermVec L k ts) (hi : i < k) :

nth (termBShiftVec L k ts) i = termBShift L (nth ts i)

@[simp]

theorem LO.ISigma1.Metamath.termBShiftVec_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

termBShiftVec L 0 0 = 0

theorem LO.ISigma1.Metamath.termBShiftVec_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k t ts : V} (ht : IsUTerm L t) (hts : IsUTermVec L k ts) :

termBShiftVec L (k + 1) (cons t ts) = cons (termBShift L t) (termBShiftVec L k ts)

@[simp]

theorem LO.ISigma1.Metamath.termBShiftVec_cons₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {t₁ : V} (ht₁ : IsUTerm L t₁) :

termBShiftVec L 1 ?[t₁] = ?[termBShift L t₁]

@[simp]

theorem LO.ISigma1.Metamath.termBShiftVec_cons₂ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {t₁ t₂ : V} (ht₁ : IsUTerm L t₁) (ht₂ : IsUTerm L t₂) :

termBShiftVec L 2 ?[t₁, t₂] = ?[termBShift L t₁, termBShift L t₂]

@[simp]

theorem LO.ISigma1.Metamath.IsSemiterm.termBShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n t : V} (ht : IsSemiterm L n t) :

IsSemiterm L (n + 1) (Metamath.termBShift L t)

@[simp]

theorem LO.ISigma1.Metamath.IsSemitermVec.termBShiftVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k n v : V} (hv : IsSemitermVec L k n v) :

IsSemitermVec L k (n + 1) (Metamath.termBShiftVec L k v)

theorem LO.ISigma1.Metamath.termBShift_termShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n t : V} (ht : IsSemiterm L n t) :

termBShift L (termShift L t) = termShift L (termBShift L t)

noncomputable def LO.ISigma1.Metamath.qVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] (w : V) :

V

Equations

LO.ISigma1.Metamath.qVec L w = cons (LO.ISigma1.Metamath.qqBvar 0) (LO.ISigma1.Metamath.termBShiftVec L (LO.ISigma1.len w) w)

Instances For

def LO.ISigma1.Metamath.qVecGraph (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] :

𝚺₁.Semisentence 2

Equations

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

Instances For

theorem LO.ISigma1.Metamath.qVec.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₁ qVec L via qVecGraph L

instance LO.ISigma1.Metamath.qVec.definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] :

𝚺₁ -Function₁ qVec L

instance LO.ISigma1.Metamath.qVec.definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₁ qVec L

@[simp]

theorem LO.ISigma1.Metamath.len_qVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k w : V} (h : IsUTermVec L k w) :

len (qVec L w) = k + 1

theorem LO.ISigma1.Metamath.IsSemitermVec.qVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {k n w : V} (h : IsSemitermVec L k n w) :

IsSemitermVec L (k + 1) (n + 1) (Metamath.qVec L w)

theorem LO.ISigma1.Metamath.substs_cons_bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n u t w : V} (ht : IsSemiterm L n t) :

termSubst L (cons u w) (termBShift L t) = termSubst L w t

theorem LO.ISigma1.Metamath.termShift_termSubsts {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n m w t : V} (ht : IsSemiterm L n t) (hw : IsSemitermVec L n m w) :

termShift L (termSubst L w t) = termSubst L (termShiftVec L n w) (termShift L t)

theorem LO.ISigma1.Metamath.bShift_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n m w t : V} (ht : IsSemiterm L n t) (hw : IsSemitermVec L n m w) :

termBShift L (termSubst L w t) = termSubst L (termBShiftVec L n w) t

theorem LO.ISigma1.Metamath.substs_qVec_bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n t m w : V} (ht : IsSemiterm L n t) (hw : IsSemitermVec L n m w) :

termSubst L (qVec L w) (termBShift L t) = termBShift L (termSubst L w t)

theorem LO.ISigma1.Metamath.termSubstVec_qVec_qVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {v w l n m : V} (hv : IsSemitermVec L l n v) (hw : IsSemitermVec L n m w) :

termSubstVec L (l + 1) (qVec L w) (qVec L v) = qVec L (termSubstVec L l w v)

theorem LO.ISigma1.Metamath.termShift_qVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n m w : V} (hw : IsSemitermVec L n m w) :

termShiftVec L (n + 1) (qVec L w) = qVec L (termShiftVec L n w)

def LO.ISigma1.Metamath.IsTermFVFree {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : FirstOrder.Language) [L.Encodable] [L.LORDefinable] (n t : V) :

Equations

LO.ISigma1.Metamath.IsTermFVFree L n t = (LO.ISigma1.Metamath.IsSemiterm L n t ∧ LO.ISigma1.Metamath.termShift L t = t)

Instances For

@[simp]

theorem LO.ISigma1.Metamath.IsTermFVFree.bvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n : V} (x : V) :

IsTermFVFree L n (qqBvar x) ↔ x < n

@[simp]

theorem LO.ISigma1.Metamath.IsTermFVFree.fvar {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : FirstOrder.Language} [L.Encodable] [L.LORDefinable] {n : V} (x : V) :

¬IsTermFVFree L n (qqFvar x)

def LO.ISigma1.Metamath.InternalArithmetic.zero :

Equations

𝟎 = LO.ISigma1.Metamath.qqFuncN 0 LO.ISigma1.Metamath.InternalArithmetic.zeroIndex 0

Instances For

def LO.ISigma1.Metamath.InternalArithmetic.one :

Equations

𝟏 = LO.ISigma1.Metamath.qqFuncN 0 LO.ISigma1.Metamath.InternalArithmetic.oneIndex 0

Instances For

noncomputable def LO.ISigma1.Metamath.InternalArithmetic.qqAdd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :

V

Equations

x ^+ y = LO.ISigma1.Metamath.qqFunc 2 ↑LO.ISigma1.Metamath.InternalArithmetic.addIndex ?[x, y]

Instances For

noncomputable def LO.ISigma1.Metamath.InternalArithmetic.qqMul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :

V

Equations

x ^* y = LO.ISigma1.Metamath.qqFunc 2 ↑LO.ISigma1.Metamath.InternalArithmetic.mulIndex ?[x, y]

Instances For

def LO.ISigma1.Metamath.InternalArithmetic.«term𝟎» :

Lean.ParserDescr

Equations

LO.ISigma1.Metamath.InternalArithmetic.«term𝟎» = Lean.ParserDescr.node `LO.ISigma1.Metamath.InternalArithmetic.«term𝟎» 1024 (Lean.ParserDescr.symbol "𝟎")

Instances For

def LO.ISigma1.Metamath.InternalArithmetic.«term𝟏» :

Lean.ParserDescr

Equations

LO.ISigma1.Metamath.InternalArithmetic.«term𝟏» = Lean.ParserDescr.node `LO.ISigma1.Metamath.InternalArithmetic.«term𝟏» 1024 (Lean.ParserDescr.symbol "𝟏")

Instances For

def LO.ISigma1.Metamath.InternalArithmetic.«term_^+_» :

Lean.TrailingParserDescr

Equations

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

Instances For

def LO.ISigma1.Metamath.InternalArithmetic.«term_^*_» :

Lean.TrailingParserDescr

Equations

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

Instances For

def LO.ISigma1.Metamath.InternalArithmetic.qqAddGraph :

𝚺₁.Semisentence 3

Equations

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

Instances For

def LO.ISigma1.Metamath.InternalArithmetic.qqMulGraph :

𝚺₁.Semisentence 3

Equations

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

Instances For

theorem LO.ISigma1.Metamath.InternalArithmetic.qqAdd_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₂ qqAdd via qqAddGraph

theorem LO.ISigma1.Metamath.InternalArithmetic.qqMul_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₂ qqMul via qqMulGraph

instance LO.ISigma1.Metamath.InternalArithmetic.instBoldfaceFunction₂MkHAddNatOfNatQqAdd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₂ qqAdd

instance LO.ISigma1.Metamath.InternalArithmetic.instBoldfaceFunction₂MkHAddNatOfNatQqMul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₂ qqMul

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.eval_qqAddGraph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :

V ⊧/v ↑qqAddGraph ↔ v 0 = v 1 ^+ v 2

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.eval_qqMulGraph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :

V ⊧/v ↑qqMulGraph ↔ v 0 = v 1 ^* v 2

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.lt_qqAdd_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :

x < x ^+ y

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.lt_qqAdd_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :

y < x ^+ y

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.lt_qqMul_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :

x < x ^* y

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.lt_qqMul_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :

y < x ^* y

theorem LO.ISigma1.Metamath.InternalArithmetic.qqFunc_absolute {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k f v : ℕ) :

↑(qqFunc k f v) = qqFunc ↑k ↑f ↑v

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.zero_semiterm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} :

IsSemiterm ℒₒᵣ n ↑𝟎

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.one_semiterm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} :

IsSemiterm ℒₒᵣ n ↑𝟏

theorem LO.ISigma1.Metamath.InternalArithmetic.coe_zero_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

↑𝟎 = qqFunc 0 ⌜FirstOrder.Language.Zero.zero ⌝ 0

theorem LO.ISigma1.Metamath.InternalArithmetic.coe_one_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

↑𝟏 = qqFunc 0 ⌜FirstOrder.Language.One.one ⌝ 0

def LO.ISigma1.Metamath.InternalArithmetic.Numeral.blueprint :

Equations

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

Instances For

noncomputable def LO.ISigma1.Metamath.InternalArithmetic.Numeral.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

PR.Construction V blueprint

Equations

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

Instances For

noncomputable def LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAux {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :

V

Equations

LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAux x = LO.ISigma1.Metamath.InternalArithmetic.Numeral.construction.result ![] x

Instances For

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAux_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

numeralAux 0 = ↑𝟏

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAux_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :

numeralAux (x + 1) = numeralAux x ^+ ↑𝟏

def LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAuxGraph :

𝚺₁.Semisentence 2

Equations

LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAuxGraph = LO.ISigma1.Metamath.InternalArithmetic.Numeral.blueprint.resultDef

Instances For

theorem LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAux.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₁ numeralAux via numeralAuxGraph

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAuxGraph.eval {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) :

V ⊧/v ↑numeralAuxGraph ↔ v 0 = numeralAux (v 1)

instance LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAux.definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

{ Γ := 𝚺, rank := 0 + 1 }-Function₁ numeralAux

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.Numeral.lt_numeralAux_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) :

n < numeralAux n

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAux_semiterm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n x : V) :

IsSemiterm ℒₒᵣ n (numeralAux x)

noncomputable def LO.ISigma1.Metamath.InternalArithmetic.numeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :

V

Equations

LO.ISigma1.Metamath.InternalArithmetic.numeral x = if x = 0 then ↑𝟎 else LO.ISigma1.Metamath.InternalArithmetic.Numeral.numeralAux (x - 1)

Instances For

def LO.ISigma1.Metamath.InternalArithmetic.numeralGraph :

𝚺₁.Semisentence 2

Equations

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

Instances For

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

numeral 0 = ↑𝟎

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

numeral 1 = ↑𝟏

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_add_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} :

numeral (n + 1 + 1) = numeral (n + 1) ^+ ↑𝟏

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_succ_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (pos : 0 < n) :

numeral (n + 1) = numeral n ^+ ↑𝟏

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_semiterm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n x : V) :

IsSemiterm ℒₒᵣ n (numeral x)

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_uterm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :

IsUTerm ℒₒᵣ (numeral x)

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.le_numeral_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) :

n ≤ numeral n

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₁ numeral via numeralGraph

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.eval_numeralGraph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) :

V ⊧/v ↑numeralGraph ↔ v 0 = numeral (v 1)

instance LO.ISigma1.Metamath.InternalArithmetic.numeral_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₁ numeral

instance LO.ISigma1.Metamath.InternalArithmetic.numeral_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₁ numeral

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m w : V} :

IsSemitermVec ℒₒᵣ n m w → ∀ (x : V), termSubst ℒₒᵣ w (numeral x) = numeral x

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :

termShift ℒₒᵣ (numeral x) = numeral x

@[simp]

theorem LO.ISigma1.Metamath.InternalArithmetic.numeral_bShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) :

termBShift ℒₒᵣ (numeral x) = numeral x