Formalized Theory $\mathsf{R_0}$

@[reducible, inline]

abbrev LO.Arith.Formalized.LOR.Theory (V : Type u_1) [ORingStruc V] : Type u_1

Equations

• LO.Arith.Formalized.LOR.Theory V = ⌜ℒₒᵣ⌝.Theory

@[simp]

theorem LO.Arith.Formalized.two_lt_three {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 2 < 1 + 1 + 1

TODO: move

@[simp]

theorem LO.Arith.Formalized.two_lt_four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 2 < 1 + 1 + 1 + 1

@[simp]

theorem LO.Arith.Formalized.three_lt_four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 3 < 1 + 1 + 1 + 1

@[simp]

theorem LO.Arith.Formalized.two_sub_one_eq_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 2 - 1 = 1

@[simp]

theorem LO.Arith.Formalized.three_sub_one_eq_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 3 - 1 = 2

class LO.Arith.Formalized.R₀Theory {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) : Type u_1

• refl : T ⊢ ((bv 0 ⋯).equals (bv 0 ⋯)).all
• replace (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) : T ⊢ ((bv 1 ⋯).equals (bv 0 ⋯) ➝ φ^/[(bv 1 ⋯).sing] ➝ φ^/[(bv 0 ⋯).sing]).all.all
• add (n m : V) : T ⊢ (typedNumeral 0 n + typedNumeral 0 m).equals (typedNumeral 0 (n + m))
• mul (n m : V) : T ⊢ (typedNumeral 0 n * typedNumeral 0 m).equals (typedNumeral 0 (n * m))
• ne {n m : V} : n ≠ m → T ⊢ (typedNumeral 0 n).notEquals (typedNumeral 0 m)
• ltNumeral (n : V) : T ⊢ ((bv 0 ⋯).lessThan (typedNumeral (0 + 1) n) ⭤ (tSubstItr (bv 0 ⋯).sing ((bv 1 ⋯).equals (bv 0 ⋯)) n).disj).all

@[reducible, inline]

abbrev LO.Arith.Formalized.oneAbbrev {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} : ⌜ℒₒᵣ⌝.Semiterm n

Equations

• LO.Arith.Formalized.oneAbbrev = LO.Arith.Formalized.typedNumeral n 1

def LO.Arith.Formalized.«term^1» : Lean.ParserDescr

Equations

• LO.Arith.Formalized.«term^1» = Lean.ParserDescr.node `LO.Arith.Formalized.«term^1» 1024 (Lean.ParserDescr.symbol "^1")

def LO.Arith.Formalized.TProof.eqRefl {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t t

Equations

• LO.Arith.Formalized.TProof.eqRefl T t = ⋯.mp (LO.Arith.Language.Theory.TProof.specialize LO.Arith.Formalized.R₀Theory.refl t)

theorem LO.Arith.Formalized.TProof.eq_refl! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t t

noncomputable def LO.Arith.Formalized.TProof.replace {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t u ➝ φ^/[Language.Semiterm.sing t] ➝ φ^/[Language.Semiterm.sing u]

Equations

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

theorem LO.Arith.Formalized.TProof.replace! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t u ➝ φ^/[Language.Semiterm.sing t] ➝ φ^/[Language.Semiterm.sing u]

def LO.Arith.Formalized.TProof.eqSymm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals t₂ t₁

Equations

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

theorem LO.Arith.Formalized.TProof.eq_symm! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals t₂ t₁

theorem LO.Arith.Formalized.TProof.eq_symm'! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {t₁ t₂ : ⌜ℒₒᵣ⌝.Term} (h : T ⊢! Language.Semiterm.equals t₁ t₂) : T ⊢! Language.Semiterm.equals t₂ t₁

def LO.Arith.Formalized.TProof.eqTrans {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals t₂ t₃ ➝ Language.Semiterm.equals t₁ t₃

Equations

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

theorem LO.Arith.Formalized.TProof.eq_trans! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals t₂ t₃ ➝ Language.Semiterm.equals t₁ t₃

noncomputable def LO.Arith.Formalized.TProof.addExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.equals (t₁ + u₁) (t₂ + u₂)

Equations

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

theorem LO.Arith.Formalized.TProof.add_ext! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.equals (t₁ + u₁) (t₂ + u₂)

noncomputable def LO.Arith.Formalized.TProof.mulExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.equals (t₁ * u₁) (t₂ * u₂)

Equations

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

theorem LO.Arith.Formalized.TProof.mul_ext! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.equals (t₁ * u₁) (t₂ * u₂)

noncomputable def LO.Arith.Formalized.TProof.eqExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.equals t₁ u₁ ➝ Language.Semiterm.equals t₂ u₂

Equations

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

theorem LO.Arith.Formalized.TProof.eq_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.equals t₁ u₁ ➝ Language.Semiterm.equals t₂ u₂

noncomputable def LO.Arith.Formalized.TProof.neExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.notEquals t₁ u₁ ➝ Language.Semiterm.notEquals t₂ u₂

Equations

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

theorem LO.Arith.Formalized.TProof.ne_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.notEquals t₁ u₁ ➝ Language.Semiterm.notEquals t₂ u₂

noncomputable def LO.Arith.Formalized.TProof.ltExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.lessThan t₁ u₁ ➝ Language.Semiterm.lessThan t₂ u₂

Equations

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

theorem LO.Arith.Formalized.TProof.lt_ext! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.lessThan t₁ u₁ ➝ Language.Semiterm.lessThan t₂ u₂

noncomputable def LO.Arith.Formalized.TProof.nltExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.notLessThan t₁ u₁ ➝ Language.Semiterm.notLessThan t₂ u₂

Equations

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

theorem LO.Arith.Formalized.TProof.nlt_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t₁ t₂ ➝ Language.Semiterm.equals u₁ u₂ ➝ Language.Semiterm.notLessThan t₁ u₁ ➝ Language.Semiterm.notLessThan t₂ u₂

noncomputable def LO.Arith.Formalized.TProof.ballReplace {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t u ➝ Language.Semiformula.ball t φ ➝ Language.Semiformula.ball u φ

Equations

• LO.Arith.Formalized.TProof.ballReplace T φ t u = ⋯.mp (LO.Arith.Formalized.TProof.replace T (LO.Arith.Language.Semiformula.ball (LO.Arith.bv 0 ⋯) (φ^/[(LO.Arith.bv 0 ⋯).sing])) t u)

theorem LO.Arith.Formalized.TProof.ball_replace! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t u ➝ Language.Semiformula.ball t φ ➝ Language.Semiformula.ball u φ

noncomputable def LO.Arith.Formalized.TProof.bexReplace {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢ Language.Semiterm.equals t u ➝ Language.Semiformula.bex t φ ➝ Language.Semiformula.bex u φ

Equations

• LO.Arith.Formalized.TProof.bexReplace T φ t u = ⋯.mp (LO.Arith.Formalized.TProof.replace T (LO.Arith.Language.Semiformula.bex (LO.Arith.bv 0 ⋯) (φ^/[(LO.Arith.bv 0 ⋯).sing])) t u)

theorem LO.Arith.Formalized.TProof.bex_replace! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) : T ⊢! Language.Semiterm.equals t u ➝ Language.Semiformula.bex t φ ➝ Language.Semiformula.bex u φ

def LO.Arith.Formalized.TProof.eqComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n = m) : T ⊢ (typedNumeral 0 n).equals (typedNumeral 0 m)

Equations

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

theorem LO.Arith.Formalized.TProof.eq_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n = m) : T ⊢! (typedNumeral 0 n).equals (typedNumeral 0 m)

def LO.Arith.Formalized.TProof.addComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (n m : V) : T ⊢ (typedNumeral 0 n + typedNumeral 0 m).equals (typedNumeral 0 (n + m))

Equations

• LO.Arith.Formalized.TProof.addComplete T n m = LO.Arith.Formalized.R₀Theory.add n m

theorem LO.Arith.Formalized.TProof.add_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (n m : V) : T ⊢! (typedNumeral 0 n + typedNumeral 0 m).equals (typedNumeral 0 (n + m))

def LO.Arith.Formalized.TProof.mulComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (n m : V) : T ⊢ (typedNumeral 0 n * typedNumeral 0 m).equals (typedNumeral 0 (n * m))

Equations

• LO.Arith.Formalized.TProof.mulComplete T n m = LO.Arith.Formalized.R₀Theory.mul n m

theorem LO.Arith.Formalized.TProof.mul_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (n m : V) : T ⊢! (typedNumeral 0 n * typedNumeral 0 m).equals (typedNumeral 0 (n * m))

def LO.Arith.Formalized.TProof.neComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n ≠ m) : T ⊢ (typedNumeral 0 n).notEquals (typedNumeral 0 m)

Equations

• LO.Arith.Formalized.TProof.neComplete T h = LO.Arith.Formalized.R₀Theory.ne h

theorem LO.Arith.Formalized.TProof.ne_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n ≠ m) : T ⊢! (typedNumeral 0 n).notEquals (typedNumeral 0 m)

def LO.Arith.Formalized.TProof.ltNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ Language.Semiterm.lessThan t (typedNumeral 0 n) ⭤ (tSubstItr (Language.Semiterm.sing t) ((bv 1 ⋯).equals (bv 0 ⋯)) n).disj

Equations

• LO.Arith.Formalized.TProof.ltNumeral T t n = ⋯.mp (LO.Arith.Language.Theory.TProof.specialize (LO.Arith.Formalized.R₀Theory.ltNumeral n) t)

noncomputable def LO.Arith.Formalized.TProof.nltNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ Language.Semiterm.notLessThan t (typedNumeral 0 n) ⭤ (tSubstItr (Language.Semiterm.sing t) ((bv 1 ⋯).notEquals (bv 0 ⋯)) n).conj

Equations

• LO.Arith.Formalized.TProof.nltNumeral T t n = ⋯.mp (LO.System.negReplaceIff' (LO.Arith.Formalized.TProof.ltNumeral T t n))

def LO.Arith.Formalized.TProof.ltComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n < m) : T ⊢ (typedNumeral 0 n).lessThan (typedNumeral 0 m)

Equations

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

theorem LO.Arith.Formalized.TProof.lt_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n < m) : T ⊢! (typedNumeral 0 n).lessThan (typedNumeral 0 m)

noncomputable def LO.Arith.Formalized.TProof.nltComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : m ≤ n) : T ⊢ (typedNumeral 0 n).notLessThan (typedNumeral 0 m)

Equations

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

theorem LO.Arith.Formalized.TProof.nlt_complete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : m ≤ n) : T ⊢! (typedNumeral 0 n).notLessThan (typedNumeral 0 m)

noncomputable def LO.Arith.Formalized.TProof.ballIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) (bs : (i : V) → i < n → T ⊢ φ^/[(typedNumeral 0 i).sing]) : T ⊢ Language.Semiformula.ball (typedNumeral 0 n) φ

Equations

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

theorem LO.Arith.Formalized.TProof.ball_intro! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) (bs : ∀ i < n, T ⊢! φ^/[(typedNumeral 0 i).sing]) : T ⊢! Language.Semiformula.ball (typedNumeral 0 n) φ

noncomputable def LO.Arith.Formalized.TProof.bexIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i : V} (hi : i < n) (b : T ⊢ φ^/[(typedNumeral 0 i).sing]) : T ⊢ Language.Semiformula.bex (typedNumeral 0 n) φ

Equations

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

theorem LO.Arith.Formalized.TProof.bex_intro! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i : V} (hi : i < n) (b : T ⊢! φ^/[(typedNumeral 0 i).sing]) : T ⊢! Language.Semiformula.bex (typedNumeral 0 n) φ