theorem Th15: :: BINARI_2:15

for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>))