---

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


1. u : polynomial-constraints()
2. v : polynomial-constraints() List
3. u1 : polynomial-constraints()
4. Xs : polynomial-constraints() List
5. A : polynomial-constraints()
⊢ (A ∈ [u / v])
⇒ (combine-pcs(A;u1) ∈ 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
{ (ListInd 2 THEN Reduce 0) }

1
1. u : polynomial-constraints()
2. u1 : polynomial-constraints()
3. Xs : polynomial-constraints() List
4. A : polynomial-constraints()
⊢ (A ∈ [u]) ⇒ (combine-pcs(A;u1) ∈ [combine-pcs(u;u1) / Xs])

2
1. u : polynomial-constraints()
2. u1 : polynomial-constraints()
3. Xs : polynomial-constraints() List
4. A : polynomial-constraints()
5. u2 : polynomial-constraints()
6. v : polynomial-constraints() List
7. (A ∈ [u / v])
⇒ (combine-pcs(A;u1) ∈ 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 ∈ [u; [u2 / v]])
⇒ (combine-pcs(A;u1) ∈ accumulate (with value sofar' and list item X):
                         [combine-pcs(X;u1) / sofar']
                        over list:
                          v
                        with starting value:
                         [combine-pcs(u2;u1); [combine-pcs(u;u1) / Xs]]))

---

Latex:

---

Latex:

1.  u  :  polynomial-constraints()
2.  v  :  polynomial-constraints()  List
3.  u1  :  polynomial-constraints()
4.  Xs  :  polynomial-constraints()  List
5.  A  :  polynomial-constraints()
\mvdash{}  (A  \mmember{}  [u  /  v])
{}\mRightarrow{}  (combine-pcs(A;u1)  \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:
(ListInd  2  THEN  Reduce  0)

---

Home Index