Nuprl - Proof: pair support double sum 1

(15steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pair support double sum 1

1. n :

2. m :

3. f :

n

m

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* n:, f:(n), m:n. Thm* (x:n. x = m f(x) = 0) sum(f(x) \| x < n) = f(m) [n;x.sum(f(x,y) \| y < m);x1] THEN All ReduceSOAps

Generated subgoals:

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
  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(sum(f(x,y) | y < m) | x < n) = f(x1,y1)+f(x2,y2)
3 steps

About:

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

(15steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc