We present a formulation of the Collatz conjecture that is potentially more amenable to modeling and analysis by automated termination checking tools.