---

Step * 2 of Lemma ipolynomial-term-cons


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))
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 BLemma `equiv_int_terms_weakening` THEN Auto)
) }

1
.....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))

---

Latex:

---

Latex:

1.  m  :  iMonomial()
2.  u  :  iMonomial()
3.  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  BLemma  `equiv\_int\_terms\_weakening`  THEN  Auto)
)

---

Home Index