:: deftheorem defines Int_add_ovfl BINARI_2:def 4 :
for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN holds Int_add_ovfl (z1,z2) = (('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry (z1,z2)) /. n);