---

Step * of Lemma satisfies-and-poly-constraints

∀f:ℤ ⟶ ℤ. ∀L2,L1:polynomial-constraints() List.
  ((∃X∈L1. satisfies-poly-constraints(f;X)) ∧ (∃X∈L2. satisfies-poly-constraints(f;X))
  ⇐⇒ (∃X∈and-poly-constraints(L1;L2). satisfies-poly-constraints(f;X)))
BY
{ ((UnivCD THENA Auto) THEN RWW "member-and-poly-constraints l_exists_iff" 0 THEN Auto THEN ExRepD) }

1
1. f : ℤ ⟶ ℤ
2. L2 : polynomial-constraints() List
3. L1 : polynomial-constraints() List
4. X1 : polynomial-constraints()
5. (X1 ∈ L1)
6. satisfies-poly-constraints(f;X1)
7. X : polynomial-constraints()
8. (X ∈ L2)
9. satisfies-poly-constraints(f;X)
⊢ ∃X:polynomial-constraints()
   ((∃A:polynomial-constraints()
      ((A ∈ L1) ∧ (∃B:polynomial-constraints(). ((B ∈ L2) ∧ (X = combine-pcs(A;B) ∈ polynomial-constraints())))))
   ∧ satisfies-poly-constraints(f;X))

2
1. f : ℤ ⟶ ℤ
2. L2 : polynomial-constraints() List
3. L1 : polynomial-constraints() List
4. X : polynomial-constraints()
5. A : polynomial-constraints()
6. (A ∈ L1)
7. B : polynomial-constraints()
8. (B ∈ L2)
9. X = combine-pcs(A;B) ∈ polynomial-constraints()
10. satisfies-poly-constraints(f;X)
⊢ ∃X:polynomial-constraints(). ((X ∈ L1) ∧ satisfies-poly-constraints(f;X))

3
1. f : ℤ ⟶ ℤ
2. L2 : polynomial-constraints() List
3. L1 : polynomial-constraints() List
4. X : polynomial-constraints()
5. A : polynomial-constraints()
6. (A ∈ L1)
7. B : polynomial-constraints()
8. (B ∈ L2)
9. X = combine-pcs(A;B) ∈ polynomial-constraints()
10. satisfies-poly-constraints(f;X)
⊢ ∃X:polynomial-constraints(). ((X ∈ L2) ∧ satisfies-poly-constraints(f;X))

---

Latex:

---

Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L2,L1:polynomial-constraints()  List.
    ((\mexists{}X\mmember{}L1.  satisfies-poly-constraints(f;X))  \mwedge{}  (\mexists{}X\mmember{}L2.  satisfies-poly-constraints(f;X))
    \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}and-poly-constraints(L1;L2).  satisfies-poly-constraints(f;X)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWW  "member-and-poly-constraints  l\_exists\_iff"  0  THEN  Auto  THEN  ExRepD)

---

Home Index