---

Step * of Lemma assert-nonneg-monomial

∀m:iMonomial(). ((↑nonneg-monomial(m)) ⇒ (∃m':iMonomial(). ∃k:ℕ+. (mul-monomials(m';m') = mul-monomials(m;<k, []>) ∈ iM\000Conomial())))
BY
{ (Auto THEN D 1 THEN RepUR ``nonneg-monomial`` -1 THEN (RW assert_pushdownC (-1) THENA Auto) THEN D -1) }

1
1. m1 : ℤ-o
2. m2 : {vs:ℤ List| sorted(vs)} 
3. 0 ≤ m1
4. ↑even-int-list(m2)
⊢ ∃m':iMonomial(). ∃k:ℕ+. (mul-monomials(m';m') = mul-monomials(<m1, m2>;<k, []>) ∈ iMonomial())

---

Latex:

---

Latex:
\mforall{}m:iMonomial()
    ((\muparrow{}nonneg-monomial(m))  {}\mRightarrow{}  (\mexists{}m':iMonomial().  \mexists{}k:\mBbbN{}\msupplus{}.  (mul-monomials(m';m')  =  mul-monomials(m;<k,  []>\000C))))


By

---

Latex:
(Auto
  THEN  D  1
  THEN  RepUR  ``nonneg-monomial``  -1
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  D  -1)

---

Home Index