(3steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
array-count
wf
1
1.
T:
Type
2.
P:
T
3.
a:
array(T)
0
sum(if P(a[i])
1 else 0 fi | i < |a|)
By:
BackThru
Thm*
n:
, f:(
n
). (
x:
n. 0
f(x))
0
sum(f(x) | x < n)
THEN
SplitOnConclITE
Generated subgoals:
None
About:
(3steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
0
sum(if P(a[i])
1 else 0 fi | i < |a|)
n:
, f:(n
). (x:n. 0f(x)) 
0sum(f(x) | x < n)
