Arithmetization.ISigmaOne.Metamath.Formula.Functions

theorem LO.Arith.neg_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :

L.neg (LO.Arith.qqRel k R v) = LO.Arith.qqNRel k R v

source

@[simp]

theorem LO.Arith.neg_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :

L.neg (LO.Arith.qqNRel k R v) = LO.Arith.qqRel k R v

source

@[simp]

theorem LO.Arith.neg_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

L.neg LO.Arith.qqVerum = LO.Arith.qqFalsum

source

@[simp]

theorem LO.Arith.neg_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

L.neg LO.Arith.qqFalsum = LO.Arith.qqVerum

source

@[simp]

theorem LO.Arith.neg_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :

L.neg (LO.Arith.qqAnd p q) = LO.Arith.qqOr (L.neg p) (L.neg q)

source

@[simp]

theorem LO.Arith.neg_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :

L.neg (LO.Arith.qqOr p q) = LO.Arith.qqAnd (L.neg p) (L.neg q)

source

@[simp]

theorem LO.Arith.neg_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :

L.neg (LO.Arith.qqAll p) = LO.Arith.qqEx (L.neg p)

source

@[simp]

theorem LO.Arith.neg_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :

L.neg (LO.Arith.qqEx p) = LO.Arith.qqAll (L.neg p)

source

theorem LO.Arith.neg_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {x : V} (h : ¬L.IsUFormula x) :

L.neg x = 0

source

theorem LO.Arith.Language.IsUFormula.neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :

L.IsUFormula p → L.IsUFormula (L.neg p)

source

@[simp]

theorem LO.Arith.Language.IsUFormula.bv_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :

L.IsUFormula p → L.bv (L.neg p) = L.bv p

source

@[simp]

theorem LO.Arith.Language.IsUFormula.neg_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :

L.IsUFormula p → L.neg (L.neg p) = p

source

@[simp]

theorem LO.Arith.Language.IsUFormula.neg_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :

L.IsUFormula (L.neg p) ↔ L.IsUFormula p

source

@[simp]

theorem LO.Arith.Language.IsSemiformula.neg_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :

L.IsSemiformula n (L.neg p) ↔ L.IsSemiformula n p

source

theorem LO.Arith.Language.IsSemiformula.neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :

L.IsSemiformula n p → L.IsSemiformula n (L.neg p)

Alias of the reverse direction of LO.Arith.Language.IsSemiformula.neg_iff.

source

theorem LO.Arith.Language.IsSemiformula.elim_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :

L.IsSemiformula n (L.neg p) → L.IsSemiformula n p

Alias of the forward direction of LO.Arith.Language.IsSemiformula.neg_iff.

source

@[simp]

theorem LO.Arith.neg_inj_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :

L.neg p = L.neg q ↔ p = q

source

def LO.Arith.Language.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) (q : V) :

Equations

p ^→[L] q = LO.Arith.qqOr (L.neg p) q

Instances For

source

def LO.Arith.«term_^→[_]_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.Arith.Language.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) (q : V) :

Equations

L.iff p q = LO.Arith.qqAnd (p ^→[L] q) (q ^→[L] p)

Instances For

source

@[simp]

theorem LO.Arith.Language.IsUFormula.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} :

L.IsUFormula (p ^→[L] q) ↔ L.IsUFormula p ∧ L.IsUFormula q

source

@[simp]

theorem LO.Arith.Language.IsSemiformula.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {q : V} :

L.IsSemiformula n (p ^→[L] q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q

source

def LO.FirstOrder.Arith.LDef.impDef (pL : LO.FirstOrder.Arith.LDef) :

𝚺₁.Semisentence 3

Equations

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

source

theorem LO.Arith.Language.imp_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₂ L.imp via pL.impDef

source

instance LO.Arith.Language.imp_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₂ L.imp

Equations

⋯ = ⋯

source

instance LO.Arith.Language.imp_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₂ L.imp

Equations

⋯ = ⋯

source

@[simp]

theorem LO.Arith.Language.IsUFormula.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} :

L.IsUFormula (L.iff p q) ↔ L.IsUFormula p ∧ L.IsUFormula q

source

@[simp]

theorem LO.Arith.Language.IsSemiformula.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {q : V} :

L.IsSemiformula n (L.iff p q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q

source

@[simp]

theorem LO.Arith.lt_iff_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) (q : V) :

p < L.iff p q

source

@[simp]

theorem LO.Arith.lt_iff_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) (q : V) :

q < L.iff p q

source

def LO.FirstOrder.Arith.LDef.qqIffDef (pL : LO.FirstOrder.Arith.LDef) :

𝚺₁.Semisentence 3

