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)
Added equivalence to holdout #400
 
(2 intermediate revisions by the same user not shown)
Line 1: Line 1:
{{machine|1RB2LA0LA_2LC---2RA_0RA2RC1LC}}{{Stub}}
{{machine|1RB2LA0LA_2LC---2RA_0RA2RC1LC}}
{{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC}} 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]].
{{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC}} 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]]. It is equivalent to "unofficial holdout ID 400" ({{TM|1RB1LC---_0LC2RB1LB_2LA0RC1RC}}) on that same list.<ref>https://discord.com/channels/960643023006490684/1084047886494470185/1215532512307052634</ref>


On July 22, 2024, busycoq received a proof that this TM doesn't halt: https://github.com/meithecatte/busycoq/commit/ce2f22e1616632924622016d9cbb8ba0847b2c6a
On July 22, 2024, busycoq received a proof that this TM doesn't halt: https://github.com/meithecatte/busycoq/commit/ce2f22e1616632924622016d9cbb8ba0847b2c6a
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
Line 169: Line 182:
   (12)^(a-2) 2222 2^b 222 C> 202 (202)^(c-1) 000 # = C(a-2,b+7,c-1)
   (12)^(a-2) 2222 2^b 222 C> 202 (202)^(c-1) 000 # = C(a-2,b+7,c-1)
</pre>
</pre>
== References ==
[[Category:BB(3,3)]]
[[Category:BB(3,3)]]

Latest revision as of 20:13, 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. It is equivalent to "unofficial holdout ID 400" (1RB1LC---_0LC2RB1LB_2LA0RC1RC (bbch)) on that same list.[1]

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)

References