:: deftheorem defines are_summable BINARITH:def 7 :
for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN holds
( z1,z2 are_summable iff add_ovfl (z1,z2) = FALSE );