:: deftheorem Def2 defines 2sComplement BINARI_4:def 2 :
for m being Nat
for i being Integer holds
( ( i < 0 implies 2sComplement (m,i) = m -BinarySequence |.((2 to_power (MajP (m,|.i.|))) + i).| ) & ( not i < 0 implies 2sComplement (m,i) = m -BinarySequence |.i.| ) );