Typed Formalized Semiformula/Formula

theorem LO.Arith.sub_succ_lt_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : b < a) : a - (b + 1) < a

theorem LO.Arith.sub_succ_lt_selfs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : b < a) : a - (a - (b + 1) + 1) = b

structure LO.Arith.Language.Semiformula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) : Type u_1

• val : V
• prop : L.IsSemiformula n self.val

@[simp]

theorem LO.Arith.Language.Semiformula.prop {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (self : L.Semiformula n) : L.IsSemiformula n self.val

@[reducible, inline]

abbrev LO.Arith.Language.Formula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : Type u_1

Equations

• L.Formula = L.Semiformula 0

@[simp]

theorem LO.Arith.Language.Semiformula.isUFormula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) : L.IsUFormula p.val

def LO.Arith.instLogicalConnectiveSemiformula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} : LO.LogicalConnective (L.Semiformula n)

Equations

• LO.Arith.instLogicalConnectiveSemiformula = LO.LogicalConnective.mk

def LO.Arith.Language.Semiformula.cast {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {n' : V} (p : L.Semiformula n) (eq : autoParam (n = n') _auto✝) : L.Semiformula n'

Equations

• p.cast eq = eq ▸ p

def LO.Arith.verums {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (k : V) : L.Semiformula n

Equations

• LO.Arith.verums k = { val := LO.Arith.qqVerums k, prop := ⋯ }

@[simp]

theorem LO.Arith.Language.Semiformula.val_cast {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {n' : V} (p : L.Semiformula n) (eq : n = n') : (p.cast eq).val = p.val

def LO.Arith.Language.Semiformula.all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) : L.Semiformula n

Equations

• p.all = { val := LO.Arith.qqAll p.val, prop := ⋯ }

def LO.Arith.Language.Semiformula.ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) : L.Semiformula n

Equations

• p.ex = { val := LO.Arith.qqEx p.val, prop := ⋯ }

@[simp]

theorem LO.Arith.Language.Semiformula.val_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} : ⊤.val = LO.Arith.qqVerum

@[simp]

theorem LO.Arith.Language.Semiformula.val_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} : ⊥.val = LO.Arith.qqFalsum

@[simp]

theorem LO.Arith.Language.Semiformula.val_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : (p ⋏ q).val = LO.Arith.qqAnd p.val q.val

@[simp]

theorem LO.Arith.Language.Semiformula.val_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : (p ⋎ q).val = LO.Arith.qqOr p.val q.val

@[simp]

theorem LO.Arith.Language.Semiformula.val_neg {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) : (∼p).val = L.neg p.val

@[simp]

theorem LO.Arith.Language.Semiformula.val_imp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : (p ➝ q).val = p.val ^→[L] q.val

@[simp]

theorem LO.Arith.Language.Semiformula.val_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) : p.all.val = LO.Arith.qqAll p.val

@[simp]

theorem LO.Arith.Language.Semiformula.val_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) : p.ex.val = LO.Arith.qqEx p.val

@[simp]

theorem LO.Arith.Language.Semiformula.val_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : (p ⭤ q).val = L.iff p.val q.val

theorem LO.Arith.Language.Semiformula.val_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : L.Semiformula n} {q : L.Semiformula n} : p.val = q.val ↔ p = q

theorem LO.Arith.Language.Semiformula.ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : L.Semiformula n} {q : L.Semiformula n} (h : p.val = q.val) : p = q

theorem LO.Arith.Language.Semiformula.ext_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : L.Semiformula n} {q : L.Semiformula n} : p = q ↔ p.val = q.val

@[simp]

theorem LO.Arith.Language.Semiformula.and_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p₁ : L.Semiformula n} {p₂ : L.Semiformula n} {q₁ : L.Semiformula n} {q₂ : L.Semiformula n} : p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[simp]

theorem LO.Arith.Language.Semiformula.or_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p₁ : L.Semiformula n} {p₂ : L.Semiformula n} {q₁ : L.Semiformula n} {q₂ : L.Semiformula n} : p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[simp]

