---

Step * 1 2 2 4 1 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())))
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:
              v
            with starting value:
             [combine-pcs(u;Y) / sofar])
           over list:
             v1
           with starting value:
            Xs))
     ⇐⇒ (X ∈ Xs) ∨ (∃A∈[u / v]. (∃B∈v1. X = combine-pcs(A;B) ∈ polynomial-constraints())))
7. Xs : polynomial-constraints() List
8. X : polynomial-constraints()
9. v2 : polynomial-constraints() List
10. [u / v] = v2 ∈ (polynomial-constraints() List)
11. A : polynomial-constraints()
12. (A ∈ v2)
13. X = combine-pcs(A;u1) ∈ polynomial-constraints()
⊢ (X ∈ accumulate (with value sofar' and list item X):
        [combine-pcs(X;u1) / sofar']
       over list:
         v
       with starting value:
        [combine-pcs(u;u1) / Xs]))
BY
{ RevHypSubst'(-4) (-2) }

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

---

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))))
4.  u1  :  polynomial-constraints()
5.  v1  :  polynomial-constraints()  List
6.  \mforall{}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:
                          [combine-pcs(u;Y)  /  sofar])
                      over  list:
                          v1
                      with  starting  value:
                        Xs))
          \mLeftarrow{}{}\mRightarrow{}  (X  \mmember{}  Xs)  \mvee{}  (\mexists{}A\mmember{}[u  /  v].  (\mexists{}B\mmember{}v1.  X  =  combine-pcs(A;B))))
7.  Xs  :  polynomial-constraints()  List
8.  X  :  polynomial-constraints()
9.  v2  :  polynomial-constraints()  List
10.  [u  /  v]  =  v2
11.  A  :  polynomial-constraints()
12.  (A  \mmember{}  v2)
13.  X  =  combine-pcs(A;u1)
\mvdash{}  (X  \mmember{}  accumulate  (with  value  sofar'  and  list  item  X):
                [combine-pcs(X;u1)  /  sofar']
              over  list:
                  v
              with  starting  value:
                [combine-pcs(u;u1)  /  Xs]))


By

---

Latex:
RevHypSubst'(-4)  (-2)

---

Home Index