1RB2LA0LA_2LC---2RA_0RA2RC1LC

1RB2LA0LA_2LC---2RA_0RA2RC1LC (bbch) is a non-halting BB(3,3) TM. It is listed as "unofficial holdout ID 494" in Justin Blanchard's 3x3 "mugshots" holdout list, which can be found at File:Mugshots small.pdf.

On July 22, 2024, busycoq received a proof that this TM doesn't halt: https://github.com/meithecatte/busycoq/commit/ce2f22e1616632924622016d9cbb8ba0847b2c6a

Analysis by LegionMammal978

https://discord.com/channels/960643023006490684/1084047886494470185/1217881464297885716

C(a,b,c) = 0^∞ (12)^a 2^b C> 202 (202)^c 000
(0^∞ A> 0^∞) -> C(1,5,1) 0^∞

C(0,b,c) -> C(b+2,1,c-1)         [c ≥ 1]
C(1,b,c) -> C(b+5,1,c-1)         [c ≥ 1]
C(2,b,0) -> C(1,5,2) 0^(b-2) 202 [b ≥ 2]
C(a,b,0) -> C(1,5,a-3) 0^b 202   [a ≥ 3]
C(a,b,c) -> C(a-2,b+7,c-1)       [a ≥ 2, c ≥ 1]
C(0,b,0) 0^5 -> C(1,5,b+1)
C(1,b,0) 0^5 -> C(1,5,b+4)

It's hard to determine whether the last two cases can ever occur at all, unless there's some modular invariant I'm not seeing. Also, if they do occur, I believe it's impossible for it to eat another 0^5 before a new 0^(b+1) or 0^(b+3) is added, but I don't have a formal proof of this.

L1: A> 00 => 2 C> 2
 A> 00
 1 B> 0
 1 <C 2
 2 C> 2
L2: C> 02 => 2 C> 2
 C> 02
 0 A> 2
 0 <A 0
 2 C> 2 [L1]
L3: C> 000 => 12 A> 1
 C> 000
 0 A> 00
 02 C> 2 [L1]
 0 <C 11
 0 A> 11
 12 A> 1 [R2]
R1: (12)^s A> (02)^(t+1) => (12)^(s+1) A> (02)^t
 (12)^s A> 02 (02)^t
 (12)^s 1 B> 2 (02)^t
 (12)^s 12 A> (02)^t
R2: 0^(s+1) (12)^t A> 1^(u+1) => 0^s (12)^(t+1) A> 1^u
 0^s 0 (12)^t A> 1 1^u
 0^s 0 <A (20)^t 2 1^u
 0^s 1 (21)^t 2 A> 1^u [R1×(t+1)]
R3: 0^(s+1) (12)^(t+1) A> 00000 (202)^u => 0^s (12)^t A> 00000 (202)^(u+1)
 0^s 0 (12)^t 12 A> 00000 (202)^u
 0^s 0 (12)^t 122 C> 2000 (202)^u [L1]
 0^s 0 (12)^t 1 <C 111000 (202)^u
 0^s 0 (12)^t 2222 C> 000 (202)^u
 0^s 0 (12)^t 222212 A> 1 (202)^u [L3]
 0^s 0 <A (20)^t 0000202 (202)^u
 0^s (12)^t A> 00000202 (202)^u [R1×s]


C(a,b,c) = 0^∞ (12)^a 2^b C> 202 (202)^c 000
(0^∞ A> 0^∞) -> C(1,5,1) 0^∞

C(0,b,c) -> C(b+2,1,c-1)         [c ≥ 1]
C(1,b,c) -> C(b+5,1,c-1)         [c ≥ 1]
C(2,b,0) -> C(1,5,2) 0^(b-2) 202 [b ≥ 2]
C(a,b,0) -> C(1,5,a-3) 0^b 202   [a ≥ 3]
C(a,b,c) -> C(a-2,b+7,c-1)       [a ≥ 2, c ≥ 1]
C(0,b,0) 00000 -> C(1,5,b+1)
C(1,b,0) 00000 -> C(1,5,b+4)

D(a,c) = C(a,1,c)
D(2k+0,c)     -> D(7k+3,c-k-1)              [c ≥ k+1]
D(2k+1,c)     -> D(7k+6,c-k-1)              [c ≥ k+1]
D(2k+0,k) 0^5 -> D(10,7k+1)
D(2k+1,k) 0^5 -> D(10,7k+4)
D(2k+0,k-1)   -> D(10,1) 0^(7k-8) 202       [k ≥ 2]
D(2k+1,k-1)   -> D(10,8) 0^(7k-11) 202      [k ≥ 2]
D(2k+0,c)     -> D(10,2k-2c-4) 0^(7c+1) 202 [c ≤ k-2]
D(2k+1,c)     -> D(10,2k-2c-3) 0^(7c+1) 202 [c ≤ k-2]


