theorem Th13: :: BINARI_2:13

for m being non zero Nat
for x being Tuple of m, BOOLEAN holds Absval ('not' x) = ((- (Absval x)) + (2 to_power m)) - 1