Change `loop` so that it can re-use existing tapes

[crei]

The main problem with this is that in order to state an eval_list theorem about loop, we need to make sure that the inner TM does not depend on or modifies the aux tapes.