Nuprl - Proof: pair support double sum

(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

n,m:

, f:(

), x1,x2:

n, y1,y2:

x1 = x2

y1 = y2

(

n, y:

(x = x1 & y = y1)

(x = x2 & y = y2)

f(x,y) = 0)

sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2)

By:	Auto THEN Unfold `double_sum` 0 THEN Decide (x1 = x2)

Generated subgoals:

1 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)
6 steps

2 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)
8 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

1	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)	6 steps
2	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)	8 steps