Equations

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

source

theorem LO.Arith.Language.iff_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₂ L.iff via pL.qqIffDef

source

instance LO.Arith.Language.iff_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₂ L.iff

Equations

⋯ = ⋯

source

instance LO.Arith.Language.iff_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₂ L.iff

Equations

⋯ = ⋯

source

def LO.Arith.Shift.blueprint (pL : LO.FirstOrder.Arith.LDef) :

LO.Arith.Language.UformulaRec1.Blueprint pL

Equations

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

source

def LO.Arith.Shift.construction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

LO.Arith.Language.UformulaRec1.Construction V L (LO.Arith.Shift.blueprint pL)

Equations

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

source

def LO.Arith.Language.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :

Equations

L.shift p = (LO.Arith.Shift.construction L).result 0 p

Instances For

source

def LO.FirstOrder.Arith.LDef.shiftDef (pL : LO.FirstOrder.Arith.LDef) :

𝚺₁.Semisentence 2

Equations

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

source

theorem LO.Arith.Language.shift_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₁ L.shift via pL.shiftDef

source

instance LO.Arith.Language.shift_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₁ L.shift

Equations

⋯ = ⋯

source

instance LO.Arith.language.shift_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₁ L.shift

Equations

⋯ = ⋯

source

@[simp]

theorem LO.Arith.shift_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :

L.shift (LO.Arith.qqRel k R v) = LO.Arith.qqRel k R (L.termShiftVec k v)

source

@[simp]

theorem LO.Arith.shift_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :

L.shift (LO.Arith.qqNRel k R v) = LO.Arith.qqNRel k R (L.termShiftVec k v)

source

@[simp]

theorem LO.Arith.shift_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

L.shift LO.Arith.qqVerum = LO.Arith.qqVerum

source

@[simp]

theorem LO.Arith.shift_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

L.shift LO.Arith.qqFalsum = LO.Arith.qqFalsum

source

@[simp]

theorem LO.Arith.shift_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :

L.shift (LO.Arith.qqAnd p q) = LO.Arith.qqAnd (L.shift p) (L.shift q)

source

@[simp]

theorem LO.Arith.shift_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :

L.shift (LO.Arith.qqOr p q) = LO.Arith.qqOr (L.shift p) (L.shift q)

source

@[simp]

theorem LO.Arith.shift_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :

L.shift (LO.Arith.qqAll p) = LO.Arith.qqAll (L.shift p)

source

@[simp]

theorem LO.Arith.shift_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :

L.shift (LO.Arith.qqEx p) = LO.Arith.qqEx (L.shift p)

source

theorem LO.Arith.shift_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {x : V} (h : ¬L.IsUFormula x) :

L.shift x = 0

source

theorem LO.Arith.Language.IsUFormula.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :

L.IsUFormula p → L.IsUFormula (L.shift p)

source

theorem LO.Arith.Language.IsUFormula.bv_shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :

L.IsUFormula p → L.bv (L.shift p) = L.bv p

source

theorem LO.Arith.Language.IsSemiformula.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :

L.IsSemiformula n p → L.IsSemiformula n (L.shift p)

source

@[simp]

theorem LO.Arith.Language.IsSemiformula.shift_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} :

L.IsSemiformula n (L.shift p) ↔ L.IsSemiformula n p

source

theorem LO.Arith.shift_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} (hp : L.IsSemiformula n p) :

L.shift (L.neg p) = L.neg (L.shift p)

source

def LO.FirstOrder.Arith.LDef.qVecDef (pL : LO.FirstOrder.Arith.LDef) :

𝚺₁.Semisentence 2

Equations

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

source

theorem LO.Arith.Language.qVec_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₁ L.qVec via pL.qVecDef

source

instance LO.Arith.Language.qVec_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₁ L.qVec

Equations

⋯ = ⋯

source

instance LO.Arith.Language.qVec_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₁ L.qVec

Equations

⋯ = ⋯

source

def LO.Arith.Substs.blueprint (pL : LO.FirstOrder.Arith.LDef) :

LO.Arith.Language.UformulaRec1.Blueprint pL

Equations

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

source

def LO.Arith.Substs.construction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

LO.Arith.Language.UformulaRec1.Construction V L (LO.Arith.Substs.blueprint pL)

Equations

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

source

def LO.Arith.Language.substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (w : V) (p : V) :

Equations

L.substs w p = (LO.Arith.Substs.construction L).result w p

Instances For

source

def LO.FirstOrder.Arith.LDef.substsDef (pL : LO.FirstOrder.Arith.LDef) :

𝚺₁.Semisentence 3

Equations

