---

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


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
6. t1 : int_term()@i
7. t2 : int_term()@i
8. t1 ≡ imonomial-term(m) "+" t2@i
⊢ imonomial-term(m) "+" t2 "+" imonomial-term(u1) ≡ imonomial-term(m) "+" t2 "+" imonomial-term(u1)
BY
{ ((D 0 THEN Auto) THEN RepUR ``int_term_value`` 0 THEN Fold `int_term_value` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  m  :  iMonomial()
2.  u  :  iMonomial()
3.  u1  :  iMonomial()@i
4.  v  :  iMonomial()  List@i
5.  \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))@i
6.  t1  :  int\_term()@i
7.  t2  :  int\_term()@i
8.  t1  \mequiv{}  imonomial-term(m)  "+"  t2@i
\mvdash{}  imonomial-term(m)  "+"  t2  "+"  imonomial-term(u1)  \mequiv{}  imonomial-term(m)  "+"  t2  "+"  imonomial-term(u1)


By

---

Latex:
((D  0  THEN  Auto)  THEN  RepUR  ``int\_term\_value``  0  THEN  Fold  `int\_term\_value`  0  THEN  Auto)

---

Home Index