Nuprl - Proof: hsuc def 1 2 1 1

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

1. m :

a,r:

.
2. iso_pair(

;

;is_num_rep;rep_num;abs_num)

rep_num(a) = r

a = abs_num(r)
3. m+1>0

ncompose(suc_rep;m+1-1;zero_rep) = rep_num(m)

By:	Assert (rep_num(m+1-1) = rep_num(m))

Generated subgoals:

1   rep_num(m+1-1) = rep_num(m)
2 steps

2 4. rep_num(m+1-1) = rep_num(m)
  ncompose(suc_rep;m+1-1;zero_rep) = rep_num(m)
1 step

About:

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

1	rep_num(m+1-1) = rep_num(m)	2 steps
2	4. rep_num(m+1-1) = rep_num(m) ncompose(suc_rep;m+1-1;zero_rep) = rep_num(m)	1 step