pL.substsDef = (LO.Arith.Substs.blueprint pL).result

source

theorem LO.Arith.Language.substs_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₂ L.substs via pL.substsDef

source

instance LO.Arith.Language.substs_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₂ L.substs

Equations

⋯ = ⋯

source

instance LO.Arith.Language.substs_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₂ L.substs

Equations

⋯ = ⋯

source

@[simp]

theorem LO.Arith.substs_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :

L.substs w (LO.Arith.qqRel k R v) = LO.Arith.qqRel k R (L.termSubstVec k w v)

source

@[simp]

theorem LO.Arith.substs_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :

L.substs w (LO.Arith.qqNRel k R v) = LO.Arith.qqNRel k R (L.termSubstVec k w v)

source

@[simp]

theorem LO.Arith.substs_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (w : V) :

L.substs w LO.Arith.qqVerum = LO.Arith.qqVerum

source

@[simp]

theorem LO.Arith.substs_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (w : V) :

L.substs w LO.Arith.qqFalsum = LO.Arith.qqFalsum

source

@[simp]

theorem LO.Arith.substs_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :

L.substs w (LO.Arith.qqAnd p q) = LO.Arith.qqAnd (L.substs w p) (L.substs w q)

source

@[simp]

theorem LO.Arith.substs_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :

L.substs w (LO.Arith.qqOr p q) = LO.Arith.qqOr (L.substs w p) (L.substs w q)

source

@[simp]

theorem LO.Arith.substs_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {p : V} (hp : L.IsUFormula p) :

L.substs w (LO.Arith.qqAll p) = LO.Arith.qqAll (L.substs (L.qVec w) p)

source

@[simp]

theorem LO.Arith.substs_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {p : V} (hp : L.IsUFormula p) :

L.substs w (LO.Arith.qqEx p) = LO.Arith.qqEx (L.substs (L.qVec w) p)

source

theorem LO.Arith.isUFormula_subst_induction_sigma1 {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → V → Prop} (hP : 𝚺₁ -Relation₃ P) (hRel : ∀ (w k R v : V), L.Rel k R → L.IsUTermVec k v → P w (LO.Arith.qqRel k R v) (LO.Arith.qqRel k R (L.termSubstVec k w v))) (hNRel : ∀ (w k R v : V), L.Rel k R → L.IsUTermVec k v → P w (LO.Arith.qqNRel k R v) (LO.Arith.qqNRel k R (L.termSubstVec k w v))) (hverum : ∀ (w : V), P w LO.Arith.qqVerum LO.Arith.qqVerum) (hfalsum : ∀ (w : V), P w LO.Arith.qqFalsum LO.Arith.qqFalsum) (hand : ∀ (w p q : V), L.IsUFormula p → L.IsUFormula q → P w p (L.substs w p) → P w q (L.substs w q) → P w (LO.Arith.qqAnd p q) (LO.Arith.qqAnd (L.substs w p) (L.substs w q))) (hor : ∀ (w p q : V), L.IsUFormula p → L.IsUFormula q → P w p (L.substs w p) → P w q (L.substs w q) → P w (LO.Arith.qqOr p q) (LO.Arith.qqOr (L.substs w p) (L.substs w q))) (hall : ∀ (w p : V), L.IsUFormula p → P (L.qVec w) p (L.substs (L.qVec w) p) → P w (LO.Arith.qqAll p) (LO.Arith.qqAll (L.substs (L.qVec w) p))) (hex : ∀ (w p : V), L.IsUFormula p → P (L.qVec w) p (L.substs (L.qVec w) p) → P w (LO.Arith.qqEx p) (LO.Arith.qqEx (L.substs (L.qVec w) p))) {w : V} {p : V} :

L.IsUFormula p → P w p (L.substs w p)

source

