---

Step * 1 of Lemma mul-mono-poly_wf


1. m : iMonomial()
2. p : iMonomial() List
3. ∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i])
4. i : ℕ||mul-mono-poly(m;p)||
5. j : ℕi
⊢ imonomial-less(mul-mono-poly(m;p)[j];mul-mono-poly(m;p)[i])
BY
{ RepeatFor 3 (MoveToConcl (-1)) }

1
1. m : iMonomial()
2. p : iMonomial() List
⊢ (∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i]))
⇒ (∀i:ℕ||mul-mono-poly(m;p)||. ∀j:ℕi.  imonomial-less(mul-mono-poly(m;p)[j];mul-mono-poly(m;p)[i]))

---

Latex:

---

Latex:

1.  m  :  iMonomial()
2.  p  :  iMonomial()  List
3.  \mforall{}i:\mBbbN{}||p||.  \mforall{}j:\mBbbN{}i.    imonomial-less(p[j];p[i])
4.  i  :  \mBbbN{}||mul-mono-poly(m;p)||
5.  j  :  \mBbbN{}i
\mvdash{}  imonomial-less(mul-mono-poly(m;p)[j];mul-mono-poly(m;p)[i])


By

---

Latex:
RepeatFor  3  (MoveToConcl  (-1))

---

Home Index