Nuprl - Proof: fib coprime sfa2 1 1 2 1 1

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

1. n :

n1:

. n1<n

(

. k = n1+1

(

x,y:

. fib(n1)

x+fib(k)

y = 1))
3. k :

4. k = n+1
5.

k = 0
6.

k = 1

a,b:

. fib(k-2)

b+fib(k-1)

(a+b) = 1

By:	Use:[k-2 \| k-1] Inst: Hyp:2

Generated subgoal:

1 7. x,y:. fib(k-2)x+fib(k-1)y = 1
a,b:. fib(k-2)b+fib(k-1)(a+b) = 1
1 step

About:

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