Nuprl - Proof: fincr formation 1 2 1 1

(25steps total) PrintForm Definitions rfunction 1 Sections StandardLIB Doc

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

1. i :

2. f : {f | i:{i1:

| i1<i }

if i=

0

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

4.

j1:

. j1<j

j1<i

f(j1)

j<i

f(j)

By:

Analyze 0

Generated subgoal:

1 5. j<i
f(j)
5 steps

About:

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

(25steps total) PrintForm Definitions rfunction 1 Sections StandardLIB Doc