---

Step * of Lemma member-and-poly-constraints

∀L1,L2:polynomial-constraints() List. ∀X:polynomial-constraints().
  ((X ∈ and-poly-constraints(L1;L2)) ⇐⇒ (∃A∈L1. (∃B∈L2. X = combine-pcs(A;B) ∈ polynomial-constraints())))
BY
{ (Assert ⌜∀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())))⌝⋅
THENM (Unfold `and-poly-constraints` 0 THEN RepeatFor 2 (ParallelLast) THEN RWO  "-1" 0 THEN Auto)
) }

1
.....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())))

---

Latex:

---

Latex:
\mforall{}L1,L2:polynomial-constraints()  List.  \mforall{}X:polynomial-constraints().
    ((X  \mmember{}  and-poly-constraints(L1;L2))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}A\mmember{}L1.  (\mexists{}B\mmember{}L2.  X  =  combine-pcs(A;B))))


By

---

Latex:
(Assert  \mkleeneopen{}\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))))\mkleeneclose{}\mcdot{}
THENM  (Unfold  `and-poly-constraints`  0  THEN  RepeatFor  2  (ParallelLast)  THEN  RWO    "-1"  0  THEN  Auto)
)

---

Home Index