---

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

∀X:polynomial-constraints(). (0 < ||rev(pcs-mon-vars(X))|| ∧ (hd(rev(pcs-mon-vars(X))) = [] ∈ (ℤ List)))
BY
{ ((UnivCD THENA Auto) THEN Assert ⌜0 < ||pcs-mon-vars(X)|| ∧ (last(pcs-mon-vars(X)) = [] ∈ (ℤ List))⌝⋅) }

1
.....assertion..... 
1. X : polynomial-constraints()
⊢ 0 < ||pcs-mon-vars(X)|| ∧ (last(pcs-mon-vars(X)) = [] ∈ (ℤ List))

2
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))

---

Latex:

---

Latex:
\mforall{}X:polynomial-constraints().  (0  <  ||rev(pcs-mon-vars(X))||  \mwedge{}  (hd(rev(pcs-mon-vars(X)))  =  []))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Assert  \mkleeneopen{}0  <  ||pcs-mon-vars(X)||  \mwedge{}  (last(pcs-mon-vars(X))  =  [])\mkleeneclose{}\mcdot{})

---

Home Index