---

Step * 1 1 2 2 1 1 1 2 of Lemma mul-mono-poly_wf


1. m : iMonomial()
2. u : iMonomial()
3. u1 : iMonomial()
4. v : iMonomial() List
5. ∀i:ℕ||[u1 / v]|| + 1. ∀j:ℕi.  imonomial-less([u; [u1 / v]][j];[u; [u1 / v]][i])
6. ∀i:ℕ||mul-mono-poly(m;[u1 / v])||. ∀j:ℕi.  imonomial-less(mul-mono-poly(m;[u1 / v])[j];mul-mono-poly(m;[u1 / v])[i])
7. i : ℕ||[mul-monomials(m;u) / mul-mono-poly(m;[u1 / v])]||
8. j : ℕi
9. j = 0 ∈ ℤ
⊢ imonomial-less(mul-monomials(m;u);mul-mono-poly(m;[u1 / v])[0])
BY
{ (RepUR ``mul-mono-poly`` 0
   THEN Fold `mul-mono-poly` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0) }

1
1. m : iMonomial()
2. u : iMonomial()
3. u1 : iMonomial()
4. v : iMonomial() List
5. ∀i:ℕ||[u1 / v]|| + 1. ∀j:ℕi.  imonomial-less([u; [u1 / v]][j];[u; [u1 / v]][i])
6. ∀i:ℕ||mul-mono-poly(m;[u1 / v])||. ∀j:ℕi.  imonomial-less(mul-mono-poly(m;[u1 / v])[j];mul-mono-poly(m;[u1 / v])[i])
7. i : ℕ||[mul-monomials(m;u) / mul-mono-poly(m;[u1 / v])]||
8. j : ℕi
9. j = 0 ∈ ℤ
⊢ imonomial-less(mul-monomials(m;u);mul-monomials(m;u1))

---

Latex:

---

Latex:

1.  m  :  iMonomial()
2.  u  :  iMonomial()
3.  u1  :  iMonomial()
4.  v  :  iMonomial()  List
5.  \mforall{}i:\mBbbN{}||[u1  /  v]||  +  1.  \mforall{}j:\mBbbN{}i.    imonomial-less([u;  [u1  /  v]][j];[u;  [u1  /  v]][i])
6.  \mforall{}i:\mBbbN{}||mul-mono-poly(m;[u1  /  v])||.  \mforall{}j:\mBbbN{}i.
          imonomial-less(mul-mono-poly(m;[u1  /  v])[j];mul-mono-poly(m;[u1  /  v])[i])
7.  i  :  \mBbbN{}||[mul-monomials(m;u)  /  mul-mono-poly(m;[u1  /  v])]||
8.  j  :  \mBbbN{}i
9.  j  =  0
\mvdash{}  imonomial-less(mul-monomials(m;u);mul-mono-poly(m;[u1  /  v])[0])


By

---

Latex:
(RepUR  ``mul-mono-poly``  0
  THEN  Fold  `mul-mono-poly`  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0)

---

Home Index