[shadowlight]

Yeah, this clarifies the logic. So because the algo above doesn't terminate it is not a proof.

The axiom of choice is an assumption that is neither known to be true or false.