@[simp]
push_neg p returns the result of normalizing ¬ p by pushing the outermost negation all the way down, until it reaches either a negation or an atom
Equations
- omega.int.push_neg (p ∧* q) = (omega.int.push_neg p ∨* omega.int.push_neg q)
- omega.int.push_neg (p ∨* q) = (omega.int.push_neg p ∧* omega.int.push_neg q)
- omega.int.push_neg (¬* p) = p
- omega.int.push_neg (a ≤* a_1) = ¬* (a ≤* a_1)
- omega.int.push_neg (a =* a_1) = ¬* (a =* a_1)
NNF transformation
Equations
- omega.int.nnf (p ∧* q) = (omega.int.nnf p ∧* omega.int.nnf q)
- omega.int.nnf (p ∨* q) = (omega.int.nnf p ∨* omega.int.nnf q)
- omega.int.nnf (¬* p) = omega.int.push_neg (omega.int.nnf p)
- omega.int.nnf (a ≤* a_1) = (a ≤* a_1)
- omega.int.nnf (a =* a_1) = (a =* a_1)
Equations
- omega.int.is_nnf (p ∧* q) = (omega.int.is_nnf p ∧ omega.int.is_nnf q)
- omega.int.is_nnf (p ∨* q) = (omega.int.is_nnf p ∧ omega.int.is_nnf q)
- omega.int.is_nnf (¬* (a ∧* a_1)) = false
- omega.int.is_nnf (¬* (a ∨* a_1)) = false
- omega.int.is_nnf (¬* ¬* a) = false
- omega.int.is_nnf (¬* (t ≤* s)) = true
- omega.int.is_nnf (¬* (t =* s)) = true
- omega.int.is_nnf (t ≤* s) = true
- omega.int.is_nnf (t =* s) = true
Argument is free of negations
Equations
- omega.int.neg_free (p ∧* q) = (omega.int.neg_free p ∧ omega.int.neg_free q)
- omega.int.neg_free (p ∨* q) = (omega.int.neg_free p ∧ omega.int.neg_free q)
- omega.int.neg_free (¬* a) = false
- omega.int.neg_free (t ≤* s) = true
- omega.int.neg_free (t =* s) = true
@[simp]
Eliminate all negations from preform
Equations
- omega.int.neg_elim (p ∧* q) = (omega.int.neg_elim p ∧* omega.int.neg_elim q)
- omega.int.neg_elim (p ∨* q) = (omega.int.neg_elim p ∨* omega.int.neg_elim q)
- omega.int.neg_elim (¬* (a ∧* a_1)) = ¬* (a ∧* a_1)
- omega.int.neg_elim (¬* (a ∨* a_1)) = ¬* (a ∨* a_1)
- omega.int.neg_elim (¬* ¬* a) = ¬* ¬* a
- omega.int.neg_elim (¬* (t ≤* s)) = (s.add_one ≤* t)
- omega.int.neg_elim (¬* (t =* s)) = (t.add_one ≤* s ∨* (s.add_one ≤* t))
- omega.int.neg_elim (a ≤* a_1) = (a ≤* a_1)
- omega.int.neg_elim (a =* a_1) = (a =* a_1)
@[simp]
Equations
- omega.int.dnf_core (p ∧* q) = list.map (λ (pq : omega.clause × omega.clause), pq.fst.append pq.snd) ((omega.int.dnf_core p).product (omega.int.dnf_core q))
- omega.int.dnf_core (p ∨* q) = omega.int.dnf_core p ++ omega.int.dnf_core q
- omega.int.dnf_core (¬* _x) = list.nil
- omega.int.dnf_core (t ≤* s) = [(list.nil omega.term, [(omega.int.canonize s).sub (omega.int.canonize t)])]
- omega.int.dnf_core (t =* s) = [([(omega.int.canonize s).sub (omega.int.canonize t)], list.nil omega.term)]
DNF transformation
Equations
theorem
omega.int.exists_clause_holds
{v : ℕ → ℤ}
{p : omega.int.preform}
(a : omega.int.neg_free p)
(a_1 : omega.int.preform.holds v p) :
∃ (c : omega.clause) (H : c ∈ omega.int.dnf_core p), omega.clause.holds v c
theorem
omega.int.clauses_sat_dnf_core
{p : omega.int.preform}
(a : omega.int.neg_free p)
(a_1 : p.sat) :
theorem
omega.int.unsat_of_clauses_unsat
{p : omega.int.preform}
(a : omega.clauses.unsat (omega.int.dnf p)) :
p.unsat