---

Step * 2 of Lemma full-omega_wf


1. fmla : int_formula()
2. v : polynomial-constraints() List
3. int_formula_dnf(fmla) = v ∈ (polynomial-constraints() List)
⊢ (satisfiable_int_formula(fmla) ⇐⇒ (∃X∈v. satisfiable_polynomial_constraints(X)))
⇒ (eval dnf = v in
    eager-accum(sat,pc.sat
    ∨blet eqs,ineqs = pcs-to-integer-problem(pc) 
      in case omega(eqs;ineqs) of inl(x) => tt | inr(_) => ff;ff;dnf) ∈ {b:𝔹| 
                                                                         b = ff ⇒ (¬satisfiable_int_formula(fmla))} )
BY
{ TACTIC:((CallByValueReduce 0 THENA Auto) THEN (D 0 THENA Auto)) }

1
1. fmla : int_formula()
2. v : polynomial-constraints() List
3. int_formula_dnf(fmla) = v ∈ (polynomial-constraints() List)
4. satisfiable_int_formula(fmla) ⇐⇒ (∃X∈v. satisfiable_polynomial_constraints(X))
⊢ eager-accum(sat,pc.sat
  ∨blet eqs,ineqs = pcs-to-integer-problem(pc) 
    in case omega(eqs;ineqs) of inl(x) => tt | inr(_) => ff;ff;v) ∈ {b:𝔹| b = ff ⇒ (¬satisfiable_int_formula(fmla))} 

---

Latex:

---

Latex:

1.  fmla  :  int\_formula()
2.  v  :  polynomial-constraints()  List
3.  int\_formula\_dnf(fmla)  =  v
\mvdash{}  (satisfiable\_int\_formula(fmla)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}v.  satisfiable\_polynomial\_constraints(X)))
{}\mRightarrow{}  (eval  dnf  =  v  in
        eager-accum(sat,pc.sat
        \mvee{}\msubb{}let  eqs,ineqs  =  pcs-to-integer-problem(pc) 
            in  case  omega(eqs;ineqs)  of  inl(x)  =>  tt  |  inr($_{}$)  =>  ff;ff;dnf)
        \mmember{}  \{b:\mBbbB{}|  b  =  ff  {}\mRightarrow{}  (\mneg{}satisfiable\_int\_formula(fmla))\}  )


By

---

Latex:
TACTIC:((CallByValueReduce  0  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index