# mathlibdocumentation

tactic.omega.eq_elim

def omega.symdiv (i j : ) :
Equations
def omega.symmod (i j : ) :
Equations
theorem omega.symmod_add_one_self {i : } :
0 < i (i + 1) = -1
theorem omega.mul_symdiv_eq {i j : } :
j * j = i - j
theorem omega.symmod_eq {i j : } :
j = i - j * j
def omega.sgm (v : ) (b : ) (as : list ) (n : ) :

(sgm v b as n) is the new value assigned to the nth variable after a single step of equality elimination using valuation v, term ⟨b, as⟩, and variable index n. If v satisfies the initial constraint set, then (v ⟨n ↦ sgm v b as n⟩) satisfies the new constraint set after equality elimination.

Equations
def omega.rhs  :
Equations
theorem omega.rhs_correct_aux {v : } {m : } {as : list } {k : } :
∃ (d : ), m * d + (list.map (λ (x : ), m) as) 0 k = 0 k
theorem omega.rhs_correct {v : } {b : } {as : list } (n : ) :
0 < as0 = (b, as)v n = omega.term.val b as n) v) b as)
def omega.sym_sym (m b : ) :
Equations
def omega.coeffs_reduce  :
Equations
• as = let a : := as, m : := a + 1 in b, as) n)
theorem omega.coeffs_reduce_correct {v : } {b : } {as : list } {n : } :
0 < as0 = (b, as)0 = omega.term.val b as n) v) as)
def omega.cancel (m : ) (t1 t2 : omega.term) :
Equations
def omega.subst (n : ) (t1 t2 : omega.term) :
Equations
theorem omega.subst_correct {v : } {b : } {as : list } {t : omega.term} {n : } :
0 < as0 = (b, as) = omega.term.val b as n) v) b as) t)
@[protected, instance]
@[protected, instance]
inductive omega.ee  :
Type

The type of equality elimination rules.

Instances for omega.ee
def omega.ee.repr  :
Equations
@[protected, instance]
Equations
@[protected, instance]

Apply a given sequence of equality elimination steps to a clause.

Equations
theorem omega.sat_eq_elim {es : list omega.ee} {c : omega.clause} :
c.sat c).sat

If the result of equality elimination is unsatisfiable, the original clause is unsatisfiable.