---

Step * of Lemma ipolynomial-term-cons

∀[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. m : iMonomial()
⊢ imonomial-term(m) ≡ imonomial-term(m) "+" "0"

2
1. m : iMonomial()
2. u : iMonomial()
3. 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{}[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