1. n : 
2. m : 
3. f : nm
4. x1 : n
5. x2 : n
6. y1 : m
7. y2 : m
8. x1 = x2  y1 = y2
9. x:n, y:m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0
10. x1 = x2
  sum(sum(f(x,y) | y < m) | x < n) = f(x1,y1)+f(x2,y2)

By:	Inst Thm: pair support [n;x.sum(f(x,y) | y < m);x1;x2] THEN All ReduceSOAps

1	9. x:n, y:m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0 10. x1 = x2 11. x : n 12. x = x1 13. x = x2   sum(f(x,y) | y < m) = 0	2 steps
2	9. x:n, y:m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0 10. x1 = x2 11. sum(sum(f(x,y) | y < m) | x < n) = sum(f(x1,y) | y < m)+sum(f(x2,y) | y < m)   sum(sum(f(x,y) | y < m) | x < n) = f(x1,y1)+f(x2,y2)	5 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html