Nuprl - Proof: pair support 1 1

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

1. n :

2. f :

3. m :

n
4. k :

n
5.

m = k
6.

x = m

x = k

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

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

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

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

Generated subgoals:

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

2 8. sum(if x=m 0 else f(x) fi | x < n) = f(k)
sum(f(x) | x < n) = f(m)+f(k)
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) = f(k)	4 steps
2	8. sum(if x=m 0 else f(x) fi \| x < n) = f(k) sum(f(x) \| x < n) = f(m)+f(k)	Auto