mathlib documentation


Linear combination of constraints. The second argument is the list of constraints, and the first argument is the list of conefficients by which the constraints are multiplied

theorem omega.lin_comb_holds {v : } {ts : list omega.term} (ns : list ) :
(∀ (t : omega.term), t ts0 omega.term.val v t)0 omega.term.val v (omega.lin_comb ns ts)
def omega.unsat_lin_comb (ns : list ) (ts : list omega.term) :

unsat_lin_comb ns ts asserts that the linear combination lin_comb ns ts is unsatisfiable

theorem omega.unsat_lin_comb_of (ns : list ) (ts : list omega.term) :
(omega.lin_comb ns ts).fst < 0(∀ (x : ), x (omega.lin_comb ns ts).sndx = 0)omega.unsat_lin_comb ns ts