---

Step * 1 2 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())))
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. (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]))
⊢ (X ∈ Xs)
∨ (∃A∈v2. (X = combine-pcs(A;u1) ∈ polynomial-constraints()) ∨ (∃B∈v1. X = combine-pcs(A;B) ∈ polynomial-constraints()))
BY
{ (RevHypSubst' (-2) 0 THEN (RWO "l_exists_cons" 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())))
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. (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]))
⊢ (X ∈ Xs)
∨ ((X = combine-pcs(u;u1) ∈ polynomial-constraints()) ∨ (∃B∈v1. X = combine-pcs(u;B) ∈ polynomial-constraints()))
∨ (∃A∈v. (X = combine-pcs(A;u1) ∈ polynomial-constraints()) ∨ (∃B∈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))))
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.  (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]))
\mvdash{}  (X  \mmember{}  Xs)  \mvee{}  (\mexists{}A\mmember{}v2.  (X  =  combine-pcs(A;u1))  \mvee{}  (\mexists{}B\mmember{}v1.  X  =  combine-pcs(A;B)))


By

---

Latex:
(RevHypSubst'  (-2)  0  THEN  (RWO  "l\_exists\_cons"  0  THENA  Auto))

---

Home Index