Skelet 17: Difference between revisions
m (fixed math formatting) |
(cleaned up Behavior description) |
||
| Line 13: | Line 13: | ||
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]]): | 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]]): | ||
<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 <math>n_i</math> | where <math>n_i</math> represents a non-negative integer. Essentially, Skelet 17 builds <math>k</math>-length lists of non-negative numbers with individual cells imprinted with a 1 acting as the delimiter. | ||
[[Category:Stub]] | [[Category:Stub]] | ||
Revision as of 07:26, 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 represents a non-negative integer. Essentially, Skelet 17 builds -length lists of non-negative numbers with individual cells imprinted with a 1 acting as the delimiter.
