---

Step * 1 1 of Lemma member-and-poly-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:
           []
         with starting value:
          sofar)
        over list:
          L2
        with starting value:
         Xs))
  ⇐⇒ (X ∈ Xs) ∨ (∃A∈[]. (∃B∈L2. X = combine-pcs(A;B) ∈ polynomial-constraints())))
BY
{ ((RWO  "l_exists_nil" 0 THENA Auto) THEN Reduce 0 THEN InductionOnList THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

\mforall{}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:
                      []
                  with  starting  value:
                    sofar)
                over  list:
                    L2
                with  starting  value:
                  Xs))
    \mLeftarrow{}{}\mRightarrow{}  (X  \mmember{}  Xs)  \mvee{}  (\mexists{}A\mmember{}[].  (\mexists{}B\mmember{}L2.  X  =  combine-pcs(A;B))))


By

---

Latex:
((RWO    "l\_exists\_nil"  0  THENA  Auto)  THEN  Reduce  0  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index