Nuprl - Proof: hsuc def 1 2 1 1 2

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

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
4. rep_num(m+1-1) = rep_num(m)

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

By:	Unab [`hrep_num`] THEN All AbReduce THEN StrongAuto

Generated subgoals:

None

About:

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