for x being Nat ex m being Nat st x < 2 to_power m