def LO.FirstOrder.Arithmetic.Bootstrapping.TermSubst.blueprint : Language.TermRec.Blueprint 1

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TermSubst.construction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : Language.TermRec.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termSubst {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (w t : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termSubstVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (k w v : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termSubstGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 3

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termSubstVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 4

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termSubst_bvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w : V} (z : V) : termSubst L w (qqBvar z) = nth w z

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termSubst_fvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w : V} (x : V) : termSubst L w (qqFvar x) = qqFvar x

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termSubst_func {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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)

instance LO.FirstOrder.Arithmetic.Bootstrapping.termSubst.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ termSubst L via termSubstGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termSubst.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ termSubst L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termSubst.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {k : ℕ} : { Γ := Γ, rank := k + 1 }-Function₂ termSubst L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termSubstVec.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₃ termSubstVec L via termSubstVecGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termSubstVec.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₃ termSubstVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termSubstVec.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} : { Γ := Γ, rank := i + 1 }-Function₃ termSubstVec L

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.len_termSubstVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w k ts : V} (hts : IsUTermVec L k ts) : len (termSubstVec L k w ts) = k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.nth_termSubstVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.termSubstVec_nil {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (w : V) : termSubstVec L 0 w 0 = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termSubstVec_cons {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w k t ts : V} (ht : IsUTerm L t) (hts : IsUTermVec L k ts) : termSubstVec L (k + 1) w (adjoin t ts) = adjoin (termSubst L w t) (termSubstVec L k w ts)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termSubstVec_cons₁ {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w t : V} (ht : IsUTerm L t) : termSubstVec L 1 w ?[t] = ?[termSubst L w t]

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termSubstVec_cons₂ {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.termSubst {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n m w t : V} (hw : IsSemitermVec L n m w) (ht : IsSemiterm L n t) : IsSemiterm L m (Bootstrapping.termSubst L w t)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.termSubst {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n w t : V} (hw : IsUTermVec L n w) (ht : IsSemiterm L n t) : IsUTerm L (Bootstrapping.termSubst L w t)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.termSubstVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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 (Bootstrapping.termSubstVec L k w v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_nil {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsSemiterm L 0 t) : termSubst L 0 t = t

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termSubst_termSubst {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.termSubst_eq_self {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.TermShift.blueprint : Language.TermRec.Blueprint 0

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TermShift.construction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : Language.TermRec.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (t : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (k v : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termShiftGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.termShiftGraph L = LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Blueprint.result L LO.FirstOrder.Arithmetic.Bootstrapping.TermShift.blueprint

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termShiftVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 3

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termShift_bvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (z : V) : termShift L (qqBvar z) = qqBvar z

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termShift_fvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (x : V) : termShift L (qqFvar x) = qqFvar (x + 1)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termShift_func {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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)

instance LO.FirstOrder.Arithmetic.Bootstrapping.termShift.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ termShift L via termShiftGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termShift.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ termShift L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termShift.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} : { Γ := Γ, rank := i + 1 }-Function₁ termShift L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termShiftVec.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ termShiftVec L via termShiftVecGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termShiftVec.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ termShiftVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termShiftVec.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} : { Γ := Γ, rank := i + 1 }-Function₂ termShiftVec L

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.len_termShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k ts : V} (hts : IsUTermVec L k ts) : len (termShiftVec L k ts) = k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.nth_termShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.termShiftVec_nil {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : termShiftVec L 0 0 = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termShiftVec_cons {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k t ts : V} (ht : IsUTerm L t) (hts : IsUTermVec L k ts) : termShiftVec L (k + 1) (adjoin t ts) = adjoin (termShift L t) (termShiftVec L k ts)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termShiftVec_cons₁ {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t₁ : V} (ht₁ : IsUTerm L t₁) : termShiftVec L 1 ?[t₁] = ?[termShift L t₁]

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termShiftVec_cons₂ {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.termShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsUTerm L t) : IsUTerm L (Bootstrapping.termShift L t)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.termShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t : V} (ht : IsSemiterm L n t) : IsSemiterm L n (Bootstrapping.termShift L t)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.termShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k v : V} (hv : IsUTermVec L k v) : IsUTermVec L k (Bootstrapping.termShiftVec L k v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.termShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n v : V} (hv : IsSemitermVec L k n v) : IsSemitermVec L k n (Bootstrapping.termShiftVec L k v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.termBVtermShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} (ht : IsUTerm L t) : termBV L (Bootstrapping.termShift L t) = termBV L t

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.termBVVectermShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k v : V} (hv : IsUTermVec L k v) : termBVVec L k (Bootstrapping.termShiftVec L k v) = termBVVec L k v

def LO.FirstOrder.Arithmetic.Bootstrapping.TermBShift.blueprint : Language.TermRec.Blueprint 0

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TermBShift.construction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : Language.TermRec.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termBShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (t : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (k v : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftGraph L = LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Blueprint.result L LO.FirstOrder.Arithmetic.Bootstrapping.TermBShift.blueprint

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 3

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBShift_bvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (z : V) : termBShift L (qqBvar z) = qqBvar (z + 1)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBShift_fvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (x : V) : termBShift L (qqFvar x) = qqFvar x

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBShift_func {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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)

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBShift.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ termBShift L via termBShiftGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBShift.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ termBShift L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBShift.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} : { Γ := Γ, rank := i + 1 }-Function₁ termBShift L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ termBShiftVec L via termBShiftVecGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ termBShiftVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} : { Γ := Γ, rank := i + 1 }-Function₂ termBShiftVec L

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.len_termBShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k ts : V} (hts : IsUTermVec L k ts) : len (termBShiftVec L k ts) = k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.nth_termBShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec_nil {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : termBShiftVec L 0 0 = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec_cons {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k t ts : V} (ht : IsUTerm L t) (hts : IsUTermVec L k ts) : termBShiftVec L (k + 1) (adjoin t ts) = adjoin (termBShift L t) (termBShiftVec L k ts)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec_cons₁ {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t₁ : V} (ht₁ : IsUTerm L t₁) : termBShiftVec L 1 ?[t₁] = ?[termBShift L t₁]

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec_cons₂ {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.termBShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t : V} (ht : IsSemiterm L n t) : IsSemiterm L (n + 1) (Bootstrapping.termBShift L t)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.termBShiftVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n v : V} (hv : IsSemitermVec L k n v) : IsSemitermVec L k (n + 1) (Bootstrapping.termBShiftVec L k v)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBShift_termShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.qVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (w : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.qVec.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ qVec L via qVecGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.qVec.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ qVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.qVec.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ qVec L

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.len_qVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k w : V} (h : IsUTermVec L k w) : len (qVec L w) = k + 1

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.qVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n w : V} (h : IsSemitermVec L k n w) : IsSemitermVec L (k + 1) (n + 1) (Bootstrapping.qVec L w)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_cons_bShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n u t w : V} (ht : IsSemiterm L n t) : termSubst L (adjoin u w) (termBShift L t) = termSubst L w t

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termShift_termSubsts {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.bShift_substs {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.substs_qVec_bShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.termSubstVec_qVec_qVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.termShift_qVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : 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.FirstOrder.Arithmetic.Bootstrapping.IsTermFVFree {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (n t : V) : Prop

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsTermFVFree L n t = (LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm L n t ∧ LO.FirstOrder.Arithmetic.Bootstrapping.termShift L t = t)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsTermFVFree.bvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : V} (x : V) : IsTermFVFree L n (qqBvar x) ↔ x < n

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsTermFVFree.fvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : V} (x : V) : ¬IsTermFVFree L n (qqFvar x)

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.zero : ℕ

Equations

• 𝟎 = LO.FirstOrder.Arithmetic.Bootstrapping.qqFuncN 0 LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.zeroIndex 0

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.one : ℕ

Equations

• 𝟏 = LO.FirstOrder.Arithmetic.Bootstrapping.qqFuncN 0 LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.oneIndex 0

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqAdd {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x y : V) : V

Equations

• x ^+ y = LO.FirstOrder.Arithmetic.Bootstrapping.qqFunc 2 ↑LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.addIndex ?[x, y]

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqMul {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x y : V) : V

Equations

• x ^* y = LO.FirstOrder.Arithmetic.Bootstrapping.qqFunc 2 ↑LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.mulIndex ?[x, y]

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term𝟎» : Lean.ParserDescr

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term𝟎» = Lean.ParserDescr.node `LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term𝟎» 1024 (Lean.ParserDescr.symbol "𝟎")

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term𝟏» : Lean.ParserDescr

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term𝟏» = Lean.ParserDescr.node `LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term𝟏» 1024 (Lean.ParserDescr.symbol "𝟏")

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term_^+_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term_^*_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqAddGraph : 𝚺₁.Semisentence 3

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqMulGraph : 𝚺₁.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqAdd_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₁-Function₂ qqAdd via qqAddGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqMul_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₁-Function₂ qqMul via qqMulGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instDefinableFunction₂MkHAddNatOfNatQqAdd {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₂ qqAdd

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instDefinableFunction₂MkHAddNatOfNatQqMul {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₂ qqMul

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqAdd_left {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x y : V) : x < x ^+ y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqAdd_right {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x y : V) : y < x ^+ y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqMul_left {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x y : V) : x < x ^* y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqMul_right {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x y : V) : y < x ^* y

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqFunc_absolute {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (k f v : ℕ) : ↑(qqFunc k f v) = qqFunc ↑k ↑f ↑v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.zero_semiterm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {n : V} : IsSemiterm ℒₒᵣ n ↑𝟎

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.one_semiterm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {n : V} : IsSemiterm ℒₒᵣ n ↑𝟏

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.coe_zero_eq {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : ↑𝟎 = qqFunc 0 ⌜Language.Zero.zero⌝ 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.coe_one_eq {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : ↑𝟏 = qqFunc 0 ⌜Language.One.one⌝ 0

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.blueprint : PR.Blueprint 0

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.construction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : PR.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAux {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAux x = LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.construction.result ![] x

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAux_zero {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : numeralAux 0 = ↑𝟏

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAux_succ {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : numeralAux (x + 1) = numeralAux x ^+ ↑𝟏

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAuxGraph : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAuxGraph = LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.blueprint.resultDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAux.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₁-Function₁ numeralAux via numeralAuxGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAux.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : { Γ := 𝚺, rank := 0 + 1 }-Function₁ numeralAux

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.lt_numeralAux_self {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (n : V) : n < numeralAux n

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAux_semiterm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (n x : V) : IsSemiterm ℒₒᵣ n (numeralAux x)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral x = if x = 0 then ↑𝟎 else LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.Numeral.numeralAux (x - 1)

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeralGraph : 𝚺₁.Semisentence 2

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_zero {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : numeral 0 = ↑𝟎

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_one {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : numeral 1 = ↑𝟏

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_add_two {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {n : V} : numeral (n + 1 + 1) = numeral (n + 1) ^+ ↑𝟏

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_succ_pos {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {n : V} (pos : 0 < n) : numeral (n + 1) = numeral n ^+ ↑𝟏

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_semiterm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (n x : V) : IsSemiterm ℒₒᵣ n (numeral x)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_uterm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : IsUTerm ℒₒᵣ (numeral x)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.le_numeral_self {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (n : V) : n ≤ numeral n

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₁-Function₁ numeral via numeralGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₁-Function₁ numeral

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ numeral

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_substs {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {n m w : V} : IsSemitermVec ℒₒᵣ n m w → ∀ (x : V), termSubst ℒₒᵣ w (numeral x) = numeral x

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_shift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : termShift ℒₒᵣ (numeral x) = numeral x

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_bShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : termBShift ℒₒᵣ (numeral x) = numeral x