---

Step * 1 of Lemma no_repeats-pcs-mon-vars

.....assertion..... 
1. X1 : iPolynomial() List@i
2. X2 : iPolynomial() List@i
⊢ ∀X:iPolynomial() List. ∀L:ℤ List List.
    (no_repeats(ℤ List;L)
    ⇒ no_repeats(ℤ List;accumulate (with value vs and list item p):
                          polynomial-mon-vars(vs;p)
                         over list:
                           X
                         with starting value:
                          L)))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. X1 : iPolynomial() List@i
2. X2 : iPolynomial() List@i
3. u : iPolynomial()@i
4. v : iPolynomial() List@i
5. ∀L:ℤ List List
     (no_repeats(ℤ List;L)
     ⇒ no_repeats(ℤ List;accumulate (with value vs and list item p):
                           polynomial-mon-vars(vs;p)
                          over list:
                            v
                          with starting value:
                           L)))@i
6. L : ℤ List List@i
7. no_repeats(ℤ List;L)@i
⊢ no_repeats(ℤ List;accumulate (with value vs and list item p):
                     polynomial-mon-vars(vs;p)
                    over list:
                      v
                    with starting value:
                     polynomial-mon-vars(L;u)))

---

Latex:

---

Latex:
.....assertion..... 
1.  X1  :  iPolynomial()  List@i
2.  X2  :  iPolynomial()  List@i
\mvdash{}  \mforall{}X:iPolynomial()  List.  \mforall{}L:\mBbbZ{}  List  List.
        (no\_repeats(\mBbbZ{}  List;L)
        {}\mRightarrow{}  no\_repeats(\mBbbZ{}  List;accumulate  (with  value  vs  and  list  item  p):
                                                    polynomial-mon-vars(vs;p)
                                                  over  list:
                                                      X
                                                  with  starting  value:
                                                    L)))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index