Nuprl - Proof: singleton support sum 1 1

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

1. n :

2. f :

3. m :

n
4.

x = m

f(x) = 0
5. sum(f(x) | x < n) = f(m)+sum(if x=

0 else f(x) fi | x < n)

sum(f(x) | x < n) = f(m)

By:	Assert (sum(if x=m 0 else f(x) fi \| x < n) = 0)

Generated subgoals:

1 sum(if x=m 0 else f(x) fi | x < n) = 0
2 steps

2 6. sum(if x=m 0 else f(x) fi | x < n) = 0
sum(f(x) | x < n) = f(m)
Auto

About:

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

1	sum(if x=m 0 else f(x) fi \| x < n) = 0	2 steps
2	6. sum(if x=m 0 else f(x) fi \| x < n) = 0 sum(f(x) \| x < n) = f(m)	Auto