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

From BusyBeaverWiki
Jump to navigation Jump to search
VisualWikitext
Created page with "{{machine|1RB2LA0LA_2LC---2RA_0RA2RC1LC}} {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC}} <code>@-d</code> — 13 Jun 2024 at 1:28 AM ET Proved this TM infinite in Coq: https://discord.com/channels/960643023006490684/1259770474897080380/1261554831055786045"
 
Polygon (talk | contribs)
1,839 edits
Added equivalence to holdout #400
 
(14 intermediate revisions by 5 users not shown)
Line 1: Line 1:
{{machine|1RB2LA0LA_2LC---2RA_0RA2RC1LC}}
{{machine|1RB2LA0LA_2LC---2RA_0RA2RC1LC}}
{{TM|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]]. 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>


<code>@-d</code> — 13 Jun 2024 at 1:28 AM ET
On July 22, 2024, busycoq received a proof that this TM doesn't halt: https://github.com/meithecatte/busycoq/commit/ce2f22e1616632924622016d9cbb8ba0847b2c6a


Proved this TM infinite in Coq: https://discord.com/channels/960643023006490684/1259770474897080380/1261554831055786045
== Analysis by LegionMammal978 ==
https://discord.com/channels/960643023006490684/1084047886494470185/1217881464297885716
<pre>
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]
</pre>
<pre>
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)
</pre>
 
== References ==
 
[[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

  1. ↑ https://discord.com/channels/960643023006490684/1084047886494470185/1215532512307052634
Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=1RB2LA0LA_2LC---2RA_0RA2RC1LC&oldid=6847"