mathlib documentation

tactic.omega.eq_elim

def omega.symdiv  :

Equations
def omega.symmod  :

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  :
()list

(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 v n omega.sgm v b as n (omega.rhs n b as)

def omega.sym_sym  :

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 v n omega.sgm v b as n (omega.coeffs_reduce n b as)

Equations

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 v n omega.sgm v b as n (omega.subst n (omega.rhs n b as) t)

@[instance]

inductive omega.ee  :
Type

The type of equality elimination rules.

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.