---

Step * 2 of Lemma satisfies-negate-poly-constraints


1. ∀f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
     ((∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X))
     ⇐⇒ (∀X∈L.(∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z))))
⊢ ∀f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
    ((∀X∈L.¬satisfies-poly-constraints(f;X)) ⇐⇒ (∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X)))
BY
{ (RepeatFor 2 (ParallelLast') THEN (RWO  "-1" 0 THENA Auto)) }

1
1. f : ℤ ⟶ ℤ
2. L : polynomial-constraints() List
3. (∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X))
⇐⇒ (∀X∈L.(∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z)))
⊢ (∀X∈L.¬satisfies-poly-constraints(f;X)) ⇐⇒ (∀X∈L.(∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z)))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  2  (ParallelLast')  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index