Supporting results for pointwise provable equality.

def PointwiseComposition.FFL.FirstOrder.Semiformula.replicate {L : Language} {ξ : Type u_1} {n : ℕ} (p : Semiformula L ξ n) : ℕ → Semiformula L ξ n

The replicate construction in FFL.FirstOrder.Semiformula.

Equations

• p.replicate 0 = p
• p.replicate k.succ = p ⋏ p.replicate k

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.replicate_zero {L : Language} {ξ : Type u_1} {n : ℕ} (p : Semiformula L ξ n) : p.replicate 0 = p

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.replicate_succ {L : Language} {ξ : Type u_1} {n : ℕ} (p : Semiformula L ξ n) (k : ℕ) : p.replicate (k + 1) = p ⋏ p.replicate k

def PointwiseComposition.FFL.FirstOrder.Semiformula.weight {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) : Semiformula L ξ n

The weight construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.weight k = PointwiseComposition.List.conj (List.replicate k ⊤)

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.QQConj.blueprint : VecRec.Blueprint 0

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

Equations

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

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

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

Equations

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

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

The qq Conj construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqConj ps = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.QQConj.construction.result ![] ps

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

The qq Conj Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqConjGraph = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.QQConj.blueprint.resultDef

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.«term^⋀_» : Lean.ParserDescr

The «term^⋀ » 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.qqConj_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : qqConj 0 = qqVerum

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqConj_cons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (p ps : V) : qqConj (adjoin p ps) = qqAnd p (qqConj ps)

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

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

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqConj_semiformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n ps : V} : IsSemiformula L n (qqConj ps) ↔ ∀ i < len ps, IsSemiformula L n (nth ps i)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.len_le_conj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (ps : V) : len ps ≤ qqConj ps

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.QQDisj.blueprint : VecRec.Blueprint 0

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

Equations

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

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

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

Equations

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

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

The qq Disj construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqDisj ps = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.QQDisj.construction.result ![] ps

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

The qq Disj Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqDisjGraph = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.QQDisj.blueprint.resultDef

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.«term^⋁_» : Lean.ParserDescr

The «term^⋁ » 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.qqDisj_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : qqDisj 0 = qqFalsum

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqDisj_cons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (p ps : V) : qqDisj (adjoin p ps) = qqOr p (qqDisj ps)

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

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

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqDisj_semiformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n ps : V} : IsSemiformula L n (qqDisj ps) ↔ ∀ i < len ps, IsSemiformula L n (nth ps i)

Disjunction of sequential substution

disjSeqSubst w p k = subst (k ∷ w) p ^⋎ ⋯ ^⋎ subst (0 ∷ w) p ^⋎ ⊥

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.DisjSeqSubst.blueprint : PR.Blueprint 2

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

Equations

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

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

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

Equations

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

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

The disj Seq Subst 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.disjSeqSubst_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (w p : V) : disjSeqSubst w p 0 = qqFalsum

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.disjSeqSubst_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (w p k : V) : disjSeqSubst w p (k + 1) = qqOr (subst ℒₒᵣ (adjoin (numeral k) w) p) (disjSeqSubst w p k)

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.disjSeqSubstGraph : Σ₁.Semisentence 4

The disj Seq Subst 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.disjSeqSubst.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₃ disjSeqSubst via disjSeqSubstGraph

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

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.disjSeqSubst {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n m w p : V} (hw : IsSemitermVec ℒₒᵣ n m w) (hp : IsSemiformula ℒₒᵣ (n + 1) p) (k : V) : IsSemiformula ℒₒᵣ m (ObjectArithmetic.disjSeqSubst w p k)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substs_conj_disjSeqSubst {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n m l v w p : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) (hv : IsSemitermVec ℒₒᵣ m l v) (k : V) : subst ℒₒᵣ v (disjSeqSubst w p k) = disjSeqSubst (termSubstVec ℒₒᵣ n v w) p k

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.SubstItr.blueprint : PR.Blueprint 2

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

Equations

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

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

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

Equations

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

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

The subst Itr 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.substItr_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (w p : V) : substItr w p 0 = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substItr_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (w p k : V) : substItr w p (k + 1) = adjoin (subst ℒₒᵣ (adjoin (numeral k) w) p) (substItr w p k)

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substItrGraph : Σ₁.Semisentence 4

The subst Itr 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.substItr.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₃ substItr via substItrGraph

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

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.len_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (w p k : V) : len (substItr w p k) = k

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substItr_nth {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (w p k : V) {i : V} (hi : i < k) : nth (substItr w p k) i = subst ℒₒᵣ (adjoin (numeral (k - (i + 1))) w) p

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.substItrConj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m n w p : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) (k : V) : IsSemiformula ℒₒᵣ m (qqConj (ObjectArithmetic.substItr w p k))

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.substItrDisj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m n w p : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) (k : V) : IsSemiformula ℒₒᵣ m (qqDisj (ObjectArithmetic.substItr w p k))

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.neg_conj_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m n w p k : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) : neg ℒₒᵣ (qqConj (substItr w p k)) = qqDisj (substItr w (neg ℒₒᵣ p) k)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.neg_disj_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m n w p k : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) : neg ℒₒᵣ (qqDisj (substItr w p k)) = qqConj (substItr w (neg ℒₒᵣ p) k)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.shift_conj_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m n w p k : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) : shift ℒₒᵣ (qqConj (substItr w p k)) = qqConj (substItr (termShiftVec ℒₒᵣ n w) (shift ℒₒᵣ p) k)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.shift_disj_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m n w p k : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) : shift ℒₒᵣ (qqDisj (substItr w p k)) = qqDisj (substItr (termShiftVec ℒₒᵣ n w) (shift ℒₒᵣ p) k)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substs_conj_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v n m l w p k : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) (hv : IsSemitermVec ℒₒᵣ m l v) : subst ℒₒᵣ v (qqConj (substItr w p k)) = qqConj (substItr (termSubstVec ℒₒᵣ n v w) p k)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substs_disj_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v n m l w p k : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) (hv : IsSemitermVec ℒₒᵣ m l v) : subst ℒₒᵣ v (qqDisj (substItr w p k)) = qqDisj (substItr (termSubstVec ℒₒᵣ n v w) p k)

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

The qq Verums construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

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

The qq Verums 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.le_qqVerums {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (k : V) : k ≤ qqVerums k

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

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

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.qqVerums {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : V} (k : V) : IsSemiformula L n (qqVerums k)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqVerums_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : qqVerums 0 = qqVerum

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.qqVerums_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (k : V) : qqVerums (k + 1) = qqAnd qqVerum (qqVerums k)