1RB0RC_1RC0LC_0RD1LE_1LE1RF_0LB---_0RA1LA

1RB0RC_1RC0LC_0RD1LE_1LE1RF_0LB---_0RA1LA (bbch) is a holdout BB(6) TM proven infinite by hand 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) >= 0` should always hold. But this is not detectible nor provable by any existing deciders.