Approach: W5-8's proof in a mirror, 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-8b is W5-8's table seen in a mirror, with its state letters renamed, started in the state that is W5-8's C instead of A. So it shows W5-8's picture in a mirror: the fixed 43-cell pattern sits at the right end and every trip starts there.

A mirror and new state names change nothing about what the machine does, so every rule of W5-8 holds here unchanged, read right to left. What is new is the opening. After 4,098,826 steps the run falls into W5-8's five-block pattern with the lengths W5-8 has when it first gets there, except that the block next to the fixed pattern is 6 cells shorter (1,953 instead of 1,959).

That difference never matters: no rule's result for the other four blocks depends on that block, and the rules only add fixed even amounts to it, which keeps it odd as they require. So the same ten collisions, with the same 12-trip stretches between them, follow in the same order and reach a start of W5-8's double cycle at step 153,013,640, still 6 cells shorter there. From then on W5-8's argument applies unchanged, 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 4,098,826-step opening from state C, chains the same collisions, and uses busycoq's mirror and renaming lemmas to turn a halt of W5-8b into a halt of that run.