Nuprl - Proof: increasing is id 1 3

(17steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: increasing is id 1 3

1. k :

2. 0<k
3.

f:(

(k-1)

(k-1)). increasing(f;k-1)

(

i:

(k-1). f(i) = i)
4. f :

k

k
5. increasing(f;k)
6. i :

k
7.

i:

(k-1). (

j.f(j))(i) = i

f(i) = i

By:	Decide (i = k-1)

Generated subgoals:

1 8. i = k-1
f(i) = i
6 steps

2 8. i = k-1
f(i) = i
1 step

About:

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

(17steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc