mathlib documentation

tactic.omega.eq_elim

def omega.symdiv (i j : ) :
Equations
def omega.symmod (i j : ) :
Equations
theorem omega.symmod_add_one_self {i : } :
0 < iomega.symmod i (i + 1) = -1
theorem omega.mul_symdiv_eq {i j : } :
theorem omega.symmod_eq {i 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  :
list omega.term
Equations
theorem omega.rhs_correct_aux {v : } {m : } {as : list } {k : } :
∃ (d : ), m * d + omega.coeffs.val_between v (list.map (λ (x : ), omega.symmod x m) as) 0 k = omega.coeffs.val_between v as 0 k
theorem omega.rhs_correct {v : } {b : } {as : list } (n : ) :
0 < list.func.get n as0 = omega.term.val v (b, as)v n = omega.term.val (omega.update n (omega.sgm v b as n) v) (omega.rhs n b as)
def omega.sym_sym (m b : ) :
Equations
Equations
theorem omega.coeffs_reduce_correct {v : } {b : } {as : list } {n : } :
0 < list.func.get n as0 = omega.term.val v (b, as)0 = omega.term.val (omega.update n (omega.sgm v b as n) v) (omega.coeffs_reduce n b 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 < list.func.get n as0 = omega.term.val v (b, as)omega.term.val v t = omega.term.val (omega.update n (omega.sgm v b as n) v) (omega.subst n (omega.rhs n b as) t)
@[protected, instance]
@[protected, instance]
inductive omega.ee  :
Type

The type of equality elimination rules.

Instances for omega.ee
@[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(omega.eq_elim es c).sat

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