Nuprl - Proof: isolate summand 2 1 1

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

1. n :

2. 0<n
3.

f:(

(n-1)

), m:

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

0 else f(x) fi | x < n-1)
4. f :

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

0 else f(x) fi | x < n-1)
6. m :

n
7. m = n-1

sum(f(x) | x < n) = f(n-1)+sum(if x=

n-1

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

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

Generated subgoal:

1 8. n = 0
9. n-1 = n-1
  sum(f(x) | x < n-1)+f(n-1)
  =
  f(n-1)+sum(if x=n-1 0 else f(x) fi | x < n-1)+0
2 steps

About:

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