---

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


1. X : polynomial-constraints()
⊢ ∀L:ℤ List List. (0 < ||L|| ⇒ (last(L) = [] ∈ (ℤ List)) ⇒ (0 < ||L|| ∧ (last(L) = [] ∈ (ℤ List))))
BY
{ Auto }

---

Latex:

---

Latex:

1.  X  :  polynomial-constraints()
\mvdash{}  \mforall{}L:\mBbbZ{}  List  List.  (0  <  ||L||  {}\mRightarrow{}  (last(L)  =  [])  {}\mRightarrow{}  (0  <  ||L||  \mwedge{}  (last(L)  =  [])))


By

---

Latex:
Auto

---

Home Index