for n being non zero Nat
for x, y being Tuple of n, BOOLEAN st y = 0* n holds
( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y )