T:Type, P:(T
), a:array(T). array-count(v.P(v);a) 
(|a|+1)n:, f:(n
). (x:n. 0
f(x)) 
0sum(f(x) | x < n)k,b:, f:(k). (x:k. f(x)b) sum(f(x) | x < k)b
k| Theorem | Name |
| Thm* T:Type, P:(T), a:array(T). array-count(v.P(v);a) (|a|+1) | [array-count_wf] |
| cites | |
| Thm* n:, f:(n). (x:n. 0f(x)) 0sum(f(x) | x < n) | [non_neg_sum] |
| Thm* k,b:, f:(k). (x:k. f(x)b) sum(f(x) | x < k)bk | [sum_bound] |