---

Step * 2 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))
⊢ valueall-type(𝔹)
BY
{ Auto }

---

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{}  valueall-type(\mBbbB{})


By

---

Latex:
Auto

---

Home Index