---

Step * 1 1 1 of Lemma es-interface-count-as-accum

.....assertion..... 
1. v : Top List@i
⊢ ∀n:ℤ. (accumulate (with value b and list item e): b + 1over list:  vwith starting value: n) = (||v|| + n) ∈ ℤ)
BY
{ (ListInd (-1) THEN Reduce 0 THEN Auto)⋅ }

1
1. u : Top@i
2. v : Top List@i
3. ∀n:ℤ. (accumulate (with value b and list item e): b + 1over list:  vwith starting value: n) = (||v|| + n) ∈ ℤ)@i
4. n : ℤ@i
⊢ accumulate (with value b and list item e): b + 1over list:  vwith starting value: n + 1) = ((||v|| + 1) + n) ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
1.  v  :  Top  List@i
\mvdash{}  \mforall{}n:\mBbbZ{}
        (accumulate  (with  value  b  and  list  item  e):
            b  +  1
          over  list:
              v
          with  starting  value:
            n)
        =  (||v||  +  n))


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index