Supporting results for pointwise provable equality.

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

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.constructionBvarAssignment {V : Type u_1} (v : Fin 3 → V) : Fin 3 → V

The construction Bvar Assignment construction in FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.constructionBvarAssignment v = ![v 0, v 2, v 1]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.constructionBvarTerms_val {V : Type u_1} [ORingStructure V] (v : Fin 3 → V) : Semiterm.val v Empty.elim ∘ ![Semiterm.bvar 0, Semiterm.bvar 2, Semiterm.bvar 1] = constructionBvarAssignment v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.constructionBvarSubstitution_eval {V : Type u_1} [ORingStructure V] (v : Fin 3 → V) : (Semiformula.Evalb v) (↑nthDef/[Semiterm.bvar 0, Semiterm.bvar 2, Semiterm.bvar 1]) ↔ (Semiformula.Evalb (constructionBvarAssignment v)) ↑nthDef

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.constructionBvarResult {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : Fin 3 → V) : (Semiformula.Evalb (constructionBvarAssignment v)) ↑nthDef ↔ v 0 = (fun (w : Fin (1 + 1) → V) => nth ((fun (x : Fin 1) => w x.succ) 1) (w 0)) fun (x : Fin (1 + 1)) => v x.succ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.constructionBvarEvaluation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : Fin (1 + 1 + 1) → V) : (Semiformula.Evalb v) ↑blueprint.bvar ↔ v 0 = (fun (w : Fin (1 + 1) → V) => nth ((fun (x : Fin 1) => w x.succ) 1) (w 0)) fun (x : Fin (1 + 1)) => v x.succ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.constructionBvarDefined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : HierarchySymbol.DefinedFunction (fun (w : Fin (1 + 1) → V) => nth ((fun (x : Fin 1) => w x.succ) 1) (w 0)) blueprint.bvar

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Language.TermRec.Construction V blueprint

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.TermSubst.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termSubst {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (w t : V) : V

The term Subst construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termSubstVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (k w v : V) : V

The term Subst Vec construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termSubstGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 3

The term Subst Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termSubstVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 4

The term Subst Vec Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termSubst.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₂ termSubst L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termSubstVec.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₃ termSubstVec L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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₂]

theorem PointwiseComposition.FFL.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)

theorem PointwiseComposition.FFL.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)

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermShift.blueprint : Language.TermRec.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.TermShift.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermShift.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Language.TermRec.Construction V blueprint

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.TermShift.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termShift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (t : V) : V

The term Shift construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termShiftVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (k v : V) : V

The term Shift Vec construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termShiftGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 2

The term Shift Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termShiftVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 3

The term Shift Vec Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termShift.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₁ termShift L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termShiftVec.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₂ termShiftVec L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termShiftVec_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : termShiftVec L 0 0 = 0

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermBShift.blueprint : Language.TermRec.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.TermBShift.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.TermBShift.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Language.TermRec.Construction V blueprint

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.TermBShift.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termBShift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (t : V) : V

The term BShift construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (k v : V) : V

The term BShift Vec construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termBShiftGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 2

The term BShift Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termBShiftVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 3

The term BShift Vec Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termBShift.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₁ termBShift L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₂ termBShiftVec L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.termBShiftVec_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : termBShiftVec L 0 0 = 0

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (w : V) : V

The q Vec construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 2

The q Vec Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qVec.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₁ qVec L

instance PointwiseComposition.FFL.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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsTermFVFree {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (n t : V) : Prop

The Is Term FVFree construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.zero : ℕ

The 𝟘 construction in 𝟘.

Equations

• 𝟘 = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqFuncN 0 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.zeroIndex 0

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.one : ℕ

The 𝟙 construction in 𝟙.

Equations

• 𝟙 = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqFuncN 0 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.oneIndex 0

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqAdd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : V

The qq Add construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqMul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : V

The qq Mul construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.«term𝟘» : Lean.ParserDescr

The «term𝟘» construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.«term𝟙» : Lean.ParserDescr

The «term𝟙» construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.«term_^+_» : Lean.TrailingParserDescr

The «term ^+ » construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.«term_^*_» : Lean.TrailingParserDescr

The «term ^* » construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqAddGraph : Σ₁.Semisentence 3

The qq Add Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqMulGraph : Σ₁.Semisentence 3

The qq Mul Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqAdd_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ qqAdd via qqAddGraph

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqMul_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ qqMul via qqMulGraph

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.instDefinableFunction₂MkHAddNatOfNatQqAdd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₂ qqAdd

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.instDefinableFunction₂MkHAddNatOfNatQqMul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₂ qqMul

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqAdd_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : x < x ^+ y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqAdd_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : y < x ^+ y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqMul_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : x < x ^* y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqMul_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : y < x ^* y

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqFunc_absolute {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (k f v : ℕ) : ↑(qqFunc k f v) = qqFunc ↑k ↑f ↑v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.zero_semiterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : V} : IsSemiterm ℒₒᵣ n ↑𝟘

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.one_semiterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : V} : IsSemiterm ℒₒᵣ n ↑𝟙

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.coe_zero_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : ↑𝟘 = qqFunc 0 ⌜Language.Zero.zero⌝ 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.coe_one_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : ↑𝟙 = qqFunc 0 ⌜Language.One.one⌝ 0

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.blueprint : PR.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : PR.Construction V blueprint

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.numeralAux {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : V

The numeral Aux construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.numeralAux_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : numeralAux 0 = ↑𝟙

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.numeralAux_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : numeralAux (x + 1) = numeralAux x ^+ ↑𝟙

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.numeralAuxGraph : Σ₁.Semisentence 2

The numeral Aux Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.numeralAux.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ numeralAux via numeralAuxGraph

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.numeralAux.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : { Γ := Σ, rank := 0 + 1 }-Function₁ numeralAux

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.lt_numeralAux_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (n : V) : n < numeralAux n

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.Numeral.numeralAux_semiterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (n x : V) : IsSemiterm ℒₒᵣ n (numeralAux x)

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : V

The numeral construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeralGraph : Σ₁.Semisentence 2

The numeral Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : numeral 0 = ↑𝟘

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : numeral 1 = ↑𝟙

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_add_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : V} : numeral (n + 1 + 1) = numeral (n + 1) ^+ ↑𝟙

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_succ_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : V} (pos : 0 < n) : numeral (n + 1) = numeral n ^+ ↑𝟙

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_semiterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (n x : V) : IsSemiterm ℒₒᵣ n (numeral x)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_uterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : IsUTerm ℒₒᵣ (numeral x)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.le_numeral_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (n : V) : n ≤ numeral n

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ numeral via numeralGraph

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ numeral

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ numeral

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : termShift ℒₒᵣ (numeral x) = numeral x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.numeral_bShift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : termBShift ℒₒᵣ (numeral x) = numeral x