---

Step * of Lemma satisfiable_int_formula_dnf

∀fmla:int_formula()
  (satisfiable_int_formula(fmla) ⇐⇒ (∃X∈int_formula_dnf(fmla). satisfiable_polynomial_constraints(X)))
BY
{ Auto }

1
1. fmla : int_formula()@i
2. satisfiable_int_formula(fmla)@i
⊢ (∃X∈int_formula_dnf(fmla). satisfiable_polynomial_constraints(X))

2
1. fmla : int_formula()@i
2. (∃X∈int_formula_dnf(fmla). satisfiable_polynomial_constraints(X))@i
⊢ satisfiable_int_formula(fmla)

---

Latex:

---

Latex:
\mforall{}fmla:int\_formula()
    (satisfiable\_int\_formula(fmla)
    \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}int\_formula\_dnf(fmla).  satisfiable\_polynomial\_constraints(X)))


By

---

Latex:
Auto

---

Home Index