View source for 1RB0RC 1RC0LC 0RD1LE 1LE1RF 0LB--- 0RA1LA

{{machine|1RB0RC_1RC0LC_0RD1LE_1LE1RF_0LB---_0RA1LA}}
{{TM|1RB0RC_1RC0LC_0RD1LE_1LE1RF_0LB---_0RA1LA}} is a non-halting [[BB(6)]] TM proven infinite in Rocq ([https://github.com/ccz181078/busycoq/blob/0a61549704e6305f752a4ad1f0faa5cf41dc0e61/verify/SBCv3.v#L8-L201 link]) by @mxdys on 6 Dec 2024.

Analysis by @mxdys:
<pre>
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
</pre>

Follow up by [[User:sligocki]]:
<pre>
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
</pre>
Which indicates that the condition <math>f(2^k, ls)-(n+2) \ge 0</math> should always hold. But this is not detectible nor provable by any existing deciders.

[[Category:BB(6)]]