1RB0LD 1RC1RA 1LD0RB 1LE1LA 1RF0RC ---1RE: Difference between revisions
Jump to navigation
Jump to search
(simulation results) |
(proven in coq and lean) |
||
| Line 24: | Line 24: | ||
(227097,0,0) --> ... | (227097,0,0) --> ... | ||
(_,0,0) --> ... | (_,0,0) --> ... | ||
</pre>The first rule can be accelerated as<pre> | </pre> | ||
These rules have been proven in Coq and [https://github.com/int-y1/proofs/blob/10a7f272a5570d3c8d5dc506881df8b7c934c0c5/BusyLean/Individual/1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE.lean Lean]. | |||
The first rule can be accelerated as | |||
<pre> | |||
(a,2b,c) --> (a,0,c+3b) | (a,2b,c) --> (a,0,c+3b) | ||
(a,2b+1,c) --> (a,1,3(b-1)/2) | (a,2b+1,c) --> (a,1,3(b-1)/2) | ||
</pre>Andrew Ducharme forward simulated the map with this acceleration 10^7 steps and found the TM had not yet halted. | </pre> | ||
Andrew Ducharme forward simulated the map with this acceleration 10^7 steps and found the TM had not yet halted. | |||
Revision as of 08:14, 6 August 2025
Unsolved problem:
Does this TM halt? If so, how many steps does it take to halt?
1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE (bbch) is a probviously halting BB(6) Cryptid analzyed by mxdys on 30 July 2025.
Analysis by mxdys
1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE (a,b,c) := 0^inf 1^a 0 01^b 0 11^c+1 B> 0^inf (a,2+b,c) --> (a,b,3+c) (a+1,0,c) --> (a,c,2) (a+1,1,c) --> (a,c,6) (0,0,c) --> halt (0,1,c) --> (2c+9,0,0) start: (3,0,0)
Confirmation that it doesn't halt early:
(3,0,0) --> ... (25,0,0) --> ... (227097,0,0) --> ... (_,0,0) --> ...
These rules have been proven in Coq and Lean.
The first rule can be accelerated as
(a,2b,c) --> (a,0,c+3b) (a,2b+1,c) --> (a,1,3(b-1)/2)
Andrew Ducharme forward simulated the map with this acceleration 10^7 steps and found the TM had not yet halted.