1RB0RC 1RC0LC 0RD1LE 1LE1RF 0LB--- 0RA1LA

1RB0RC_1RC0LC_0RD1LE_1LE1RF_0LB---_0RA1LA (bbch) is a non-halting BB(6) TM proven infinite in Rocq (link) by @mxdys on 6 Dec 2024.

Analysis by @mxdys:

f(n0, ()) := n0
f(n0, (n,ls)) := 2*(f(n0, ls) - n)

start: (2, (), 1)
(k, ls, n) --> (k+1, (n,ls), 2*(f(2^k, ls)-(n+2))),  f(2^k, ls)-(n+2) >= 0

Follow up by User:sligocki:

Let (k, ls, n) --> (k+1, [n, ls], n')

Then:
  n'+2 = 2 (f(2^k, ls) - n) - 2
  f(2^{k+1}, [n, ls]) = 2 (f(2^{k+1}, ls) - n)

So:
  f(2^{k+1}, [n, ls]) - (n'+2) = 2 (f(2^{k+1}, ls) - f(2^k, ls)) + 2

Which indicates that the condition $f(2^k,ls)-(n+2)\ge 0$ should always hold. But this is not detectible nor provable by any existing deciders.