1RB2LA0LA 2LC---2RA 0RA2RC1LC: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
Polygon (talk | contribs)
Analysis by LegionMammal978: there's a fixed version (the old one had errors)
Polygon (talk | contribs)
Analysis by LegionMammal978: Added D-rules, splitted into two blocks
Line 20: Line 20:
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.
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.


D(a,c) = C(a,1,c)
(0^∞ A> 0^∞) -> D(10,0) 0^∞
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]
</pre>
<pre>
L1: A> 00 => 2 C> 2
L1: A> 00 => 2 C> 2
  A> 00
  A> 00

Revision as of 19:50, 30 March 2026

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.

D(a,c) = C(a,1,c)
(0^∞ A> 0^∞) -> D(10,0) 0^∞

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