:: deftheorem defines add_ovfl BINARITH:def 6 :
for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN holds add_ovfl (z1,z2) = (((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n));