---

Step * 2 of Lemma ipolynomial-term-cons-ringeq


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))
BY
{ ((Assert ⌜∀t1,t2:int_term().
              (t1 ≡ imonomial-term(m) (+) t2
              ⇒ accumulate (with value t and list item m):
                  t (+) imonomial-term(m)
                 over list:
                   v
                 with starting value:
                  t1) ≡ imonomial-term(m)
                 (+) accumulate (with value t and list item m):
                      t (+) imonomial-term(m)
                     over list:
                       v
                     with starting value:
                      t2))⌝⋅
   THENM ((BHyp -1  THEN Auto) THEN D 0 THEN Auto)
   )
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN BHyp 6 
   THEN Auto
   THEN (RWO  "-1" 0 THENA Auto)
   THEN D 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}t1,t2:int\_term().
                        (t1  \mequiv{}  imonomial-term(m)  (+)  t2
                        {}\mRightarrow{}  accumulate  (with  value  t  and  list  item  m):
                                t  (+)  imonomial-term(m)
                              over  list:
                                  v
                              with  starting  value:
                                t1)  \mequiv{}  imonomial-term(m)
                              (+)  accumulate  (with  value  t  and  list  item  m):
                                        t  (+)  imonomial-term(m)
                                      over  list:
                                          v
                                      with  starting  value:
                                        t2))\mkleeneclose{}\mcdot{}
  THENM  ((BHyp  -1    THEN  Auto)  THEN  D  0  THEN  Auto)
  )
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  BHyp  6 
  THEN  Auto
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index