---

Step * 1 2 2 1 1 1 1 of Lemma member-and-poly-constraints


1. v : polynomial-constraints() List
2. u1 : polynomial-constraints()
3. X : polynomial-constraints()
4. v3 : polynomial-constraints() List
⊢ (X ∈ accumulate (with value sofar' and list item X):
        [combine-pcs(X;u1) / sofar']
       over list:
         v
       with starting value:
        v3))
⇒ ((X ∈ v3) ∨ (∃A∈v. X = combine-pcs(A;u1) ∈ polynomial-constraints()))
BY
{ (MoveToConcl (-1) THEN ListInd 1 THEN Reduce 0 THEN Auto) }

1
1. u1 : polynomial-constraints()
2. X : polynomial-constraints()
3. u : polynomial-constraints()
4. v : polynomial-constraints() List
5. ∀v3:polynomial-constraints() List
     ((X ∈ accumulate (with value sofar' and list item X):
            [combine-pcs(X;u1) / sofar']
           over list:
             v
           with starting value:
            v3))
     ⇒ ((X ∈ v3) ∨ (∃A∈v. X = combine-pcs(A;u1) ∈ polynomial-constraints())))
6. v3 : polynomial-constraints() List
7. (X ∈ accumulate (with value sofar' and list item X):
         [combine-pcs(X;u1) / sofar']
        over list:
          v
        with starting value:
         [combine-pcs(u;u1) / v3]))
⊢ (X ∈ v3) ∨ (∃A∈[u / v]. X = combine-pcs(A;u1) ∈ polynomial-constraints())

---

Latex:

---

Latex:

1.  v  :  polynomial-constraints()  List
2.  u1  :  polynomial-constraints()
3.  X  :  polynomial-constraints()
4.  v3  :  polynomial-constraints()  List
\mvdash{}  (X  \mmember{}  accumulate  (with  value  sofar'  and  list  item  X):
                [combine-pcs(X;u1)  /  sofar']
              over  list:
                  v
              with  starting  value:
                v3))
{}\mRightarrow{}  ((X  \mmember{}  v3)  \mvee{}  (\mexists{}A\mmember{}v.  X  =  combine-pcs(A;u1)))


By

---

Latex:
(MoveToConcl  (-1)  THEN  ListInd  1  THEN  Reduce  0  THEN  Auto)

---

Home Index