mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def sum(f(x;y) | x < n; y < m) == sum(sum(f(x;y) | y < m) | x < n)

is mentioned by

Thm* n,m:, f,g:(nm).
Thm* (x:n, y:m. f(x,y) = g(x,y))
Thm* 
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)		[double_sum_functionality]
Thm* n,m:, f,g:(nm), d:.
Thm* sum(f(x,y)-g(x,y) | x < n; y < m) = d
Thm* 
Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)+d		[double_sum_difference]
Thm* n,m:, f:(nm), x1,x2:n, y1,y2:m.
Thm* x1 = x2  y1 = y2
Thm* 
Thm* (x:n, y:m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0)
Thm* 
Thm* sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2)		[pair_support_double_sum]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb nat Sections MarkB generic Doc