---

Step * of Lemma mul-monomials_wf

∀[m1,m2:iMonomial()].  (mul-monomials(m1;m2) ∈ iMonomial())
BY
{ ((UnivCD THENA Auto)
   THEN D 2
   THEN D 1
   THEN RepUR ``mul-monomials`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (RWO "merge-int-accum-sq" 0 THENA Auto)) }

1
1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
⊢ <m5 * m3, merge-int(m6;m4)> ∈ iMonomial()

---

Latex:

---

Latex:
\mforall{}[m1,m2:iMonomial()].    (mul-monomials(m1;m2)  \mmember{}  iMonomial())


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  2
  THEN  D  1
  THEN  RepUR  ``mul-monomials``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (RWO  "merge-int-accum-sq"  0  THENA  Auto))

---

Home Index