Approach: #3's proof, from a different start

3 counts a binary number down on a list of pairs of blocks, like an odometer running backward, and its proof is a checklist of inequalities showing that a block only ever runs out where that is harmless. This machine is #3's table with two pairs of state letters swapped, so it is #3 started in state C instead of A. Watching it, you see #3's countdown with one block at the far end of the list a little longer.

What is new is the opening: after 79,114 steps the run reaches the checkpoint #3's argument starts from (#3 gets there after 78,710 steps), except that the last pair has 26 copies of 01 instead of 24, which the checklist allows. From there #3's argument (the nine moves and the checklist, none of which depends on the start) applies unchanged, so it never halts. Side by side, the two runs then make the same move every time, this one with its far block 2 copies longer and a growing number of steps behind. That explains why nothing else changes, but the proof does not rely on it.

The Rocq file is #3's with the state names swapped and a new opening. It replays the 79,114 steps, checks the checklist there, and proves the result for this table directly.