---

Step * of Lemma no_repeats-pcs-mon-vars

∀X:polynomial-constraints(). no_repeats(ℤ List;pcs-mon-vars(X))
BY
{ ((Auto THEN D 1 THEN RepUR ``pcs-mon-vars`` 0)
   THEN (Assert ⌜∀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)))⌝⋅
        THENM (BHyp (-1)  THEN Auto)
        )
   ) }

1
.....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)))

---

Latex:

---

Latex:
\mforall{}X:polynomial-constraints().  no\_repeats(\mBbbZ{}  List;pcs-mon-vars(X))


By

---

Latex:
((Auto  THEN  D  1  THEN  RepUR  ``pcs-mon-vars``  0)
  THEN  (Assert  \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{}
            THENM  (BHyp  (-1)    THEN  Auto)
            )
  )

---

Home Index