Nuprl - Proof: increasing is id 1 1 1

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

1. k :

2. 0<k
3.

f:(

(k-1)

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

(

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

k
5. increasing(f;k)
6.

k
7. j :

(k-1)
8. f(k-1)<k

f(j)

(k-1)

By:	Assert (i:(k-1). f(i) (k-1))

Generated subgoals:

1   i:(k-1). f(i)  (k-1)
3 steps

2 9. i:(k-1). f(i)  (k-1)
  f(j)  (k-1)
1 step

About:

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

1	i:(k-1). f(i) (k-1)	3 steps
2	9. i:(k-1). f(i) (k-1) f(j) (k-1)	1 step