---

Step * of Lemma mul-ipoly_wf

∀[p,q:iPolynomial()].  (mul-ipoly(p;q) ∈ iPolynomial())
BY
{ (Auto THEN Unfold `mul-ipoly` 0 THEN (CallByValueReduce 0 THENA Auto) THEN RepeatFor 2 (D 1) THEN Reduce 0) }

1
1. ∀i:ℕ||[]||. ∀j:ℕi.  imonomial-less([][j];[][i])
2. q : iPolynomial()
⊢ [] ∈ iPolynomial()

2
1. u : iMonomial()
2. v : iMonomial() List
3. ∀i:ℕ||[u / v]||. ∀j:ℕi.  imonomial-less([u / v][j];[u / v][i])
4. q : iPolynomial()
⊢ let qq ⟵ q
  in if null(qq)
  then []
  else accumulate (with value sofar and list item m):
        add-ipoly(sofar;mul-mono-poly(m;qq))
       over list:
         v
       with starting value:
        mul-mono-poly(u;qq))
  fi  ∈ iPolynomial()

---

Latex:

---

Latex:
\mforall{}[p,q:iPolynomial()].    (mul-ipoly(p;q)  \mmember{}  iPolynomial())


By

---

Latex:
(Auto
  THEN  Unfold  `mul-ipoly`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RepeatFor  2  (D  1)
  THEN  Reduce  0)

---

Home Index