Formalized Theory $\mathsf{R_0}$

@[reducible, inline]

abbrev LO.Arith.Formalized.LOR.Theory (V : Type u_1) [LO.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 2 < 1 + 1 + 1

TODO: move

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[reducible, inline]

abbrev LO.Arith.Formalized.oneAbbrev {V : Type u_1} [LO.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [LO.Arith.Formalized.R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) : T ⊢ LO.Arith.Language.Semiterm.equals t t

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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

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

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

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

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

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

Equations

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

noncomputable def LO.Arith.Formalized.TProof.nltNumeral {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [LO.Arith.Formalized.R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ LO.Arith.Language.Semiterm.notLessThan t (LO.Arith.Formalized.typedNumeral 0 n) ⭤ (LO.Arith.Formalized.tSubstItr (LO.Arith.Language.Semiterm.sing t) ((LO.Arith.bv 1 ⋯).notEquals (LO.Arith.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [LO.Arith.Formalized.R₀Theory T] {n : V} {m : V} (h : n < m) : T ⊢ (LO.Arith.Formalized.typedNumeral 0 n).lessThan (LO.Arith.Formalized.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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : ⌜ℒₒᵣ⌝.TTheory) [LO.Arith.Formalized.R₀Theory T] {n : V} {m : V} (h : n < m) : T ⊢! (LO.Arith.Formalized.typedNumeral 0 n).lessThan (LO.Arith.Formalized.typedNumeral 0 m)

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

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

Equations

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

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

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

Equations

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

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