---

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


1. X : polynomial-constraints()
2. u : iPolynomial()
3. v : iPolynomial() List
4. ∀L:ℤ List List
     (0 < ||L||
     ⇒ (last(L) = [] ∈ (ℤ List))
     ⇒ (0 < ||accumulate (with value vs and list item p):
                polynomial-mon-vars(vs;p)
               over list:
                 v
               with starting value:
                L)||
        ∧ (last(accumulate (with value vs and list item p):
                 polynomial-mon-vars(vs;p)
                over list:
                  v
                with starting value:
                 L))
          = []
          ∈ (ℤ List))))
5. L : ℤ List List
6. 0 < ||L||
7. last(L) = [] ∈ (ℤ List)
⊢ 0 < ||accumulate (with value vs and list item p):
         polynomial-mon-vars(vs;p)
        over list:
          v
        with starting value:
         polynomial-mon-vars(L;u))||
∧ (last(accumulate (with value vs and list item p):
         polynomial-mon-vars(vs;p)
        over list:
          v
        with starting value:
         polynomial-mon-vars(L;u)))
  = []
  ∈ (ℤ List))
BY
{ ((InstHyp [⌜polynomial-mon-vars(L;u)⌝] 4⋅ THENM Trivial) THENW Auto) }

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

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

---

Latex:

---

Latex:

1.  X  :  polynomial-constraints()
2.  u  :  iPolynomial()
3.  v  :  iPolynomial()  List
4.  \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:
                                  v
                              with  starting  value:
                                L)||
                \mwedge{}  (last(accumulate  (with  value  vs  and  list  item  p):
                                  polynomial-mon-vars(vs;p)
                                over  list:
                                    v
                                with  starting  value:
                                  L))
                    =  [])))
5.  L  :  \mBbbZ{}  List  List
6.  0  <  ||L||
7.  last(L)  =  []
\mvdash{}  0  <  ||accumulate  (with  value  vs  and  list  item  p):
                  polynomial-mon-vars(vs;p)
                over  list:
                    v
                with  starting  value:
                  polynomial-mon-vars(L;u))||
\mwedge{}  (last(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:
((InstHyp  [\mkleeneopen{}polynomial-mon-vars(L;u)\mkleeneclose{}]  4\mcdot{}  THENM  Trivial)  THENW  Auto)

---

Home Index