theorem LO.Arith.semiformula_subst_induction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → V → V → Prop} (hP : 𝚺₁ -Relation₄ P) (hRel : ∀ (n w k R v : V), L.Rel k R → L.IsSemitermVec k n v → P n w (LO.Arith.qqRel k R v) (LO.Arith.qqRel k R (L.termSubstVec k w v))) (hNRel : ∀ (n w k R v : V), L.Rel k R → L.IsSemitermVec k n v → P n w (LO.Arith.qqNRel k R v) (LO.Arith.qqNRel k R (L.termSubstVec k w v))) (hverum : ∀ (n w : V), P n w LO.Arith.qqVerum LO.Arith.qqVerum) (hfalsum : ∀ (n w : V), P n w LO.Arith.qqFalsum LO.Arith.qqFalsum) (hand : ∀ (n w p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n w p (L.substs w p) → P n w q (L.substs w q) → P n w (LO.Arith.qqAnd p q) (LO.Arith.qqAnd (L.substs w p) (L.substs w q))) (hor : ∀ (n w p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n w p (L.substs w p) → P n w q (L.substs w q) → P n w (LO.Arith.qqOr p q) (LO.Arith.qqOr (L.substs w p) (L.substs w q))) (hall : ∀ (n w p : V), L.IsSemiformula (n + 1) p → P (n + 1) (L.qVec w) p (L.substs (L.qVec w) p) → P n w (LO.Arith.qqAll p) (LO.Arith.qqAll (L.substs (L.qVec w) p))) (hex : ∀ (n w p : V), L.IsSemiformula (n + 1) p → P (n + 1) (L.qVec w) p (L.substs (L.qVec w) p) → P n w (LO.Arith.qqEx p) (LO.Arith.qqEx (L.substs (L.qVec w) p))) {n : V} {p : V} {w : V} :

L.IsSemiformula n p → P n w p (L.substs w p)

source

@[simp]

theorem LO.Arith.Language.IsSemiformula.substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {m : V} {w : V} :

L.IsSemiformula n p → L.IsSemitermVec n m w → L.IsSemiformula m (L.substs w p)

source

theorem LO.Arith.substs_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {w : V} {x : V} (h : ¬L.IsUFormula x) :

L.substs w x = 0

source

theorem LO.Arith.substs_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {w : V} {n : V} {p : V} (hp : L.IsSemiformula n p) :

L.IsSemitermVec n m w → L.substs w (L.neg p) = L.neg (L.substs w p)

source

theorem LO.Arith.shift_substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {w : V} {n : V} {p : V} (hp : L.IsSemiformula n p) :

L.IsSemitermVec n m w → L.shift (L.substs w p) = L.substs (L.termShiftVec n w) (L.shift p)

source

theorem LO.Arith.substs_substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : V} {w : V} {l : V} {n : V} {v : V} {p : V} (hp : L.IsSemiformula l p) :

L.IsSemitermVec n m w → L.IsSemitermVec l n v → L.substs w (L.substs v p) = L.substs (L.termSubstVec l w v) p

source

theorem LO.Arith.subst_eq_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {n : V} {w : V} (hp : L.IsSemiformula n p) (hw : L.IsSemitermVec n n w) (H : ∀ i < n, LO.Arith.nth w i = LO.Arith.qqBvar i) :

L.substs w p = p

source

theorem LO.Arith.subst_eq_self₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsSemiformula 1 p) :

L.substs ?[LO.Arith.qqBvar 0] p = p

source

def LO.Arith.Language.substs₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (t : V) (u : V) :

Equations

L.substs₁ t u = L.substs ?[t] u

Instances For

source

def LO.FirstOrder.Arith.LDef.substs₁Def (pL : LO.FirstOrder.Arith.LDef) :

𝚺₁.Semisentence 3

Equations

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

source

theorem LO.Arith.Language.substs₁_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₂ L.substs₁ via pL.substs₁Def

source

instance LO.Arith.Language.substs₁_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₂ L.substs₁

Equations

⋯ = ⋯

source

instance LO.Arith.instBoldfaceFunction₂MkHAddNatOfNatSubsts₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₂ L.substs₁

Equations

⋯ = ⋯

source

theorem LO.Arith.Language.IsSemiformula.substs₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {t : V} {p : V} (ht : L.IsSemiterm n t) (hp : L.IsSemiformula 1 p) :

L.IsSemiformula n (L.substs₁ t p)

source

def LO.Arith.Language.free {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :

Equations

L.free p = L.substs₁ (LO.Arith.qqFvar 0) (L.shift p)

Instances For

source

def LO.FirstOrder.Arith.LDef.freeDef (pL : LO.FirstOrder.Arith.LDef) :

𝚺₁.Semisentence 2

Equations

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

source

theorem LO.Arith.Language.free_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₁ L.free via pL.freeDef

source

instance LO.Arith.Language.free_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] :

𝚺₁ -Function₁ L.free

Equations

⋯ = ⋯

source

instance LO.Arith.Language.free_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }-Function₁ L.free

Equations

⋯ = ⋯

source

@[simp]

theorem LO.Arith.Language.IsSemiformula.free {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsSemiformula 1 p) :

L.IsFormula (L.free p)

source

def LO.Arith.Formalized.qqEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

Equations

x ^= y = LO.Arith.qqRel 2 ↑LO.Arith.Formalized.eqIndex ?[x, y]

Instances For

LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqEQ

source

def LO.Arith.Formalized.qqNEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

Equations

