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