View source for 1RB0LD 1LC0RA 1RA1LB 1LA1LE 1RF0LC ---0RE

{{machine|1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE}}
{{TM|1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE}} is a potential [[BB(6)]] [[Cryptid]] found by @mxdys and shared on Discord on 7 Aug 2024. Andrew Ducharme forward simulated its representative map 33,342,087,612,867 steps, at which point both entries in the tuples (x,y) were on the order 10^(2.00705*10^6). The TM had not yet halted.

When the TM starts on these states, it exhibits similar behaviour:

* When the starting state is A, the [[Tree Normal Form|TNF]] is {{TM|1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE}}.
* When the starting state is C, the TNF is {{TM|1RB1LC_1RC0LD_1LA0RB_1LB1LE_1RF0LA_---0RE}}.
* When the starting state is D, the TNF is {{TM|1RB1RE_1LC0RA_1RD0LB_1LB1RC_1LF0RD_---0LE}}.

== Analysis by @mxdys ==
<pre>
1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE

start from (2,3)
(a,b+a+2) --> (2a+3,b)
(a+b+1,b) --> (2,a+4b+5)
(a,a) --> halt          not used?
(a,a+1) --> (2,2a+4)    only used once?

(a,b) := 0^inf 01^a 110 A> 1^(2b+1) 0^inf

example:
(2,3)-->
(2,8)-->(7,4)-->
(2,23)-->(7,19)-->(17,10)-->
(2,51)-->(7,47)-->(17,38)-->(37,19)-->
(2,98)-->(7,94)-->(17,85)-->(37,66)-->(77,27)-->
(2,162)-->(7,158)-->(17,149)-->(37,130)-->(77,91)-->(157,12)-->
(2,197)-->(7,193)-->(17,184)-->(37,165)-->(77,126)-->(157,47)-->
(2,302)-->(7,298)-->(17,289)-->(37,270)-->(77,231)-->(157,152)-->
(2,617)-->(7,613)-->(17,604)-->(37,585)-->(77,546)-->(157,467)-->(317,308)-->
...
</pre>

<pre>
start from <0,4>
b >= a(i)+2: <i,b> --> <i+1,b-a(i)-2>
b <= a(i)-1: <i,b> --> <i,3b+i+7>
b =  a(i)+0: <i,b> --> halt          unused?
b =  a(i)+1: <i,b> --> <i+1,i+5>     unused?

<i,b> = (a(i),b)
a(i) = 10*2^i-3
</pre>
These rules have been proved in [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v Rocq].

== Analysis by @dyuan01 ==
If you apply the b=a(i)+1 rule into the b >= a(i)+2 rule, you get (i+1, -1). Applying b <= a(i)-1 gives us (i+1, i+5), which is the result you have shown.

So we can just remove the last rule and add its condition to the condition of the first rule:
<pre>
start from <0,4>
b >= a(i)+1: <i,b> --> <i+1,b-a(i)-2>
b <= a(i)-1: <i,b> --> <i,3b+i+7>
b =  a(i)+0: <i,b> --> halt          unused?

<i,b> = (a(i),b)
a(i) = 10*2^i-3
</pre>
Since b can equal -1, I want to shift the second term up by 1:
<pre>
start from <0,5>
b >= a(i)+2: <i,b> --> <i+1,b-a(i)-2>
b <= a(i)+0: <i,b> --> <i,3b+i+5>
b =  a(i)+1: <i,b> --> halt          unused?

<i,b> = (a(i),b+1)
a(i) = 10*2^i-3
</pre>
 
I also want to redefine a(i) to mean 10*2^i-1, so we get
<pre>
start from <0,5>
b >= a(i)+0: <i,b> --> <i+1,b-a(i)>
b <= a(i)-2: <i,b> --> <i,3b+i+5>
b =  a(i)-1: <i,b> --> halt          unused?

<i,b> = (a(i)-2,b+1)
a(i) = 10*2^i-1
</pre>

[[Category:BB(6)]]