---

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


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())
BY
{ (FHyp (-3) [-1] 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]))
8. (X ∈ [combine-pcs(u;u1) / v3]) ∨ (∃A∈v. X = combine-pcs(A;u1) ∈ polynomial-constraints())
⊢ (X ∈ v3) ∨ (∃A∈[u / v]. X = combine-pcs(A;u1) ∈ polynomial-constraints())

---

Latex:

---

Latex:

1.  u1  :  polynomial-constraints()
2.  X  :  polynomial-constraints()
3.  u  :  polynomial-constraints()
4.  v  :  polynomial-constraints()  List
5.  \mforall{}v3:polynomial-constraints()  List
          ((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))))
6.  v3  :  polynomial-constraints()  List
7.  (X  \mmember{}  accumulate  (with  value  sofar'  and  list  item  X):
                  [combine-pcs(X;u1)  /  sofar']
                over  list:
                    v
                with  starting  value:
                  [combine-pcs(u;u1)  /  v3]))
\mvdash{}  (X  \mmember{}  v3)  \mvee{}  (\mexists{}A\mmember{}[u  /  v].  X  =  combine-pcs(A;u1))


By

---

Latex:
(FHyp  (-3)  [-1]  THEN  Auto)

---

Home Index