Nuprl - Proof: fib wf 1

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

1. n :

n1:

. n1<n

fib(n1)

fib(n)

By:	RecCaseSplit `fib`

Generated subgoals:

1 3. n = 0  n = 1
  1
Auto

2 3. n = 0 & n = 1
  fib(n-1)+fib(n-2)
1 step

About:

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

1	3. n = 0 n = 1 1	Auto
2	3. n = 0 & n = 1 fib(n-1)+fib(n-2)	1 step