1RB0LF_1RC1RA_1LD0RE_1LB1LD_---1RC_1RC1LA

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 $b\to 2b+5$ repeatedly until $b\ge a-4$. This sequences is $b_k=2^{k+3}-5$. Let $c_k=\sum _{i=0}^{k-1}(b_k+4)=2^{k+3}-8-k$. Then if $c_k<a<=c_{k+1}$ the next reset will be: $(a-c_k,b_k,0)$. The question is whether we can ever reach $a-c_k=1$. If $a-c_k>1$ then $(a-c_k,b_k,0)\to (3b_k+c_k-a+9,3,0)$. Let $f(a)=3b_k+c_k-a+9$ be that next value of a.

$f(a)=3b_k+c_k-a+9<3b_k+9=32^{k+3}-6<c_{k+2}$ for all $k\ge 0$

$f(a)=3b_k+c_k-a+9>=3b_k+c_k-c_{k+1}=(3+1-2)2^{k+3}+(-15-8-k+8+k+1)=2^{k+4}-14>c_{k+1}+1$ for all $k>7$

So, if $k\ge 8$ and $c_k+1<a<=c_{k+1}$ then $c_{k+1}+1<f(a)\le c_{k+2}$ and this will continue to rule will apply repeatedly forever. Finally, starting from the blank tape, the trajectory gets to $(0,0,0)\to (2719,3,0)$ where $c_8+1<2719<=c_9$. 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)