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


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

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

2
1. Top List@i
2. ∀n:ℤ(accumulate (with value and list item e): 1over list:  vwith starting value: n) (||v|| n) ∈ ℤ)
⊢ ||v|| accumulate (with value and list item e): 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