---

Step * 2 1 2 2 of Lemma full-omega_wf

.....set predicate..... 
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))
⊢ accumulate (with value sat and list item pc):
   sat ∨blet eqs,ineqs = pcs-to-integer-problem(pc) in case omega(eqs;ineqs) of inl(x) => tt | inr(_) => ff
  over list:
    v
  with starting value:
   ff) 
= ff
⇒ (¬satisfiable_int_formula(fmla))
BY
{ TACTIC:(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))
5. accumulate (with value sat and list item pc):
    sat ∨blet eqs,ineqs = pcs-to-integer-problem(pc) in case omega(eqs;ineqs) of inl(x) => tt | inr(_) => ff
   over list:
     v
   with starting value:
    ff) 
= ff
⊢ ¬satisfiable_int_formula(fmla)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  fmla  :  int\_formula()
2.  v  :  polynomial-constraints()  List
3.  int\_formula\_dnf(fmla)  =  v
4.  satisfiable\_int\_formula(fmla)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}v.  satisfiable\_polynomial\_constraints(X))
\mvdash{}  accumulate  (with  value  sat  and  list  item  pc):
      sat
      \mvee{}\msubb{}let  eqs,ineqs  =  pcs-to-integer-problem(pc) 
          in  case  omega(eqs;ineqs)  of  inl(x)  =>  tt  |  inr($_{}$)  =>  ff
    over  list:
        v
    with  starting  value:
      ff) 
=  ff
{}\mRightarrow{}  (\mneg{}satisfiable\_int\_formula(fmla))


By

---

Latex:
TACTIC:(D  0  THENA  Auto)

---

Home Index