View source for 1RB0LD 1RC1RA 1LD0RB 1LE1LA 1RF0RC ---1RE

{{machine|1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE}}{{unsolved|Does this TM halt? If so, how many steps does it take to halt?}}
{{TM|1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE}} is a [[probviously]] halting [[BB(6)]] [[Cryptid]] analyzed by mxdys on 30 July 2025. This TM is probviously halting because it decrements a 3-tuple <code>(a,b,c)</code> into either <code>(0,0,c)</code> or <code>(0,1,c)</code> with equal probability. If it lands on <code>(0,0,c)</code>, the TM halts. It takes roughly 2a rule (not TM) steps to reach an a=0 state. On the first 3 occasions, the TM lands on <code>(0,1,c)</code>:

# <code>(0,1,8) --> (25,0,0)</code>
# <code>(0,1,113544) --> (227097,0,0)</code>
# <code>(0,1,28155...08204) --> (56311...16417,0,0)</code>, where 28155...08204 and 56311...16417 are 39991-digit numbers.

As a is now so large, the next 3-tuple is <math>(0, ?, \approx 10^{10^{39990}})</math>, and forward simulation of the current rules is no longer a viable option to understand if the TM halts.

== Analysis by mxdys ==
[https://discord.com/channels/960643023006490684/1239205785913790465/1400141896944320602]

<pre>
1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE

(a,b,c) := 0^inf 1^a 0 01^b 0 11^c+1 B> 0^inf

(a,2+b,c) --> (a,b,3+c)
(a+1,0,c) --> (a,c,2)
(a+1,1,c) --> (a,c,6)
(0,0,c) --> halt
(0,1,c) --> (2c+9,0,0)
start: (3,0,0)
</pre>

Confirmation that it doesn't halt early:
<pre>
(3,0,0) --> ...
(25,0,0) --> ...
(227097,0,0) --> ...
(_,0,0) --> ...
</pre>

These rules have been proven in Rocq and [https://github.com/int-y1/proofs/blob/10a7f272a5570d3c8d5dc506881df8b7c934c0c5/BusyLean/Individual/1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE.lean Lean]. The first rule can be accelerated as<pre>
(a,2b,c) --> (a,0,c+3b)
(a,2b+1,c) --> (a,1,c+3b)
</pre>

[[Category:BB(6)]][[Category:Cryptids]]