Nuprl - Proof: fincr formation 1 2 1 1 1 1 1 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 1 1 1 1

1. i :

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

| i1<i }

if i=

0

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

4. j<i
5. y : if j=

0

else {f(j-1)...} fi
6. y = f(j)
7. j

0
8. f(j-1)

9.

i:

, j:{i...}. j

f(j)

By:	(With (f(j-1)) (Analyze -1)) THEN (With (f(j)) (Analyze -1))

Generated subgoals:

None

About:

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

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