1. n : 
2. n1:. n1<n  (k:. k = n1+1  (x,y:. fib(n1)x+fib(k)y = 1))
3. k : 
4. 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	5. k = 0  k = 1   a,b:. fib(n)a+1b = 1	1 step
2	5. k = 0 6. 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