C(a,b,c) = 0^∞ (12)^a 2^b C> 202 (202)^c 000 #
a = 0:
 2^b C> 202 (202)^c 000 #
 0 <C 1^b 102 (202)^c 000 #
 0 A> 1^b 102 (202)^c 000 #
 (12)^(b+1) A> 02 (202)^c 000 # [R2×(b+1)]
 (12)^(b+1) 12 A> (202)^c 000 # [L1]
 c = 0:
  (12)^(b+1) 12 A> 000 #
  # = 00000 #:
   (12)^(b+1) 12 A> 00000000 #
   A> 00000 (202)^(b+2) 000 # [R3×(b+2)]
   2 C> 2000 (202)^(b+2) 000 # [L1]
   0 <C 11000 (202)^(b+2) 000 #
   0 A> 11000 (202)^(b+2) 000 #
   1212 A> 000 (202)^(b+2) 000 # [R2×2]
   12122 C> 20 (202)^(b+2) 000 # [L1]
   121 <C 1110 (202)^(b+2) 000 #
   122222 C> 0 (202)^(b+2) 000 #
   1222222 C> (202)^(b+2) 000 # [L2] = C(1,5,b+1)
  otherwise: undefined
 c ≥ 1:
  (12)^(b+1) 12 A> 202 (202)^(c-1) 000 #
  0 <A (20)^(b+1) 20002 (202)^(c-1) 000 #
  (12)^(b+1) 12 A> 0002 (202)^(c-1) 000 # [R1×(b+2)]
  (12)^(b+1) 122 C> 202 (202)^(c-1) 000 # [L1] = C(b+2,1,c-1)
a ≥ 1:
 (12)^(a-1) 12 2^b C> 202 (202)^c 000 #
 (12)^(a-1) 1 <C 1 1^b 102 (202)^c 000 #
 (12)^(a-1) 22 2^b 2 C> 02 (202)^c 000 #
 (12)^(a-1) 22 2^b 22 C> 2 (202)^c 000 # [L2]
 a = 1:
  22 2^b 22 C> 2 (202)^c 000 #
  0 <C 11 1^b 111 (202)^c 000 #
  0 A> 11 1^b 111 (202)^c 000 #
  (12)^(b+5) A> (202)^c 000 # [R2×(b+5)]
  c = 0:
   (12)^(b+5) A> 000 #
   # = 00000 #:
    (12)^(b+5) A> 00000000 #
    A> 00000 (202)^(b+5) 000 # [R3×(b+5)]
    2 C> 2000 (202)^(b+5) 000 # [L1]
    0 <C 11000 (202)^(b+5) 000 #
    0 A> 11000 (202)^(b+5) 000 #
    1212 A> 000 (202)^(b+5) 000 # [R2×2]
    12122 C> 20 (202)^(b+5) 000 # [L1]
    121 <C 1110 (202)^(b+5) 000 #
    122222 C> 0 (202)^(b+5) 000 #
    1222222 C> (202)^(b+5) 000 # [L2] = C(1,5,b+4)
   otherwise: undefined
  c ≥ 1:
   (12)^(b+5) A> 202 (202)^(c-1) 000 # = A(b+5,c-1)
   0 <A (20)^(b+5) 002 (202)^(c-1) 000 #
   (12)^(b+5) A> 0002 (202)^(c-1) 000 # [R1×(b+5)]
   (12)^(b+5) 2 C> 202 (202)^(c-1) 000 # [L1] = C(b+5,1,c-1)
 a ≥ 2:
  (12)^(a-2) 1222 2^b 22 C> 2 (202)^c 000 #
  (12)^(a-2) 1 <C 111 1^b 111 (202)^c 000 #
  (12)^(a-2) 2222 2^b 222 C> (202)^c 000 #
  c = 0:
   (12)^(a-2) 2222 2^b 222 C> 000 #
   (12)^(a-2) 2222 2^b 22212 A> 1 # [L3]
   0 <A (20)^(a-2) 0000 0^b 000202 #
   (12)^(a-2) A> 00000 0^b 000202 # [R1×(a-2)]
   A> 00000 (202)^(a-2) 0^b 000202 # [R3×(a-2)]
   2 C> 2000 (202)^(a-2) 0^b 000202 # [L1]
   0 <C 11000 (202)^(a-2) 0^b 000202 #
   0 A> 11000 (202)^(a-2) 0^b 000202 #
   1212 A> 000 (202)^(a-2) 0^b 000202 # [R2×2]
   12122 C> 20 (202)^(a-2) 0^b 000202 # [L1]
   121 <C 1110 (202)^(a-2) 0^b 000202 #
   122222 C> 0 (202)^(a-2) 0^b 000202 #
   a = 2:
    122222 C> 0 0^b 000202 #
    12222212 A> 1 0^b 0202 # [L3]
    0 <A 200000202 0^b 0202 #
    12 A> 00000202 0^b 0202 # [R1]
    A> 00000202202 0^b 0202 # [R3]
    2 C> 2000202202 0^b 0202 # [L1]
    0 <C 11000202202 0^b 0202 #
    0 A> 11000202202 0^b 0202 #
    1212 A> 000202202 0^b 0202 # [R2×2]
    12122 C> 20202202 0^b 0202 # [L1]
    121 <C 1110202202 0^b 0202 #
    122222 C> 0202202 0^b 0202 #
    1222222 C> 202202 0^b 0202 # [L2] = C(1,5,2) 0^(b-2) 202
   a ≥ 3:
    122222 C> 0202 (202)^(a-3) 0^b 000202 #
    1222222 C> 202 (202)^(a-3) 0^b 000202 # [L2] = C(1,5,a-3) 0^b 202
  c ≥ 1:
   (12)^(a-2) 2222 2^b 222 C> 202 (202)^(c-1) 000 # = C(a-2,b+7,c-1)