I believe I have proofs for 4 more holdouts (identified and proved non-halting with AI-assistance): one transition table started in A, B, C and D. One proof idea, four .v files, Skelet 1-like Class 2 again! :skull_crossbones:

`1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---` (start A): <FILE_LINK_1RB0LE_1RC0RC>
`1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` (start B): <FILE_LINK_1RB0RB_1LC0RA>
`1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---` (start C, mirrored): <FILE_LINK_1RB0LD_1RC0RE>
`1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---` (start D, mirrored): <FILE_LINK_1RB0RE_1LC0RE>
PR: <PR_LINK>
Informal write-ups: attached

The tape is a binary counter on (10)^u (01)^v digits, with 00 between the halves for a 0. A carry costs every digit it touches one 01, and a digit that runs out merges into the next. On overflow every digit swaps its halves and a digit is added.

The A file composes window lemmas into these rules and carries a per-step invariant (parities and lower bounds; architecture of SBCv6 TM21). B is that file with renamed states and its own start. D mirrors it by hand, keeping the invariant part verbatim, and C is the D file renamed.

Thanks to hipparcos for his analysis of `1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` in his thread; §7 of its write-up answers his `C C0` right-end question.

All four compile against unmodified busycoq, Print Assumptions is closed, and coqchk passes.

AI disclosure: as before, produced with Claude Code (Opus 5.5). The results rest on the Coq files; extra verification and feedback are very welcome!