---

Step * 1 2 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())))
⊢ ∀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())))
BY
{ (InductionOnList THEN (Reduce 0 THENA Auto)) }

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

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())))
4. u1 : polynomial-constraints()
5. v1 : polynomial-constraints() List
6. ∀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:
             v1
           with starting value:
            Xs))
     ⇐⇒ (X ∈ Xs) ∨ (∃A∈[u / v]. (∃B∈v1. X = combine-pcs(A;B) ∈ polynomial-constraints())))
⊢ ∀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:
            [combine-pcs(u;Y) / sofar])
          over list:
            v1
          with starting value:
           accumulate (with value sofar' and list item X):
            [combine-pcs(X;u1) / sofar']
           over list:
             v
           with starting value:
            [combine-pcs(u;u1) / Xs])))
    ⇐⇒ (X ∈ Xs) ∨ (∃A∈[u / v]. (∃B∈[u1 / v1]. X = combine-pcs(A;B) ∈ polynomial-constraints())))

---

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


By

---

Latex:
(InductionOnList  THEN  (Reduce  0  THENA  Auto))

---

Home Index