---

Step * 2 1 of Lemma ipolynomial-term-cons

.....assertion..... 
1. m : iMonomial()
2. u : iMonomial()
3. v : iMonomial() List
⊢ ∀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))
BY
{ (ListInd (-1) THEN Reduce 0) }

1
1. m : iMonomial()
2. u : iMonomial()
⊢ ∀t1,t2:int_term().  (t1 ≡ imonomial-term(m) "+" t2 ⇒ t1 ≡ imonomial-term(m) "+" t2)

2
1. m : iMonomial()
2. u : iMonomial()
3. u1 : iMonomial()@i
4. v : iMonomial() List@i
5. ∀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))@i
⊢ ∀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(u1)) ≡ imonomial-term(m) "+" accumulate (with value t and list item m):
                                                            t "+" imonomial-term(m)
                                                           over list:
                                                             v
                                                           with starting value:
                                                            t2 "+" imonomial-term(u1)))

---

Latex:

---

Latex:
.....assertion..... 
1.  m  :  iMonomial()
2.  u  :  iMonomial()
3.  v  :  iMonomial()  List
\mvdash{}  \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))


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0)

---

Home Index