The assertion that at least one selection algorithm succeeds without presenting that algorithm _is_ the axiom of choice.

By _assuming_ that program terminates, you are yourself taking the axiom of choice.

If it _does_ terminate, then it's not an axiom anymore it's a proof.