Nuprl - Proof: fib coprime sfa2 1 1 2

(9steps total) PrintForm Definitions Lemmas NumThyExamples Sections NuprlLIB Doc

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

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
5.

k = 0
6.

k = 1

a,b:

. fib(n)

a+(fib(k-1)+fib(k-2))

b = 1

By:	Rewrite by n = k-1

Generated subgoal:

1 a,b:. fib(k-1)a+(fib(k-1)+fib(k-2))b = 1
3 steps

About:

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

(9steps total) PrintForm Definitions Lemmas NumThyExamples Sections NuprlLIB Doc