---

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


1. X1 : iPolynomial() List
2. X2 : iPolynomial() List
3. ∀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 < ||accumulate (with value vs and list item p):
         polynomial-mon-vars(vs;p)
        over list:
          X2
        with starting value:
         accumulate (with value vs and list item p):
          polynomial-mon-vars(vs;p)
         over list:
           X1
         with starting value:
          [[]]))||
∧ (last(accumulate (with value vs and list item p):
         polynomial-mon-vars(vs;p)
        over list:
          X2
        with starting value:
         accumulate (with value vs and list item p):
          polynomial-mon-vars(vs;p)
         over list:
           X1
         with starting value:
          [[]])))
  = []
  ∈ (ℤ List))
BY
{ (((InstHyp [⌜X2⌝;⌜accumulate (with value vs and list item p):
                     polynomial-mon-vars(vs;p)
                    over list:
                      X1
                    with starting value:
                     [[]])⌝] (-1)⋅
    THENM Trivial
    )
    THENW Auto
    )
   THEN InstHyp [⌜X1⌝;⌜[[]]⌝] (-1)⋅
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  X1  :  iPolynomial()  List
2.  X2  :  iPolynomial()  List
3.  \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))
                    =  [])))
\mvdash{}  0  <  ||accumulate  (with  value  vs  and  list  item  p):
                  polynomial-mon-vars(vs;p)
                over  list:
                    X2
                with  starting  value:
                  accumulate  (with  value  vs  and  list  item  p):
                    polynomial-mon-vars(vs;p)
                  over  list:
                      X1
                  with  starting  value:
                    [[]]))||
\mwedge{}  (last(accumulate  (with  value  vs  and  list  item  p):
                  polynomial-mon-vars(vs;p)
                over  list:
                    X2
                with  starting  value:
                  accumulate  (with  value  vs  and  list  item  p):
                    polynomial-mon-vars(vs;p)
                  over  list:
                      X1
                  with  starting  value:
                    [[]])))
    =  [])


By

---

Latex:
(((InstHyp  [\mkleeneopen{}X2\mkleeneclose{};\mkleeneopen{}accumulate  (with  value  vs  and  list  item  p):
                                      polynomial-mon-vars(vs;p)
                                    over  list:
                                        X1
                                    with  starting  value:
                                      [[]])\mkleeneclose{}]  (-1)\mcdot{}
    THENM  Trivial
    )
    THENW  Auto
    )
  THEN  InstHyp  [\mkleeneopen{}X1\mkleeneclose{};\mkleeneopen{}[[]]\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Reduce  0
  THEN  Auto)

---

Home Index