---

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


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) ∈ ℤ
BY
{ (RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "-2"  0  THEN  Auto)

---

Home Index