---

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


1. v : Top List@i
2. ∀n:ℤ. (accumulate (with value b and list item e): b + 1over list:  vwith starting value: n) = (||v|| + n) ∈ ℤ)
⊢ ||v|| = accumulate (with value b and list item e): b + 1over list:  vwith starting value: 0) ∈ ℕ
BY
{ ((InstHyp [⌈0⌉] (-1)⋅ THEN Auto) THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)  THEN  Auto')

---

Home Index