---

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

.....assertion..... 
∀L1,L2,Xs:polynomial-constraints() List. ∀X:polynomial-constraints().
  ((X ∈ accumulate (with value sofar and list item Y):
         accumulate (with value sofar' and list item X):
          [combine-pcs(X;Y) / sofar']
         over list:
           L1
         with starting value:
          sofar)
        over list:
          L2
        with starting value:
         Xs))
  ⇐⇒ (X ∈ Xs) ∨ (∃A∈L1. (∃B∈L2. X = combine-pcs(A;B) ∈ polynomial-constraints())))
BY
{ InductionOnList }

1
∀L2,Xs:polynomial-constraints() List. ∀X:polynomial-constraints().
  ((X ∈ accumulate (with value sofar and list item Y):
         accumulate (with value sofar' and list item X):
          [combine-pcs(X;Y) / sofar']
         over list:
           []
         with starting value:
          sofar)
        over list:
          L2
        with starting value:
         Xs))
  ⇐⇒ (X ∈ Xs) ∨ (∃A∈[]. (∃B∈L2. X = combine-pcs(A;B) ∈ polynomial-constraints())))

2
1. u : polynomial-constraints()
2. v : polynomial-constraints() List
3. ∀L2,Xs:polynomial-constraints() List. ∀X:polynomial-constraints().
     ((X ∈ accumulate (with value sofar and list item Y):
            accumulate (with value sofar' and list item X):
             [combine-pcs(X;Y) / sofar']
            over list:
              v
            with starting value:
             sofar)
           over list:
             L2
           with starting value:
            Xs))
     ⇐⇒ (X ∈ Xs) ∨ (∃A∈v. (∃B∈L2. X = combine-pcs(A;B) ∈ polynomial-constraints())))
⊢ ∀L2,Xs:polynomial-constraints() List. ∀X:polynomial-constraints().
    ((X ∈ accumulate (with value sofar and list item Y):
           accumulate (with value sofar' and list item X):
            [combine-pcs(X;Y) / sofar']
           over list:
             [u / v]
           with starting value:
            sofar)
          over list:
            L2
          with starting value:
           Xs))
    ⇐⇒ (X ∈ Xs) ∨ (∃A∈[u / v]. (∃B∈L2. X = combine-pcs(A;B) ∈ polynomial-constraints())))

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}L1,L2,Xs:polynomial-constraints()  List.  \mforall{}X:polynomial-constraints().
    ((X  \mmember{}  accumulate  (with  value  sofar  and  list  item  Y):
                  accumulate  (with  value  sofar'  and  list  item  X):
                    [combine-pcs(X;Y)  /  sofar']
                  over  list:
                      L1
                  with  starting  value:
                    sofar)
                over  list:
                    L2
                with  starting  value:
                  Xs))
    \mLeftarrow{}{}\mRightarrow{}  (X  \mmember{}  Xs)  \mvee{}  (\mexists{}A\mmember{}L1.  (\mexists{}B\mmember{}L2.  X  =  combine-pcs(A;B))))


By

---

Latex:
InductionOnList

---

Home Index