1. n : 
2. 0<n
3. k:. k = n-1+1  (x,y:. fib(n-1)x+fib(k)y = 1)
4. k : 
5. k = n+1
  x,y:. fib(n)x+fib(k)y = 1

By:	Compute fib(k) * if k=0  k=1 1 else fib(k-1)+fib(k-2) fi THEN SplitOnConclITE THEN CBV: a,b:. <prop>

1

6. k = 0 7. k = 1   a,b:. fib(n)a+(fib(k-1)+fib(k-2))b = 1

4 steps

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