Nuprl - Proof: increasing is id 1

(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

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

f(i) = i

By:	AllHyps (InstHyp [j.f(j)])

Generated subgoals:

1 7. j : (k-1)
  f(j)  (k-1)
6 steps

2   increasing(j.f(j);k-1)
1 step

3 7. i:(k-1). (j.f(j))(i) = i
  f(i) = i
8 steps

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