theorem LO.Arith.Language.Semiformula.all_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : L.Semiformula (n + 1)} {q : L.Semiformula (n + 1)} : p.all = q.all ↔ p = q

@[simp]

theorem LO.Arith.Language.Semiformula.ex_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : L.Semiformula (n + 1)} {q : L.Semiformula (n + 1)} : p.ex = q.ex ↔ p = q

@[simp]

theorem LO.Arith.Language.Semiformula.val_verums {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} : (LO.Arith.verums k).val = LO.Arith.qqVerums k

@[simp]

theorem LO.Arith.Language.Semiformula.verums_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} : LO.Arith.verums 0 = ⊤

@[simp]

theorem LO.Arith.Language.Semiformula.verums_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (k : V) : LO.Arith.verums (k + 1) = ⊤ ⋏ LO.Arith.verums k

@[simp]

theorem LO.Arith.Language.Semiformula.neg_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} : ∼⊤ = ⊥

@[simp]

theorem LO.Arith.Language.Semiformula.neg_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} : ∼⊥ = ⊤

@[simp]

theorem LO.Arith.Language.Semiformula.neg_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : ∼(p ⋏ q) = ∼p ⋎ ∼q

@[simp]

theorem LO.Arith.Language.Semiformula.neg_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : ∼(p ⋎ q) = ∼p ⋏ ∼q

@[simp]

theorem LO.Arith.Language.Semiformula.neg_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) : ∼p.all = (∼p).ex

@[simp]

theorem LO.Arith.Language.Semiformula.neg_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) : ∼p.ex = (∼p).all

theorem LO.Arith.Language.Semiformula.imp_def {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : p ➝ q = ∼p ⋎ q

@[simp]

theorem LO.Arith.Language.Semiformula.neg_neg {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) : ∼∼p = p

def LO.Arith.Language.Semiformula.shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) : L.Semiformula n

Equations

• p.shift = { val := L.shift p.val, prop := ⋯ }

def LO.Arith.Language.Semiformula.substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (p : L.Semiformula n) (w : L.SemitermVec n m) : L.Semiformula m

Equations

• p^/[w] = { val := L.substs w.val p.val, prop := ⋯ }

@[simp]

theorem LO.Arith.Language.Semiformula.val_shift {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) : p.shift.val = L.shift p.val

@[simp]

theorem LO.Arith.Language.Semiformula.val_substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (p : L.Semiformula n) (w : L.SemitermVec n m) : p^/[w].val = L.substs w.val p.val

@[simp]

theorem LO.Arith.Language.Semiformula.shift_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} : ⊤.shift = ⊤

@[simp]

theorem LO.Arith.Language.Semiformula.shift_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} : ⊥.shift = ⊥

@[simp]

theorem LO.Arith.Language.Semiformula.shift_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : (p ⋏ q).shift = p.shift ⋏ q.shift

@[simp]

theorem LO.Arith.Language.Semiformula.shift_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : (p ⋎ q).shift = p.shift ⋎ q.shift

@[simp]

theorem LO.Arith.Language.Semiformula.shift_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) : p.all.shift = p.shift.all

@[simp]

theorem LO.Arith.Language.Semiformula.shift_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) : p.ex.shift = p.shift.ex

@[simp]

theorem LO.Arith.Language.Semiformula.neg_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : L.Semiformula n} {q : L.Semiformula n} : ∼p = ∼q ↔ p = q

@[simp]

theorem LO.Arith.Language.Semiformula.imp_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p₁ : L.Semiformula n} {p₂ : L.Semiformula n} {q₁ : L.Semiformula n} {q₂ : L.Semiformula n} : p₁ ➝ p₂ = q₁ ➝ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[simp]

theorem LO.Arith.Language.Semiformula.shift_neg {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) : (∼p).shift = ∼p.shift

@[simp]

