for n being non zero Nat
for k being Nat st k < 2 to_power n holds
Absval (n -BinarySequence k) = k