Nuprl - Proof: sum split 2 2 2 1 1

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

1. n :

2. 0<n
3.

f:(

(n-1)

), m:

(n-1+1).
3. sum(f(x) | x < n-1) = sum(f(x) | x < m)+sum(f(x+m) | x < n-1-m)
4. f :

(n-1+1). sum(f(x) | x < n-1) = sum(f(x) | x < m)+sum(f(x+m) | x < n-1-m)
6. m :

(n+1)
7.

m = n-1
8.

m = n
9. sum(f(x) | x < n-1) = sum(f(x) | x < m)+sum(f(x+m) | x < n-1-m)
10. s :

11. sum(f(x) | x < m) = s

sum(f(x) | x < n) = s+sum(f(x+m) | x < n-m)

By:	Unfold `sum` 0 THEN RecUnfold `primrec` 0 THEN Fold `sum` 0 THEN RepeatFor 2 (SplitOnConclITE THEN Reduce 0)

Generated subgoals:

None

About:

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