---

Step * of Lemma satisfies-negate-poly-constraint

∀X:polynomial-constraints(). ∀f:ℤ ⟶ ℤ.
  ((∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z)) ⇐⇒ ¬satisfies-poly-constraints(f;X))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN D 1 THEN RenameVar `eqs' 1 THEN RenameVar `ineqs' 2) }

1
1. eqs : iPolynomial() List
2. ineqs : iPolynomial() List
3. f : ℤ ⟶ ℤ
⊢ (∃Z∈negate-poly-constraint(<eqs, ineqs>). satisfies-poly-constraints(f;Z)) ⇐⇒ ¬satisfies-poly-constraints(f;<eqs, ine\000Cqs>)

---

Latex:

---

Latex:
\mforall{}X:polynomial-constraints().  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.
    ((\mexists{}Z\mmember{}negate-poly-constraint(X).  satisfies-poly-constraints(f;Z))
    \mLeftarrow{}{}\mRightarrow{}  \mneg{}satisfies-poly-constraints(f;X))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  D  1  THEN  RenameVar  `eqs'  1  THEN  RenameVar  `ineqs'  2)

---

Home Index