---

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


1. u : iMonomial() List
⊢ ∀L:ℤ List List. (0 < ||L|| ⇒ (last(polynomial-mon-vars(L;u)) = last(L) ∈ (ℤ List)))
BY
{ (ListInd 1 THEN RepUR ``polynomial-mon-vars`` 0 THEN Try (Fold `polynomial-mon-vars` 0) THEN Auto) }

1
1. u : iMonomial()
2. v : iMonomial() List
3. ∀L:ℤ List List. (0 < ||L|| ⇒ (last(polynomial-mon-vars(L;v)) = last(L) ∈ (ℤ List)))
4. L : ℤ List List
5. 0 < ||L||
⊢ last(polynomial-mon-vars(let c,vs = u in insert(vs;L);v)) = last(L) ∈ (ℤ List)

---

Latex:

---

Latex:

1.  u  :  iMonomial()  List
\mvdash{}  \mforall{}L:\mBbbZ{}  List  List.  (0  <  ||L||  {}\mRightarrow{}  (last(polynomial-mon-vars(L;u))  =  last(L)))


By

---

Latex:
(ListInd  1  THEN  RepUR  ``polynomial-mon-vars``  0  THEN  Try  (Fold  `polynomial-mon-vars`  0)  THEN  Auto)

---

Home Index