---

Step * 1 2 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())))
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())))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Reduce (-3)
   THEN (RWO "-3" 0 THENA Auto)
   THEN (GenConclTerm ⌜[u / v]⌝⋅ THENA Auto)
   THEN RWO "l_exists_cons" 0
   THEN Auto
   THEN SplitOrHyps) }

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)
∨ (∃A∈v2. (X = combine-pcs(A;u1) ∈ polynomial-constraints()) ∨ (∃B∈v1. 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:
              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∈v2. (∃B∈v1. X = combine-pcs(A;B) ∈ polynomial-constraints()))
⊢ (X ∈ Xs)
∨ (∃A∈v2. (X = combine-pcs(A;u1) ∈ polynomial-constraints()) ∨ (∃B∈v1. X = combine-pcs(A;B) ∈ polynomial-constraints()))

3
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 ∈ Xs)
⊢ (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]))
∨ (∃A∈v2. (∃B∈v1. X = combine-pcs(A;B) ∈ polynomial-constraints()))

4
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∈v2. (X = combine-pcs(A;u1) ∈ polynomial-constraints())
∨ (∃B∈v1. X = combine-pcs(A;B) ∈ 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]))
∨ (∃A∈v2. (∃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:
                            [u  /  v]
                        with  starting  value:
                          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))))
\mvdash{}  \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:
                      accumulate  (with  value  sofar'  and  list  item  X):
                        [combine-pcs(X;u1)  /  sofar']
                      over  list:
                          v
                      with  starting  value:
                        [combine-pcs(u;u1)  /  Xs])))
        \mLeftarrow{}{}\mRightarrow{}  (X  \mmember{}  Xs)  \mvee{}  (\mexists{}A\mmember{}[u  /  v].  (\mexists{}B\mmember{}[u1  /  v1].  X  =  combine-pcs(A;B))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Reduce  (-3)
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}[u  /  v]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RWO  "l\_exists\_cons"  0
  THEN  Auto
  THEN  SplitOrHyps)

---

Home Index