'a,'b:S.
  and
  (all(a:hsum('a; 'b). equal(abs_sum(rep_sum(a)),a))
  ,all
  ,(r:hbool  'a  'b  hbool. equal
  ,(r:hbool  'a  'b  hbool. (is_sum_rep(r)
  ,(r:hbool  'a  'b  hbool. ,equal(rep_sum(abs_sum(r)),r))))

1

'a,'b:S.   (a:'a+'b. abs_sum(rep_sum(a)) = a  'a+'b)   & (r:('a'b). is_sum_rep(r) = ((rep_sum(abs_sum(r))) = r))

16 steps

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