theorem LO.Arith.Language.Semiformula.shift_imp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) (q : L.Semiformula n) : (p ➝ q).shift = p.shift ➝ q.shift

@[simp]

theorem LO.Arith.Language.Semiformula.substs_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) : ⊤^/[w] = ⊤

@[simp]

theorem LO.Arith.Language.Semiformula.substs_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) : ⊥^/[w] = ⊥

@[simp]

theorem LO.Arith.Language.Semiformula.substs_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (p : L.Semiformula n) (q : L.Semiformula n) : (p ⋏ q)^/[w] = p^/[w] ⋏ q^/[w]

@[simp]

theorem LO.Arith.Language.Semiformula.substs_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (p : L.Semiformula n) (q : L.Semiformula n) : (p ⋎ q)^/[w] = p^/[w] ⋎ q^/[w]

@[simp]

theorem LO.Arith.Language.Semiformula.substs_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (p : L.Semiformula (n + 1)) : p.all^/[w] = p^/[w.q].all

@[simp]

theorem LO.Arith.Language.Semiformula.substs_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (p : L.Semiformula (n + 1)) : p.ex^/[w] = p^/[w.q].ex

@[simp]

theorem LO.Arith.Language.Semiformula.substs_neg {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (p : L.Semiformula n) : (∼p)^/[w] = ∼p^/[w]

@[simp]

theorem LO.Arith.Language.Semiformula.substs_imp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (p : L.Semiformula n) (q : L.Semiformula n) : (p ➝ q)^/[w] = p^/[w] ➝ q^/[w]

@[simp]

theorem LO.Arith.Language.Semiformula.substs_imply {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (p : L.Semiformula n) (q : L.Semiformula n) : (p ⭤ q)^/[w] = p^/[w] ⭤ q^/[w]

def LO.Arith.«term_^/[_]» : Lean.TrailingParserDescr

Equations

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

structure LO.Arith.Language.SemiformulaVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (n : V) : Type u_1

• val : V
• prop : ∀ i < LO.Arith.len self.val, L.IsSemiformula n (LO.Arith.nth self.val i)

theorem LO.Arith.Language.SemiformulaVec.prop {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (self : LO.Arith.Language.SemiformulaVec n) (i : V) : i < LO.Arith.len self.val → L.IsSemiformula n (LO.Arith.nth self.val i)

def LO.Arith.Language.SemiformulaVec.conj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : LO.Arith.Language.SemiformulaVec n) : L.Semiformula n

Equations

• ps.conj = { val := LO.Arith.qqConj ps.val, prop := ⋯ }

def LO.Arith.Language.SemiformulaVec.disj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : LO.Arith.Language.SemiformulaVec n) : L.Semiformula n

Equations

• ps.disj = { val := LO.Arith.qqDisj ps.val, prop := ⋯ }

def LO.Arith.Language.SemiformulaVec.nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : LO.Arith.Language.SemiformulaVec n) (i : V) (hi : i < LO.Arith.len ps.val) : L.Semiformula n

Equations

• ps.nth i hi = { val := LO.Arith.nth ps.val i, prop := ⋯ }

@[simp]

theorem LO.Arith.Language.SemiformulaVec.val_conj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : LO.Arith.Language.SemiformulaVec n) : ps.conj.val = LO.Arith.qqConj ps.val

@[simp]

theorem LO.Arith.Language.SemiformulaVec.val_disj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : LO.Arith.Language.SemiformulaVec n) : ps.disj.val = LO.Arith.qqDisj ps.val

@[simp]

theorem LO.Arith.Language.SemiformulaVec.val_nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : LO.Arith.Language.SemiformulaVec n) (i : V) (hi : i < LO.Arith.len ps.val) : (ps.nth i hi).val = LO.Arith.nth ps.val i

theorem LO.Arith.Language.TSemifromula.subst_eq_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (w : L.SemitermVec n n) (p : L.Semiformula n) (H : ∀ (i : V) (hi : i < n), w.nth i hi = L.bvar i hi) : p^/[w] = p

