---

Step * of Lemma mul-mono-poly-ringeq

∀[r:CRng]. ∀[m:iMonomial()]. ∀[p:iMonomial() List].
  ipolynomial-term(mul-mono-poly(m;p)) ≡ imonomial-term(m) (*) ipolynomial-term(p)
BY
{ xxx(Auto
      THEN ListInd (-1)
      THEN RepUR ``mul-mono-poly`` 0
      THEN Try ((Fold `mul-mono-poly` 0 THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto)))))xxx }

1
1. r : CRng
2. m : iMonomial()
⊢ ipolynomial-term([]) ≡ imonomial-term(m) (*) ipolynomial-term([])

2
.....aux..... 
1. r : CRng
2. m : iMonomial()
3. u : iMonomial()
4. v : iMonomial() List
5. ipolynomial-term(mul-mono-poly(m;v)) ≡ imonomial-term(m) (*) ipolynomial-term(v)
⊢ (mul-mono-poly(m;v))↓

3
1. r : CRng
2. m : iMonomial()
3. u : iMonomial()
4. v : iMonomial() List
5. ipolynomial-term(mul-mono-poly(m;v)) ≡ imonomial-term(m) (*) ipolynomial-term(v)
⊢ ipolynomial-term([mul-monomials(m;u) / mul-mono-poly(m;v)]) ≡ imonomial-term(m) (*) ipolynomial-term([u / v])

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[m:iMonomial()].  \mforall{}[p:iMonomial()  List].
    ipolynomial-term(mul-mono-poly(m;p))  \mequiv{}  imonomial-term(m)  (*)  ipolynomial-term(p)


By

---

Latex:
xxx(Auto
        THEN  ListInd  (-1)
        THEN  RepUR  ``mul-mono-poly``  0
        THEN  Try  ((Fold  `mul-mono-poly`  0  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))))xxx

---

Home Index