I disagree with your stated claim on (6) which is that there is no accepting state for (M) after an arbitrary move in (5). E.g. In bitcoin script any encounter

I disagree with your stated claim on (6) which is that there is no accepting state for (M) after an arbitrary move in (5). E.g. In bitcoin script any encounter with OP_RETURN moves you immediately into an accepting state whereupon the program halts and interpreter performs a predicate evaluation on the state of the stack. Hopcroft et. al. also makes no claim on the input to the FSM being infinite (requiring an infinite loop). Quite the opposite. The FSM clearly reads the Program until it encounters a "simulated blank" signifying the end of input, so it can start processing the "tape". A simpler way of satisfying the requirement of Bitcoin Script Interpreter as a 2-PDA is simply to define the State Transition function in terms of Bitcoin Script Primitives. Q × ( ∑ ∪ {ε} ) × S × Q × S* Where: * Q is the finite number of states * ∑ is input alphabet * S is stack symbols * q0 is the initial state (q0 ∈ Q) * I is the initial stack top symbol (I ∈ S) * F is a set of accepting states (F ∈ Q) Resolving each of the above is left as an exercise to the reader. I do concede that the actual usefulness of the computation is limited to the extent that the Bitcoin Implementation limits the size of the "input tape" i.e. the limits on size of Script. Hence the need for Big Blocks and unbounded Script sizes to allow the market to discover the correct trade-offs between economic benefit and computational cost.