---

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


1. X : polynomial-constraints()
2. 0 < ||pcs-mon-vars(X)|| ∧ (last(pcs-mon-vars(X)) = [] ∈ (ℤ List))
⊢ 0 < ||rev(pcs-mon-vars(X))|| ∧ (hd(rev(pcs-mon-vars(X))) = [] ∈ (ℤ List))
BY
{ Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index