---

Step * of Lemma mul-monomials-equiv

∀[m1,m2:iMonomial()].  imonomial-term(mul-monomials(m1;m2)) ≡ imonomial-term(m1) (*) imonomial-term(m2)
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)} 
⊢ imonomial-term(<m5 * m3, merge-int(m6;m4)>) ≡ imonomial-term(<m5, m6>) (*) imonomial-term(<m3, m4>)

---

Latex:

---

Latex:
\mforall{}[m1,m2:iMonomial()].
    imonomial-term(mul-monomials(m1;m2))  \mequiv{}  imonomial-term(m1)  (*)  imonomial-term(m2)


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