---

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


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))
6. t1 : int_term()@i
7. t2 : int_term()@i
8. 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))
BY
{ (Auto THEN BHyp 5 THEN Auto THEN (RWO  "-1" 0 THENA Auto)) }

1
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))
6. t1 : int_term()@i
7. t2 : int_term()@i
8. t1 ≡ imonomial-term(m) (+) t2
⊢ (imonomial-term(m) (+) t2) (+) imonomial-term(u1) ≡ imonomial-term(m) (+) t2 (+) imonomial-term(u1)

---

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))
6.  t1  :  int\_term()@i
7.  t2  :  int\_term()@i
8.  t1  \mequiv{}  imonomial-term(m)  (+)  t2
\mvdash{}  accumulate  (with  value  t  and  list  item  m):
      t  (+)  imonomial-term(m)
    over  list:
        v
    with  starting  value:
      t1  (+)  imonomial-term(u1))  \mequiv{}  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))


By

---

Latex:
(Auto  THEN  BHyp  5  THEN  Auto  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index