Nuprl - Proof: num iso 2 1 1 1

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

1. x' :

2. x'' :

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

5. 0<n
6. zero_rep = suc_rep(ncompose(suc_rep;n-1;zero_rep))

0 = n

By:	Thin 3 THEN Unab [`hzero_rep`] THEN Simp THEN StrongAuto

Generated subgoal:

1 3. n :
4. 0<n
5. (@x:. (y:. x = suc_rep(y)  ))
5. =
5. suc_rep(ncompose(suc_rep;n-1;@x:. (y:. x = suc_rep(y)  )))
  0 = n
10 steps

About:

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