> My only quibble with this one is with step 19 ("hangIf3") which relies on "infinity is not considered even" — that is a distraction IMO, and if I understand correctly (have not thought about this carefully) the example could be replaced with something that involves an actual odd number.
Indeed, you could just replace haltIf3or7 by haltIf3or5or7 (or whatever). (And, of course, whether or not infinity is considered even cannot be deduced from the information given, so relying on this technicality here I'd argue is beyond distracting and into the realm of so underspecified that it might be wrong. Or we could raise the same objection mentioned earlier, that it's not specified what kind of object `n` is, and numeric types often have only finitely many inhabitants ….)