2. f :
n
3. m :
n
4. k :
n
5.
m = k
6.
x:n. x = m 
x = k f(x) = 0
7. sum(f(x) | x < n) = f(m)+sum(if x=
m
0 else f(x) fi | x < n)
sum(if x=m 0 else f(x) fi | x < n) = f(k)
n
n
n
m = k
x:n. x = m x = k f(x) = 0
m 0 else f(x) fi | x < n)
sum(if x=m 0 else f(x) fi | x < n) = f(k)| By: |
Thm* n:, f:(n), m:n.
Thm* ( x:n. x = m f(x) = 0) sum(f(x) | x < n) = f(m)
[n;  x.if x=m 0 else f(x) fi;k]
THEN All ReduceSOAps |
| 1 |
x:n. x = m x = k f(x) = 0
7. sum(f(x) | x < n) = f(m)+sum(if x= m 0 else f(x) fi | x < n)
8. x : n
9. x = k
if x=m 0 else f(x) fi = 0 | 1 step |
| 2 |
x:n. x = m x = k f(x) = 0
7. sum(f(x) | x < n) = f(m)+sum(if x= m 0 else f(x) fi | x < n)
8. sum(if x= m 0 else f(x) fi | x < n) = if k=m 0 else f(k) fi
sum(if x=m 0 else f(x) fi | x < n) = f(k) | 2 steps |
About:
 |  |  |  |  |
 |  |  |  |  |