---

Step * of Lemma satisfies-combine-pcs

∀f:ℤ ⟶ ℤ. ∀A,B:polynomial-constraints().
  (satisfies-poly-constraints(f;combine-pcs(A;B)) ⇐⇒ satisfies-poly-constraints(f;A) ∧ satisfies-poly-constraints(f;B))
BY
{ ((UnivCD THENA Auto⋅)
   THEN D 2
   THEN D -1
   THEN RepUR ``combine-pcs satisfies-poly-constraints`` 0
   THEN RWO "l_all_append" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}A,B:polynomial-constraints().
    (satisfies-poly-constraints(f;combine-pcs(A;B))
    \mLeftarrow{}{}\mRightarrow{}  satisfies-poly-constraints(f;A)  \mwedge{}  satisfies-poly-constraints(f;B))


By

---

Latex:
((UnivCD  THENA  Auto\mcdot{})
  THEN  D  2
  THEN  D  -1
  THEN  RepUR  ``combine-pcs  satisfies-poly-constraints``  0
  THEN  RWO  "l\_all\_append"  0
  THEN  Auto)

---

Home Index