1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE
This is a potential 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).
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