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

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

1. x' :

2. x'' :

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

5. 0<m
6.

.
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
11. one_one(

;

;suc_rep)

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

By:	Unab [`one_one`] THEN FwdThru 11 [9] THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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