---

Step * 1 of Lemma satisfiable_int_formula_dnf


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

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -1
  THEN  (RWO  "satisfies\_int\_formula\_dnf"  (-1)  THEN  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index