1. n : 
2. k:. k<n  (x,y:. fib(k)x+fib(k+1)y = 1)
  a,b:. fib(n)a+fib(n+1)b = 1

By:	Compute fib(n+1) * if n+1=0  n+1=1 1 else fib(n+1-1)+fib(n+1-2) fi THEN SplitOnConclITE

1	a,b:. fib(n)a+1b = 1	1 step
2	3. n+1 = 1   a,b:. fib(n)a+(fib(n)+fib(n-1))b = 1	4 steps

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