Nuprl - Proof: num iso 2 1 2 1 1 1

(46steps total) PrintForm Definitions hol num Sections HOLlib Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 2 1 2 1 1 1

1. x' :

2. x'' :

3. ncompose(suc_rep;x';zero_rep) = ncompose(suc_rep;x'';zero_rep)
4. m :

5. 0<m
6.

n:

.
6. m-1<n
6.

6. ncompose(suc_rep;m-1;zero_rep) = suc_rep(ncompose(suc_rep;n-1;zero_rep))
6.

6. m-1 = n
7. n :

8. m<n
9. suc_rep(ncompose(suc_rep;m-1;zero_rep))
9. =
9. suc_rep(ncompose(suc_rep;n-1;zero_rep))
10. 0<n

one_one(

;

;suc_rep)

By:	All Thin THEN Unab [`hsuc_rep`] THEN ChooseDC THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

1 1. f :
2. one_one(;;f)
3. onto(;;f)
one_one(;;x:. f(x))
2 steps

2 f:(). one_one(;;f) & onto(;;f)
2 steps

About:

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

(46steps total) PrintForm Definitions hol num Sections HOLlib Doc