---

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


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)))
BY
{ (BHyp -3  THEN EAuto 1) }

---

Latex:

---

Latex:

1.  X1  :  iPolynomial()  List@i
2.  X2  :  iPolynomial()  List@i
3.  u  :  iPolynomial()@i
4.  v  :  iPolynomial()  List@i
5.  \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:
                                                        v
                                                    with  starting  value:
                                                      L)))@i
6.  L  :  \mBbbZ{}  List  List@i
7.  no\_repeats(\mBbbZ{}  List;L)@i
\mvdash{}  no\_repeats(\mBbbZ{}  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)))


By

---

Latex:
(BHyp  -3    THEN  EAuto  1)

---

Home Index