---

Step * 2 of Lemma satisfiable_int_formula_dnf


1. fmla : int_formula()@i
2. (∃X∈int_formula_dnf(fmla). satisfiable_polynomial_constraints(X))@i
⊢ satisfiable_int_formula(fmla)
BY
{ ((RWO  "l_exists_iff" (-1) THENA Auto)
   THEN ExRepD
   THEN D -1
   THEN With ⌜f⌝ (D 0)⋅
   THEN Auto
   THEN RWO "satisfies_int_formula_dnf" 0
   THEN Auto
   THEN RWO  "l_exists_iff" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  fmla  :  int\_formula()@i
2.  (\mexists{}X\mmember{}int\_formula\_dnf(fmla).  satisfiable\_polynomial\_constraints(X))@i
\mvdash{}  satisfiable\_int\_formula(fmla)


By

---

Latex:
((RWO    "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  D  -1
  THEN  With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RWO  "satisfies\_int\_formula\_dnf"  0
  THEN  Auto
  THEN  RWO    "l\_exists\_iff"  0
  THEN  Auto)

---

Home Index