Nuprl - Proof: hsum iso def 1

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

'a,'b:S.

(

a:'a+'b. abs_sum(rep_sum(a)) = a

'a+'b)

& (

r:(

). is_sum_rep(r) = ((rep_sum(abs_sum(r))) =

r))

By:	((RepeatMFor 2 (Analyze 0)) (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)))) THENA Try (Complete Auto)

Generated subgoals:

1 1. 'a : S
2. 'b : S
'a'b S
1 step

2 1. 'a : S
2. 'b : S
iso_pair('a+'b;'a'b;is_sum_rep;rep_sum;abs_sum)
14 steps

About:

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

1	1. 'a : S 2. 'b : S 'a'b S	1 step
2	1. 'a : S 2. 'b : S iso_pair('a+'b;'a'b;is_sum_rep;rep_sum;abs_sum)	14 steps