1RB0LD 1LC0RA 1RA1LB 1LA1LE 1RF0LC ---0RE

This is a potential Cryptid found by @mxdys and shared on Discord on 7 Aug 2024.

Analysis by @mxdys

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)-->
...

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

These rules have been proved in Coq.

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:

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

Since b can equal -1, I want to shift the second term up by 1:

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

I also want to redefine a(i) to mean 10*2^i-1, so we get

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