Nuprl - Proof: num iso 2 1 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

3. n :

4. 0<n
5. (@x:

. (

x = suc_rep(y)))
5. =
5. suc_rep(ncompose(suc_rep;n-1;@x:

. (

x = suc_rep(y))))

0 = n

By:	MoveToConcl 5 THEN ChooseDC THEN Simp THEN StrongAuto

Generated subgoals:

1 5. x :
6. y:. x = suc_rep(y)
7. x = suc_rep(ncompose(suc_rep;n-1;x))
  0 = n
1 step

2   x:. y:. x = suc_rep(y)
8 steps

About:

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

1	5. x : 6. y:. x = suc_rep(y) 7. x = suc_rep(ncompose(suc_rep;n-1;x)) 0 = n	1 step
2	x:. y:. x = suc_rep(y)	8 steps