Eq #

source

def Matrix.iget {α : Type u_1} {k : ℕ} [Inhabited α] (v : Fin k → α) (x : ℕ) :

Imported declaration from the Incompleteness formalization.

Equations

Matrix.iget v x = if h : x < k then v ⟨x, h⟩ else default

Instances For

source

class LO.FirstOrder.Theory.Sub {L : Language} (T U : Theory L) :

Prop

Imported declaration from the Incompleteness formalization.

sub : T ⊆ U

Instances

source

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.refl (L : Language) [Semiformula.Operator.Eq L] :

SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.Theory.Eq.refl L = (“!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 0)”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.symm (L : Language) [Semiformula.Operator.Eq L] :

SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.Theory.Eq.symm L = (“(!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 1) → !!(LO.FirstOrder.Semiterm.fvar 1) = !!(LO.FirstOrder.Semiterm.fvar 0))”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.trans (L : Language) [Semiformula.Operator.Eq L] :

SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.funcExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (f : L.Func k) :

SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Eq.relExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (r : L.Rel k) :

SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

inductive LO.FirstOrder.Theory.eqAxiom {L : Language} [Semiformula.Operator.Eq L] :

Theory L

Imported declaration from the Incompleteness formalization.

refl {L : Language} [Semiformula.Operator.Eq L] : 𝐄𝐐 (Eq.refl L)
symm {L : Language} [Semiformula.Operator.Eq L] : 𝐄𝐐 (Eq.symm L)
trans {L : Language} [Semiformula.Operator.Eq L] : 𝐄𝐐 (Eq.trans L)
funcExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (f : L.Func k) : 𝐄𝐐 (Eq.funcExt f)
relExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (r : L.Rel k) : 𝐄𝐐 (Eq.relExt r)

Instances For

source

def LO.FirstOrder.Theory.«term𝐄𝐐» :

Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.Theory.«term𝐄𝐐» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝐄𝐐» 1024 (Lean.ParserDescr.symbol "𝐄𝐐")

Instances For

source

theorem LO.FirstOrder.Theory.Eq.defeq {L : Language} [Semiformula.Operator.Eq L] :

𝐄𝐐 = ({refl L, symm L, trans L} ∪ Set.range fun (f : (k : ℕ) × L.Func k) => funcExt f.snd) ∪ Set.range fun (f : (k : ℕ) × L.Rel k) => relExt f.snd

source

@[simp]

theorem LO.FirstOrder.Theory.EqAxiom.finite {L : Language} [Semiformula.Operator.Eq L] [L.Finite] :

Set.Finite 𝐄𝐐

source

@[simp]

