Nuprl - Proof: fincr wf 1 4 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fincr wf 1 4 2 1 1

1. i :

2. f : {f | i:{z:

| z<i }

if i=

else {f(i-1)...} fi}
3.

j:{k:

| k<i }. f(j)

4. i

f(i-1)

By:	With (i-1) (Analyze -2)

Generated subgoals:

None

About:

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