for m being Nat
for i being Integer ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>