@[simp]

theorem LO.Arith.Language.TSemifromula.subst_eq_self₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) : p^/[(L.bvar 0 ⋯).sing] = p

@[simp]

theorem LO.Arith.Language.TSemifromula.subst_nil_eq_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : L.Semiformula 0} (w : L.SemitermVec 0 0) : p^/[w] = p

theorem LO.Arith.Language.TSemifromula.shift_substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} (w : L.SemitermVec n m) (p : L.Semiformula n) : p^/[w].shift = p.shift^/[w.shift]

theorem LO.Arith.Language.TSemifromula.substs_substs {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {m : V} {l : V} (v : L.SemitermVec m l) (w : L.SemitermVec n m) (p : L.Semiformula n) : (p^/[w])^/[v] = p^/[w.substs v]

def LO.Arith.Language.Semiterm.equals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) : ⌜ℒₒᵣ⌝.Semiformula n

Equations

• t.equals u = { val := t.val ^= u.val, prop := ⋯ }

def LO.Arith.Language.Semiterm.notEquals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) : ⌜ℒₒᵣ⌝.Semiformula n

Equations

• t.notEquals u = { val := t.val ^≠ u.val, prop := ⋯ }

def LO.Arith.Language.Semiterm.lessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) : ⌜ℒₒᵣ⌝.Semiformula n

Equations

• t.lessThan u = { val := t.val ^< u.val, prop := ⋯ }

def LO.Arith.Language.Semiterm.notLessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) : ⌜ℒₒᵣ⌝.Semiformula n

Equations

• t.notLessThan u = { val := t.val ^≮ u.val, prop := ⋯ }

def LO.Arith.«term_='_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_='_» = Lean.ParserDescr.trailingNode `LO.Arith.term_='_ 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =' ") (Lean.ParserDescr.cat `term 76))

def LO.Arith.«term_≠'_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_≠'_» = Lean.ParserDescr.trailingNode `LO.Arith.term_≠'_ 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠' ") (Lean.ParserDescr.cat `term 76))

def LO.Arith.«term_<'_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_<'_» = Lean.ParserDescr.trailingNode `LO.Arith.term_<'_ 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <' ") (Lean.ParserDescr.cat `term 76))

def LO.Arith.«term_≮'_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_≮'_» = Lean.ParserDescr.trailingNode `LO.Arith.term_≮'_ 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≮' ") (Lean.ParserDescr.cat `term 76))

def LO.Arith.Language.Semiformula.ball {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : ⌜ℒₒᵣ⌝.Semiformula n

Equations

• LO.Arith.Language.Semiformula.ball t p = ((⌜ℒₒᵣ⌝.bvar 0 ⋯).notLessThan t.bShift ⋎ p).all

def LO.Arith.Language.Semiformula.bex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : ⌜ℒₒᵣ⌝.Semiformula n

Equations

• LO.Arith.Language.Semiformula.bex t p = ((⌜ℒₒᵣ⌝.bvar 0 ⋯).lessThan t.bShift ⋏ p).ex

@[simp]

theorem LO.Arith.Formalized.val_equals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) : (t.equals u).val = t.val ^= u.val

@[simp]

theorem LO.Arith.Formalized.val_notEquals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) : (t.notEquals u).val = t.val ^≠ u.val

@[simp]

theorem LO.Arith.Formalized.val_lessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) : (t.lessThan u).val = t.val ^< u.val

@[simp]

theorem LO.Arith.Formalized.val_notLessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (u : ⌜ℒₒᵣ⌝.Semiterm n) : (t.notLessThan u).val = t.val ^≮ u.val

@[simp]

