|a|
if P(v)
1 else 0 fi+sum(if x=
i0 ;P(a[i:=v][x])1 else 0 fi | x < |a|) = if P(a[i]) 1 else 0 fi+sum(if x=i0 ;P(a[x])1 else 0 fi | x < |a|)+if P(v)if P(a[i]) 0 else 1 fi ;P(a[i])-1 else 0 fi
i0 ;P(a[i:=v][x])1 else 0 fi | x < |a|) = sum(if x=i0 ;P(a[x])1 else 0 fi | x < |a|))
((BackThru
Thm* 
n:, f,g:(n
). (i:n. f(i) = g(i)) 
sum(f(x) | x < n) = sum(g(x) | x < n))
THEN
(RWO
Thm* a:array(T), j,i:|a|, v:T. a[i:=v][j] ~ if j=i v else a[j] fi
0)
THEN
SplitOnConclITE
THEN
(Reduce 0))
None
About:
| | | | | | |
 |  |  |  |  |  |