Approach: W5-8's proof, from a different start

W5-8's tape is mostly five long blocks of 1s with short words between them; their lengths follow exact rules through 12-trip stretches and collisions of the short words, into a double cycle that repeats forever. W5-8c is W5-8's table with its state letters renamed (no mirror), started in the state that is W5-8's E instead of A. So it shows W5-8's picture the right way round: the same 43-cell pattern at the left end, the same blocks, short words and collisions.

New state names change nothing about what the machine does, so every rule of W5-8 holds here unchanged. What is new is the opening. After 6,950,830 steps the run falls into the five-block pattern with lengths 2,583, 70, 76, 43 and 18. From there its collisions come in an order of their own: nine collisions, with 12-trip stretches between them, each inside the range where its rule is proved.

They reach a start of W5-8's double cycle at step 163,638,058, with a second block of 220 cells where W5-8's run has 212. The cycle's conditions (an odd first block, and a second block of at least 52 that leaves remainder 4 when divided by 8, with the other three blocks set by it) hold there. So the cycle repeats forever, the second block growing 220, 252, 284 and so on, and the missing transition is never used.

The Rocq proof keeps W5-8's rules and double cycle word for word, for W5-8's table. It replays that table's 6,950,830-step opening from state E in ten pieces, chains the nine collisions, and uses busycoq's renaming lemma to turn a halt of W5-8c into a halt of that run.