---

Step * 1 of Lemma hd-rev-pcs-mon-vars

.....assertion..... 
1. X : polynomial-constraints()
⊢ 0 < ||pcs-mon-vars(X)|| ∧ (last(pcs-mon-vars(X)) = [] ∈ (ℤ List))
BY
{ Assert ⌜∀X:iPolynomial() List. ∀L:ℤ List List.
            (0 < ||L||
            ⇒ (last(L) = [] ∈ (ℤ List))
            ⇒ (0 < ||accumulate (with value vs and list item p):
                       polynomial-mon-vars(vs;p)
                      over list:
                        X
                      with starting value:
                       L)||
               ∧ (last(accumulate (with value vs and list item p):
                        polynomial-mon-vars(vs;p)
                       over list:
                         X
                       with starting value:
                        L))
                 = []
                 ∈ (ℤ List))))⌝⋅ }

1
.....assertion..... 
1. X : polynomial-constraints()
⊢ ∀X:iPolynomial() List. ∀L:ℤ List List.
    (0 < ||L||
    ⇒ (last(L) = [] ∈ (ℤ List))
    ⇒ (0 < ||accumulate (with value vs and list item p):
               polynomial-mon-vars(vs;p)
              over list:
                X
              with starting value:
               L)||
       ∧ (last(accumulate (with value vs and list item p):
                polynomial-mon-vars(vs;p)
               over list:
                 X
               with starting value:
                L))
         = []
         ∈ (ℤ List))))

2
1. X : polynomial-constraints()
2. ∀X:iPolynomial() List. ∀L:ℤ List List.
     (0 < ||L||
     ⇒ (last(L) = [] ∈ (ℤ List))
     ⇒ (0 < ||accumulate (with value vs and list item p):
                polynomial-mon-vars(vs;p)
               over list:
                 X
               with starting value:
                L)||
        ∧ (last(accumulate (with value vs and list item p):
                 polynomial-mon-vars(vs;p)
                over list:
                  X
                with starting value:
                 L))
          = []
          ∈ (ℤ List))))
⊢ 0 < ||pcs-mon-vars(X)|| ∧ (last(pcs-mon-vars(X)) = [] ∈ (ℤ List))

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  polynomial-constraints()
\mvdash{}  0  <  ||pcs-mon-vars(X)||  \mwedge{}  (last(pcs-mon-vars(X))  =  [])


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}X:iPolynomial()  List.  \mforall{}L:\mBbbZ{}  List  List.
                    (0  <  ||L||
                    {}\mRightarrow{}  (last(L)  =  [])
                    {}\mRightarrow{}  (0  <  ||accumulate  (with  value  vs  and  list  item  p):
                                          polynomial-mon-vars(vs;p)
                                        over  list:
                                            X
                                        with  starting  value:
                                          L)||
                          \mwedge{}  (last(accumulate  (with  value  vs  and  list  item  p):
                                            polynomial-mon-vars(vs;p)
                                          over  list:
                                              X
                                          with  starting  value:
                                            L))
                              =  [])))\mkleeneclose{}\mcdot{}

---

Home Index