x ^≠ y = LO.Arith.qqNRel 2 ↑LO.Arith.Formalized.eqIndex ?[x, y]

Instances For

LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNEQ

source

def LO.Arith.Formalized.qqLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

Equations

x ^< y = LO.Arith.qqRel 2 ↑LO.Arith.Formalized.ltIndex ?[x, y]

Instances For

LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqLT

source

def LO.Arith.Formalized.qqNLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

Equations

x ^≮ y = LO.Arith.qqNRel 2 ↑LO.Arith.Formalized.ltIndex ?[x, y]

Instances For

LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNLT

source

def LO.Arith.Formalized.«term_^=_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.Arith.Formalized.«term_^≠_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.Arith.Formalized.«term_^<_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.Arith.Formalized.«term_^≮_» :

Lean.TrailingParserDescr

Equations

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

source

@[simp]

theorem LO.Arith.Formalized.lt_qqEQ_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

x < x ^= y

source

@[simp]

theorem LO.Arith.Formalized.lt_qqEQ_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

y < x ^= y

source

@[simp]

theorem LO.Arith.Formalized.lt_qqLT_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

x < x ^< y

source

@[simp]

theorem LO.Arith.Formalized.lt_qqLT_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

y < x ^< y

source

@[simp]

theorem LO.Arith.Formalized.lt_qqNEQ_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

x < x ^≠ y

source

@[simp]

theorem LO.Arith.Formalized.lt_qqNEQ_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

y < x ^≠ y

source

@[simp]

theorem LO.Arith.Formalized.lt_qqNLT_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

x < x ^≮ y

source

@[simp]

theorem LO.Arith.Formalized.lt_qqNLT_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) :

y < x ^≮ y

source

def LO.FirstOrder.Arith.qqEQDef :

𝚺₁.Semisentence 3

Equations

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

source

def LO.FirstOrder.Arith.qqNEQDef :

𝚺₁.Semisentence 3

Equations

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

source

def LO.FirstOrder.Arith.qqLTDef :

𝚺₁.Semisentence 3

Equations

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

source

def LO.FirstOrder.Arith.qqNLTDef :

𝚺₁.Semisentence 3

Equations

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

source

theorem LO.Arith.Formalized.qqEQ_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₂ LO.Arith.Formalized.qqEQ via LO.FirstOrder.Arith.qqEQDef

source

theorem LO.Arith.Formalized.qqNEQ_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₂ LO.Arith.Formalized.qqNEQ via LO.FirstOrder.Arith.qqNEQDef

source

theorem LO.Arith.Formalized.qqLT_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₂ LO.Arith.Formalized.qqLT via LO.FirstOrder.Arith.qqLTDef

source

theorem LO.Arith.Formalized.qqNLT_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :

𝚺₁ -Function₂ LO.Arith.Formalized.qqNLT via LO.FirstOrder.Arith.qqNLTDef

source

instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) :

{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqEQ

Equations

⋯ = ⋯

source

instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) :

{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqNEQ

Equations

⋯ = ⋯

source

instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) :

{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqLT

Equations

⋯ = ⋯

source

instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) :

{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqNLT

Equations

⋯ = ⋯

source

@[simp]

theorem LO.Arith.Formalized.eval_qqEQDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :

V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqEQDef) ↔ v 0 = v 1 ^= v 2

source

@[simp]

theorem LO.Arith.Formalized.eval_qqNEQDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :

V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqNEQDef) ↔ v 0 = v 1 ^≠ v 2

source

@[simp]

theorem LO.Arith.Formalized.eval_qqLTDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :

V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqLTDef) ↔ v 0 = v 1 ^< v 2

source

@[simp]

theorem LO.Arith.Formalized.eval_qqNLTDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :

V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqNLTDef) ↔ v 0 = v 1 ^≮ v 2

source

theorem LO.Arith.Formalized.neg_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :

⌜ℒₒᵣ⌝.neg (t ^= u) = t ^≠ u

source

theorem LO.Arith.Formalized.neg_neq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :

⌜ℒₒᵣ⌝.neg (t ^≠ u) = t ^= u

source

theorem LO.Arith.Formalized.neg_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :

⌜ℒₒᵣ⌝.neg (t ^< u) = t ^≮ u

source

theorem LO.Arith.Formalized.neg_nlt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :

⌜ℒₒᵣ⌝.neg (t ^≮ u) = t ^< u

source

theorem LO.Arith.Formalized.substs_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {w : V} {t : V} {u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :

⌜ℒₒᵣ⌝.substs w (t ^= u) = ⌜ℒₒᵣ⌝.termSubst w t ^= ⌜ℒₒᵣ⌝.termSubst w u