But this is bash, which runs on Unixy systems, which have exec. behave_differently is trivial:

    echo foo
    exec “$@“

This little hack will carry over to some, but possibly not all [0], models of computation. Fixing this would involve cleaning up some definitions in the proof.

[0] Specifically, it does carry over to any model of a program that outputs a stream of symbols one at a time. A single-tape Turing machine that computes a function doesn’t work like that.