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