theorem LO.Arith.Formalized.equals_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ : ⌜ℒₒᵣ⌝.Semiterm n} {t₂ : ⌜ℒₒᵣ⌝.Semiterm n} {u₁ : ⌜ℒₒᵣ⌝.Semiterm n} {u₂ : ⌜ℒₒᵣ⌝.Semiterm n} : t₁.equals u₁ = t₂.equals u₂ ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem LO.Arith.Formalized.notequals_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ : ⌜ℒₒᵣ⌝.Semiterm n} {t₂ : ⌜ℒₒᵣ⌝.Semiterm n} {u₁ : ⌜ℒₒᵣ⌝.Semiterm n} {u₂ : ⌜ℒₒᵣ⌝.Semiterm n} : t₁.notEquals u₁ = t₂.notEquals u₂ ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem LO.Arith.Formalized.lessThan_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ : ⌜ℒₒᵣ⌝.Semiterm n} {t₂ : ⌜ℒₒᵣ⌝.Semiterm n} {u₁ : ⌜ℒₒᵣ⌝.Semiterm n} {u₂ : ⌜ℒₒᵣ⌝.Semiterm n} : t₁.lessThan u₁ = t₂.lessThan u₂ ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem LO.Arith.Formalized.notLessThan_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ : ⌜ℒₒᵣ⌝.Semiterm n} {t₂ : ⌜ℒₒᵣ⌝.Semiterm n} {u₁ : ⌜ℒₒᵣ⌝.Semiterm n} {u₂ : ⌜ℒₒᵣ⌝.Semiterm n} : t₁.notLessThan u₁ = t₂.notLessThan u₂ ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem LO.Arith.Formalized.neg_equals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : ∼t₁.equals t₂ = t₁.notEquals t₂

@[simp]

theorem LO.Arith.Formalized.neg_notEquals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : ∼t₁.notEquals t₂ = t₁.equals t₂

@[simp]

theorem LO.Arith.Formalized.neg_lessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : ∼t₁.lessThan t₂ = t₁.notLessThan t₂

@[simp]

theorem LO.Arith.Formalized.neg_notLessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : ∼t₁.notLessThan t₂ = t₁.lessThan t₂

@[simp]

theorem LO.Arith.Formalized.shift_equals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁.equals t₂).shift = t₁.shift.equals t₂.shift

@[simp]

theorem LO.Arith.Formalized.shift_notEquals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁.notEquals t₂).shift = t₁.shift.notEquals t₂.shift

@[simp]

theorem LO.Arith.Formalized.shift_lessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁.lessThan t₂).shift = t₁.shift.lessThan t₂.shift

@[simp]

theorem LO.Arith.Formalized.shift_notLessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁.notLessThan t₂).shift = t₁.shift.notLessThan t₂.shift

@[simp]

theorem LO.Arith.Formalized.substs_equals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁.equals t₂)^/[w] = t₁^ᵗ/[w].equals (t₂^ᵗ/[w])

@[simp]

theorem LO.Arith.Formalized.substs_notEquals {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁.notEquals t₂)^/[w] = t₁^ᵗ/[w].notEquals (t₂^ᵗ/[w])

@[simp]

theorem LO.Arith.Formalized.substs_lessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁.lessThan t₂)^/[w] = t₁^ᵗ/[w].lessThan (t₂^ᵗ/[w])

@[simp]

theorem LO.Arith.Formalized.substs_notLessThan {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ : ⌜ℒₒᵣ⌝.Semiterm n) (t₂ : ⌜ℒₒᵣ⌝.Semiterm n) : (t₁.notLessThan t₂)^/[w] = t₁^ᵗ/[w].notLessThan (t₂^ᵗ/[w])

@[simp]

