Skelet 17: Difference between revisions
m (typos and math formatting) |
m (fixed math formatting) |
||
| Line 15: | Line 15: | ||
<math>0^\infty \; 10^{n_1} \; 1 \; 10^{n_2} \; \dots 1 \; 10^{n_k} \textrm{ B> } \; 0^\infty</math> | <math>0^\infty \; 10^{n_1} \; 1 \; 10^{n_2} \; \dots 1 \; 10^{n_k} \textrm{ B> } \; 0^\infty</math> | ||
where | where <math>n_i</math> represent a non-negative integer. Essentially, Skelet 17 operates with the <math>1</math>-separated lists of non-negative numbers (the <math>k</math> is the length of this list). | ||
[[Category:Stub]] | [[Category:Stub]] | ||
Revision as of 07:17, 24 July 2024
1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA (bbch)
Skelet #17 was one of Skelet's 43 holdouts and one of the last holdouts in BB(5).
The first step towards its resolution was made by savask, who showed the connection to Gray Code: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf
Building upon this work, Chris Xu produced a full proof of its nonhalting that can be found here: https://chrisxudoesmath.com/papers/skelet17.pdf
Adapting the above, a formal proof of its nonhalting by mxdys can be found here: https://github.com/ccz181078/Coq-BB5/blob/main/Skelet17.md
TM Behavior
It can be shown that when the machine head is at the right end of the tape, the complete tape configuration is of the following form (using Directed head notation):
where represent a non-negative integer. Essentially, Skelet 17 operates with the -separated lists of non-negative numbers (the is the length of this list).
