1RB0LF_1RC1RA_1LD0RE_1LB1LD_---1RC_1RC1LA
(bbch) is a non-halting BB(6) TM.
Analysis by Shawn Ligocki
A(a, b, c) = 0^inf 10^a <A 10^b 11^c 0^inf
A(a+1, b, c+1) -> A(a, b+2, c)
A(0, b, c+1) -> A(0, b+3, c)
A(0, b, 0) -> A(b+1, 1, 1)
A(a+2, b, 0) -> A(a, 1, b+2)
A(1, b, 0) -> Halt(b+3)
Start: A(0, 0, 0)
Analysis by @rae
(a,b,0) -> (3b-a+9,3,0) if 2<=a<=b+4
(a,b,0) -> (a-b-4,2b+5,0) if a>b+4
(1,b,0) -> halt
If we call the first rule the "reset" rule, then: Starting from a reset rule, b will follow the same trajectory each time, starting from 3 and increasing by
repeatedly until
. This sequences is
. Let
. Then if
the next reset will be:
. The question is whether we can ever reach
. If
then
. Let
be that next value of a.
for all
for all
So, if
and
then
and this will continue to rule will apply repeatedly forever. Finally, starting from the blank tape, the trajectory gets to
where
. QED.
Analysis by mxdys
On Jul 29 2025, mxdys gave a Rocq proof that this TM is non-halting: https://github.com/ccz181078/busycoq/blob/256b1916a325cef4d9f904bc61398e1d97b02c9e/verify/Loop4v4.v#L11-L131 (note: in this proof, the TM machine code is L/R flipped)