---

Step * 2 1 of Lemma full-omega_wf


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))} 
BY
{ TACTIC:(RWO "eager-accum-list_accum" 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))
⊢ valueall-type(𝔹)

2
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) ∈ {b:𝔹| b = ff ⇒ (¬satisfiable_int_formula(fmla))} 

---

Latex:

---

Latex:

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{}  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;v)
    \mmember{}  \{b:\mBbbB{}|  b  =  ff  {}\mRightarrow{}  (\mneg{}satisfiable\_int\_formula(fmla))\} 


By

---

Latex:
TACTIC:(RWO  "eager-accum-list\_accum"  0  THENA  Auto)

---

Home Index