---

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


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())))
⊢ ∀Xs:polynomial-constraints() List. ∀X:polynomial-constraints().
    ((X ∈ Xs) ⇐⇒ (X ∈ Xs) ∨ (∃A∈[u / v]. (∃B∈[]. X = combine-pcs(A;B) ∈ polynomial-constraints())))
BY
{ (RWO  "l_exists_nil" 0 THEN Auto THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  polynomial-constraints()
2.  v  :  polynomial-constraints()  List
3.  \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:
                            v
                        with  starting  value:
                          sofar)
                      over  list:
                          L2
                      with  starting  value:
                        Xs))
          \mLeftarrow{}{}\mRightarrow{}  (X  \mmember{}  Xs)  \mvee{}  (\mexists{}A\mmember{}v.  (\mexists{}B\mmember{}L2.  X  =  combine-pcs(A;B))))
\mvdash{}  \mforall{}Xs:polynomial-constraints()  List.  \mforall{}X:polynomial-constraints().
        ((X  \mmember{}  Xs)  \mLeftarrow{}{}\mRightarrow{}  (X  \mmember{}  Xs)  \mvee{}  (\mexists{}A\mmember{}[u  /  v].  (\mexists{}B\mmember{}[].  X  =  combine-pcs(A;B))))


By

---

Latex:
(RWO    "l\_exists\_nil"  0  THEN  Auto  THEN  D  -1  THEN  Auto)

---

Home Index