Nuprl - Proof: fib coprime sfa2 1 1 1

(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 1

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

k = 1

a,b:

. fib(n)

a+1

b = 1

By:	Witness: 0 \| 1

Generated subgoals:

None

About:

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

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