---

Step * of Lemma ipolynomial-term-cons-ringeq

∀[r:Rng]. ∀[m:iMonomial()]. ∀[p:iMonomial() List].
  ipolynomial-term([m / p]) ≡ imonomial-term(m) (+) ipolynomial-term(p)
BY
{ (Auto THEN DVar `p' THEN RepUR ``ipolynomial-term`` 0) }

1
1. r : Rng
2. m : iMonomial()
⊢ imonomial-term(m) ≡ imonomial-term(m) (+) "0"

2
1. r : Rng
2. m : iMonomial()
3. u : iMonomial()
4. v : iMonomial() List
⊢ accumulate (with value t and list item m):
   t (+) imonomial-term(m)
  over list:
    v
  with starting value:
   imonomial-term(m) (+) imonomial-term(u)) ≡ imonomial-term(m)
(+) accumulate (with value t and list item m):
     t (+) imonomial-term(m)
    over list:
      v
    with starting value:
     imonomial-term(u))

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[m:iMonomial()].  \mforall{}[p:iMonomial()  List].
    ipolynomial-term([m  /  p])  \mequiv{}  imonomial-term(m)  (+)  ipolynomial-term(p)


By

---

Latex:
(Auto  THEN  DVar  `p'  THEN  RepUR  ``ipolynomial-term``  0)

---

Home Index