These are two separate things. The `loop` construction / function or whatever it is called in the sCrypt language is a compile-time loop. That is, the body gets unrolled N times (8 in this example). It's just an implementation detail for the lookup in the transition table. However, that is not part of a proof. The author is pretty clear that each transition in the TM is implemented as a bitcoin transaction.