Nuprl - Proof: bijection restriction

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bijection restriction

, f:(

k).

0<k

Bij(

k; f)

f(k-1) = k-1

(k-1)

(k-1) & Bij(

(k-1);

(k-1); f)

By:	Auto THEN Unfold `guard` 0 THEN AssertSubterm [1]

Generated subgoals:

1 1. k :
2. f : kk
3. 0<k
4. Bij(k; k; f)
5. f(k-1) = k-1
  f  (k-1)(k-1)
3 steps

2 1. k :
2. f : kk
3. 0<k
4. Bij(k; k; f)
5. f(k-1) = k-1
6. f  (k-1)(k-1)
  Bij((k-1); (k-1); f)
2 steps

About:

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

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

1	1. k : 2. f : kk 3. 0<k 4. Bij(k; k; f) 5. f(k-1) = k-1 f (k-1)(k-1)	3 steps
2	1. k : 2. f : kk 3. 0<k 4. Bij(k; k; f) 5. f(k-1) = k-1 6. f (k-1)(k-1) Bij((k-1); (k-1); f)	2 steps