---

Step * 2 1 2 3 of Lemma full-omega_wf

.....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)))
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:
.....wf..... 
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.  b  :  \mBbbB{}
\mvdash{}  istype(b  =  ff  {}\mRightarrow{}  (\mneg{}satisfiable\_int\_formula(fmla)))


By

---

Latex:
TACTIC:Auto

---

Home Index