---

Step * 2 1 2 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))
⊢ 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))} 
BY
{ TACTIC:MemTypeCD }

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))
⊢ 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) ∈ 𝔹

2
.....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))

3
.....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))
5. b : 𝔹
⊢ istype(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{}  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)  \mmember{}  \{b:\mBbbB{}|  b  =  ff  {}\mRightarrow{}  (\mneg{}satisfiable\_int\_formula(fmla))\} 


By

---

Latex:
TACTIC:MemTypeCD

---

Home Index