theorem LO.Arith.Formalized.val_ball {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : (LO.Arith.Language.Semiformula.ball t p).val = LO.Arith.qqAll (LO.Arith.qqOr (LO.Arith.qqBvar 0 ^≮ ⌜ℒₒᵣ⌝.termBShift t.val) p.val)

@[simp]

theorem LO.Arith.Formalized.val_bex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : (LO.Arith.Language.Semiformula.bex t p).val = LO.Arith.qqEx (LO.Arith.qqAnd (LO.Arith.qqBvar 0 ^< ⌜ℒₒᵣ⌝.termBShift t.val) p.val)

theorem LO.Arith.Formalized.neg_ball {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : ∼LO.Arith.Language.Semiformula.ball t p = LO.Arith.Language.Semiformula.bex t (∼p)

theorem LO.Arith.Formalized.neg_bex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : ∼LO.Arith.Language.Semiformula.bex t p = LO.Arith.Language.Semiformula.ball t (∼p)

@[simp]

theorem LO.Arith.Formalized.shifts_ball {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : (LO.Arith.Language.Semiformula.ball t p).shift = LO.Arith.Language.Semiformula.ball t.shift p.shift

@[simp]

theorem LO.Arith.Formalized.shifts_bex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : (LO.Arith.Language.Semiformula.bex t p).shift = LO.Arith.Language.Semiformula.bex t.shift p.shift

@[simp]

theorem LO.Arith.Formalized.substs_ball {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : (LO.Arith.Language.Semiformula.ball t p)^/[w] = LO.Arith.Language.Semiformula.ball (t^ᵗ/[w]) (p^/[w.q])

@[simp]

theorem LO.Arith.Formalized.substs_bex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : (LO.Arith.Language.Semiformula.bex t p)^/[w] = LO.Arith.Language.Semiformula.bex (t^ᵗ/[w]) (p^/[w.q])

def LO.Arith.Formalized.tSubstItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) : LO.Arith.Language.SemiformulaVec m

Equations

• LO.Arith.Formalized.tSubstItr w p k = { val := LO.Arith.Formalized.substItr w.val p.val k, prop := ⋯ }

@[simp]

theorem LO.Arith.Formalized.val_tSubstItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) : (LO.Arith.Formalized.tSubstItr w p k).val = LO.Arith.Formalized.substItr w.val p.val k

@[simp]

theorem LO.Arith.Formalized.len_tSubstItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) : LO.Arith.len (LO.Arith.Formalized.tSubstItr w p k).val = k

theorem LO.Arith.Formalized.nth_tSubstItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) {i : V} (hi : i < k) : (LO.Arith.Formalized.tSubstItr w p k).nth i ⋯ = p^/[(LO.Arith.Formalized.typedNumeral m (k - (i + 1))).cons w]

theorem LO.Arith.Formalized.nth_tSubstItr' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) {i : V} (hi : i < k) : (LO.Arith.Formalized.tSubstItr w p k).nth (k - (i + 1)) ⋯ = p^/[(LO.Arith.Formalized.typedNumeral m i).cons w]

@[simp]

theorem LO.Arith.Formalized.neg_conj_tSubstItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) : ∼(LO.Arith.Formalized.tSubstItr w p k).conj = (LO.Arith.Formalized.tSubstItr w (∼p) k).disj

@[simp]

theorem LO.Arith.Formalized.neg_disj_tSubstItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) : ∼(LO.Arith.Formalized.tSubstItr w p k).disj = (LO.Arith.Formalized.tSubstItr w (∼p) k).conj

@[simp]

theorem LO.Arith.Formalized.substs_conj_tSubstItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} {l : V} (v : ⌜ℒₒᵣ⌝.SemitermVec m l) (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) : (LO.Arith.Formalized.tSubstItr w p k).conj^/[v] = (LO.Arith.Formalized.tSubstItr (w.substs v) p k).conj

@[simp]

theorem LO.Arith.Formalized.substs_disj_tSubstItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {m : V} {l : V} (v : ⌜ℒₒᵣ⌝.SemitermVec m l) (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) : (LO.Arith.Formalized.tSubstItr w p k).disj^/[v] = (LO.Arith.Formalized.tSubstItr (w.substs v) p k).disj

theorem LO.Arith.Language.Semiformula.ball_eq_imp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) : LO.Arith.Language.Semiformula.ball t p = ((⌜ℒₒᵣ⌝.bvar 0 ⋯).lessThan t.bShift ➝ p).all