---

Step * 2 1 2 2 1 1 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))
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
6. i : ℕ||v||
7. satisfiable_polynomial_constraints(v[i])
⊢ False
BY
{ TACTIC:Assert ⌜(∀pc∈v.let eqs,ineqs = pcs-to-integer-problem(pc) 
                        in case omega(eqs;ineqs) of inl(x) => tt | inr(_) => ff 
                     = ff)⌝⋅ }

1
.....assertion..... 
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
6. i : ℕ||v||
7. satisfiable_polynomial_constraints(v[i])
⊢ (∀pc∈v.let eqs,ineqs = pcs-to-integer-problem(pc) in case omega(eqs;ineqs) of inl(x) => tt | inr(_) => ff = ff)

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))
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
6. i : ℕ||v||
7. satisfiable_polynomial_constraints(v[i])
8. (∀pc∈v.let eqs,ineqs = pcs-to-integer-problem(pc) in case omega(eqs;ineqs) of inl(x) => tt | inr(_) => ff = ff)
⊢ False

---

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))
5.  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
6.  i  :  \mBbbN{}||v||
7.  satisfiable\_polynomial\_constraints(v[i])
\mvdash{}  False


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}(\mforall{}pc\mmember{}v.let  eqs,ineqs  =  pcs-to-integer-problem(pc) 
                                            in  case  omega(eqs;ineqs)  of  inl(x)  =>  tt  |  inr($_{}$)  =>  f\000Cf 
                                      =  ff)\mkleeneclose{}\mcdot{}

---

Home Index