---

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


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

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

2
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) ∈ ℕ

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbZ{}
                    (accumulate  (with  value  b  and  list  item  e):
                        b  +  1
                      over  list:
                          v
                      with  starting  value:
                        n)
                    =  (||v||  +  n))\mkleeneclose{}\mcdot{}

---

Home Index