'b,'a:S.
Thm* all
Thm* (
e:'a. equal(inl(e),abs_sum(b:hbool. x:'a. y:'b. and(equal(x,e),b))))'a,'b:S.
Thm* (
x:'a+'b. abs_sum(rep_sum(x)) = x 
'a+'b)
Thm* & (
x:(
'a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) =
x))| Rank | Theorem | Name |
| 4 | 'b,'a:S.
Thm* all Thm* ( e:'a. equal(inl(e),abs_sum(b:hbool. x:'a. y:'b. and(equal(x,e),b)))) | [hinl_def] |
| cites the following: | ||
| 3 | 'a,'b:S.
Thm* ( x:'a+'b. abs_sum(rep_sum(x)) = x 'a+'b)
Thm* & ( x:('a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) = x)) | [sum_iso] |