(([t₁,...tₘ],[s₁,...,sₙ]) : clause) encodes the constraints 0 = ⟦t₁⟧ ∧ ... ∧ 0 = ⟦tₘ⟧ ∧ 0 ≤ ⟦s₁⟧ ∧ ... ∧ 0 ≤ ⟦sₙ⟧, where ⟦t⟧ is the value of (t : term).
Equations
holds v c := clause c holds under valuation v
Equations
- omega.clause.holds v (eqs, les) = ((∀ (t : omega.term), t ∈ eqs → 0 = omega.term.val v t) ∧ ∀ (t : omega.term), t ∈ les → 0 ≤ omega.term.val v t)
sat c := there exists a valuation v under which c holds
Equations
- c.sat = ∃ (v : ℕ → ℤ), omega.clause.holds v c
unsat c := there is no valuation v under which c holds
append two clauses by elementwise appending
theorem
omega.clause.holds_append
{v : ℕ → ℤ}
{c1 c2 : omega.clause} :
omega.clause.holds v c1 → omega.clause.holds v c2 → omega.clause.holds v (c1.append c2)
There exists a satisfiable clause c in argument
Equations
- omega.clauses.sat cs = ∃ (c : omega.clause) (H : c ∈ cs), c.sat
There is no satisfiable clause c in argument
Equations
theorem
omega.clauses.unsat_cons
(c : omega.clause)
(cs : list omega.clause) :
c.unsat → omega.clauses.unsat cs → omega.clauses.unsat (c :: cs)