mb list 2 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:(nm), p:(nn), q:(mm).
Thm* Bij(n; n; p)
Thm* 
Thm* Bij(m; m; q)
Thm* 
Thm* sum(f(p(x),q(y)) | x < n; y < m) = sum(f(x,y) | x < n; y < m)		[permute_double_sum]
Def count(x < y in L | P(x;y))
Def == sum(if (i<j)P(L[i];L[j]) 1 else 0 fi | i < ||L||; j < ||L||)		[count_pairs]

In prior sections: mb nat

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

mb list 2 Sections MarkB generic Doc