Nuprl - Proof: hnum iso def

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hnum iso def

and

(all(

a:hnum. equal(abs_num(rep_num(a)),a))

,all(

r:hind. equal(is_num_rep(r),equal(rep_num(abs_num(r)),r))))

By:	(HN (THEN ((L ((Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a). ((Thm* iso_pair('a;'b;P;rep;abs) ((Thm* ((Thm* (a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) = r)))) THEN StrongAuto THEN L Thm* iso_pair(;;is_num_rep;rep_num;abs_num) THEN StrongAuto

Generated subgoals:

None

About:

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