theorem LO.FirstOrder.Structure.Eq.models_eqAxiom {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [Structure.Eq L M] :

M ⊧ₘ* 𝐄𝐐

source

instance LO.FirstOrder.Structure.Eq.models_eqAxiom' (L : Language) [Semiformula.Operator.Eq L] (M : Type u) [Nonempty M] [Structure L M] [Structure.Eq L M] :

M ⊧ₘ* 𝐄𝐐

source

def LO.FirstOrder.Structure.Eq.eqv (L : Language) [Semiformula.Operator.Eq L] {M : Type u} [Structure L M] (a b : M) :

Prop

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.Structure.Eq.eqv L a b = op(=).val ![a, b]

Instances For

source

theorem LO.FirstOrder.Structure.Eq.eqv_refl {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] (a : M) :

eqv L a a

source

theorem LO.FirstOrder.Structure.Eq.eqv_symm {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {a b : M} :

eqv L a b → eqv L b a

source

theorem LO.FirstOrder.Structure.Eq.eqv_trans {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {a b c : M} :

eqv L a b → eqv L b c → eqv L a c

source

theorem LO.FirstOrder.Structure.Eq.eqv_funcExt {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {k : ℕ} (f : L.Func k) {v w : Fin k → M} (h : ∀ (i : Fin k), eqv L (v i) (w i)) :

eqv L (func f v) (func f w)

source

theorem LO.FirstOrder.Structure.Eq.eqv_relExt_aux {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {k : ℕ} (r : L.Rel k) {v w : Fin k → M} (h : ∀ (i : Fin k), eqv L (v i) (w i)) :

rel r v → rel r w

source

theorem LO.FirstOrder.Structure.Eq.eqv_relExt {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {k : ℕ} (r : L.Rel k) {v w : Fin k → M} (h : ∀ (i : Fin k), eqv L (v i) (w i)) :

rel r v = rel r w

source

theorem LO.FirstOrder.Structure.Eq.eqv_equivalence {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] :

Equivalence (eqv L)

source

def LO.FirstOrder.Structure.Eq.eqvSetoid (L : Language) [Semiformula.Operator.Eq L] (M : Type u) [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] :

Setoid M

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.Structure.Eq.eqvSetoid L M = { r := LO.FirstOrder.Structure.Eq.eqv L, iseqv := ⋯ }

Instances For

source

def LO.FirstOrder.Structure.Eq.QuotEq (L : Language) [Semiformula.Operator.Eq L] (M : Type u) [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] :

Type u

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.Structure.Eq.QuotEq L M = Quotient (LO.FirstOrder.Structure.Eq.eqvSetoid L M)

Instances For

source

instance LO.FirstOrder.Structure.Eq.QuotEq.inhabited {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] :

Nonempty (QuotEq L M)

source

theorem LO.FirstOrder.Structure.Eq.of_eq_of {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {a b : M} :

⟦a⟧ = ⟦b⟧ ↔ eqv L a b

source

def LO.FirstOrder.Structure.Eq.QuotEq.func {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] ⦃k : ℕ⦄ (f : L.Func k) (v : Fin k → QuotEq L M) :

QuotEq L M

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.Structure.Eq.QuotEq.func f v = Quotient.liftVec (fun (x : Fin k → M) => ⟦LO.FirstOrder.Structure.func f x⟧) ⋯ v

Instances For

source

def LO.FirstOrder.Structure.Eq.QuotEq.rel {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] ⦃k : ℕ⦄ (r : L.Rel k) (v : Fin k → QuotEq L M) :

Prop

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.Structure.Eq.QuotEq.rel r v = Quotient.liftVec (LO.FirstOrder.Structure.rel r) ⋯ v

Instances For

source

@[implicit_reducible]

instance LO.FirstOrder.Structure.Eq.QuotEq.struc {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] :

Structure L (QuotEq L M)

Equations

LO.FirstOrder.Structure.Eq.QuotEq.struc = { func := LO.FirstOrder.Structure.Eq.QuotEq.func, rel := LO.FirstOrder.Structure.Eq.QuotEq.rel }

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.funk_mk {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {k : ℕ} (f : L.Func k) (v : Fin k → M) :

(Structure.func f fun (i : Fin k) => ⟦v i⟧) = ⟦Structure.func f v⟧

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.rel_mk {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {k : ℕ} (r : L.Rel k) (v : Fin k → M) :

(Structure.rel r fun (i : Fin k) => ⟦v i⟧) ↔ Structure.rel r v

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.val_mk {L : Language} {μ : Type u_1} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {n : ℕ} {e : Fin n → M} {ε : μ → M} (t : Semiterm L μ n) :

Semiterm.valm (QuotEq L M) (fun (i : Fin n) => ⟦e i⟧) (fun (i : μ) => ⟦ε i⟧) t = ⟦Semiterm.valm M e ε t⟧

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.eval_mk {L : Language} {μ : Type u_1} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {n : ℕ} {e : Fin n → M} {ε : μ → M} {φ : Semiformula L μ n} :

(Semiformula.Evalm (QuotEq L M) (fun (i : Fin n) => ⟦e i⟧) fun (i : μ) => ⟦ε i⟧) φ ↔ (Semiformula.Evalm M e ε) φ

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.eval_mk₀ {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {ξ : Type u_2} {ε : ξ → M} {φ : Formula L ξ} :

(Semiformula.Evalfm (QuotEq L M) fun (i : ξ) => ⟦ε i⟧) φ ↔ (Semiformula.Evalfm M ε) φ

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.models_iff {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] {φ : SyntacticFormula L} :

QuotEq L M ⊧ₘ φ ↔ M ⊧ₘ φ

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.elementaryEquiv (L : Language) [Semiformula.Operator.Eq L] (M : Type u) [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] :

QuotEq L M ≡ₑ[L] M

source

theorem LO.FirstOrder.Structure.Eq.QuotEq.rel_eq {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] (a b : QuotEq L M) :

op(=).val ![a, b] ↔ a = b

source

instance LO.FirstOrder.Structure.Eq.QuotEq.structureEq {L : Language} [Semiformula.Operator.Eq L] {M : Type u} [Nonempty M] [Structure L M] [H : M ⊧ₘ* 𝐄𝐐] :

Structure.Eq L (QuotEq L M)

source

theorem LO.FirstOrder.consequence_iff_eq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] {φ : SyntacticFormula L} :

T ⊨[Struc L] φ ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Structure L M] [Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ φ

source

theorem LO.FirstOrder.consequence_iff_eq' {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] {φ : SyntacticFormula L} :

T ⊨[Struc L] φ ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Structure L M] [Structure.Eq L M] [M ⊧ₘ* T], M ⊧ₘ φ

source

theorem LO.FirstOrder.satisfiable_iff_eq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] :

Semantics.Satisfiable (Struc L) T ↔ ∃ (M : Type v) (x : Nonempty M) (x_1 : Structure L M) (_ : Structure.Eq L M), M ⊧ₘ* T

source

instance LO.FirstOrder.instModelsTheoryModelOfSatEqAxiomOfWeakerThanSyntacticFormulaTheory {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) :

ModelOfSat sat ⊧ₘ* 𝐄𝐐

source

def LO.FirstOrder.ModelOfSatEq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) :

Type v

Imported declaration from the Incompleteness formalization.

Equations

LO.FirstOrder.ModelOfSatEq sat = LO.FirstOrder.Structure.Eq.QuotEq L (LO.FirstOrder.ModelOfSat sat)

Instances For

source

instance LO.FirstOrder.ModelOfSatEq.instNonempty {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) :

Nonempty (ModelOfSatEq sat)

source

@[implicit_reducible]

noncomputable instance LO.FirstOrder.ModelOfSatEq.struc {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) :

Structure L (ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.struc sat = LO.FirstOrder.Structure.Eq.QuotEq.struc

source

instance LO.FirstOrder.ModelOfSatEq.instEq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) :

Structure.Eq L (ModelOfSatEq sat)

source

theorem LO.FirstOrder.ModelOfSatEq.models {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) :

ModelOfSatEq sat ⊧ₘ* T

source

instance LO.FirstOrder.ModelOfSatEq.mod {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) :

ModelOfSatEq sat ⊧ₘ* T

source

@[implicit_reducible]

noncomputable instance LO.FirstOrder.ModelOfSatEq.instZeroOfZero {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Zero L] :

Zero (ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instZeroOfZero sat = { zero := LO.FirstOrder.Semiterm.Operator.val op(0) ![] }

source

instance LO.FirstOrder.ModelOfSatEq.strucZero {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Zero L] :

Structure.Zero L (ModelOfSatEq sat)

source

@[implicit_reducible]

noncomputable instance LO.FirstOrder.ModelOfSatEq.instOneOfOne {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.One L] :

One (ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instOneOfOne sat = { one := LO.FirstOrder.Semiterm.Operator.val op(1) ![] }

source

instance LO.FirstOrder.ModelOfSatEq.instOne {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.One L] :

Structure.One L (ModelOfSatEq sat)

source

@[implicit_reducible]

noncomputable instance LO.FirstOrder.ModelOfSatEq.instAddOfAdd {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Add L] :

Add (ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instAddOfAdd sat = { add := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(+).val ![x, y] }

source

instance LO.FirstOrder.ModelOfSatEq.instAdd {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Add L] :

Structure.Add L (ModelOfSatEq sat)

source

@[implicit_reducible]

noncomputable instance LO.FirstOrder.ModelOfSatEq.instMulOfMul {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Mul L] :

Mul (ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instMulOfMul sat = { mul := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(*).val ![x, y] }

source

instance LO.FirstOrder.ModelOfSatEq.instMul {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiterm.Operator.Mul L] :

Structure.Mul L (ModelOfSatEq sat)

source

@[implicit_reducible]

instance LO.FirstOrder.ModelOfSatEq.instLTOfLT {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiformula.Operator.LT L] :

LT (ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instLTOfLT sat = { lt := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(<).val ![x, y] }

source

instance LO.FirstOrder.ModelOfSatEq.instLT {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiformula.Operator.LT L] :

Structure.LT L (ModelOfSatEq sat)

source

@[implicit_reducible]

instance LO.FirstOrder.ModelOfSatEq.instMembershipOfMem {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiformula.Operator.Mem L] :

Membership (ModelOfSatEq sat) (ModelOfSatEq sat)

Equations

LO.FirstOrder.ModelOfSatEq.instMembershipOfMem sat = { mem := fun (x y : LO.FirstOrder.ModelOfSatEq sat) => op(∈).val ![y, x] }

source

instance LO.FirstOrder.ModelOfSatEq.instMem {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 wkn T] (sat : Semantics.Satisfiable (Struc L) T) [Semiformula.Operator.Mem L] :

Structure.Mem L (ModelOfSatEq sat)

source

def LO.FirstOrder.Semiformula.existsUnique {L : Language} [Operator.Eq L] {n : ℕ} {ξ : Type u_3} (φ : Semiformula L ξ (n + 1)) :

Semiformula L ξ n

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

def LO.FirstOrder.Semiformula.«term∃'!_» :

Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[simp]

theorem LO.FirstOrder.Semiformula.eval_existsUnique {L : Language} [Operator.Eq L] {M : Type u_2} [s : Structure L M] [Structure.Eq L M] {ξ : Type u_3} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {φ : Semiformula L ξ (n + 1)} :

(Eval s e ε) (∃'! φ) ↔ ∃! x : M, (Eval s (x :> e) ε) φ

source

def LO.FirstOrder.BinderNotation.«firstOrderFormula∃!_» :

Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

def LO.FirstOrder.BinderNotation.«firstOrderFormula∃!_,_» :

Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

Documentation

LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Eq

Eq #