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