Nuprl - Proof: hsuc def 1 2

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

1. m :

a,r:

.
2. iso_pair(

;

;is_num_rep;rep_num;abs_num)

rep_num(a) = r

a = abs_num(r)

rep_num(m+1) = suc_rep(rep_num(m))

By:	Assert (m+1>0) THEN StrongAuto THEN UnfoldFirst `hrep_num` 0 THEN Simp THEN StrongAuto

Generated subgoal:

1 3. m+1>0
suc_rep(ncompose(suc_rep;m+1-1;zero_rep)) = suc_rep(rep_num(m))
5 steps

About:

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