@[simp]
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
Equations
- omega.lin_comb (n :: ns) (t :: ts) = (omega.term.mul ↑n t).add (omega.lin_comb ns ts)
- omega.lin_comb (_x :: _x_1) list.nil = (0, list.nil ℤ)
- omega.lin_comb list.nil (_x :: _x_1) = (0, list.nil ℤ)
- omega.lin_comb list.nil list.nil = (0, list.nil ℤ)
theorem
omega.lin_comb_holds
{v : ℕ → ℤ}
{ts : list omega.term}
(ns : list ℕ) :
(∀ (t : omega.term), t ∈ ts → 0 ≤ omega.term.val v t) → 0 ≤ omega.term.val v (omega.lin_comb ns ts)
unsat_lin_comb ns ts asserts that the linear combination
lin_comb ns ts is unsatisfiable
Equations
- omega.unsat_lin_comb ns ts = ((omega.lin_comb ns ts).fst < 0 ∧ ∀ (x : ℤ), x ∈ (omega.lin_comb ns ts).snd → x = 0)
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).snd → x = 0) → omega.unsat_lin_comb ns ts
theorem
omega.unsat_of_unsat_lin_comb
(ns : list ℕ)
(ts : list omega.term) :
omega.unsat_lin_comb ns ts → omega.clause.unsat (list.nil omega.term, ts)