Skelet 17: Difference between revisions
(Stub) |
(add details) |
||
| Line 3: | Line 3: | ||
Skelet #17 was one of [[Skelet's 43 holdouts]] and one of the last holdouts in BB(5). | Skelet #17 was one of [[Skelet's 43 holdouts]] and one of the last holdouts in BB(5). | ||
The first step towards it's resolution was made by savask, who shown the connection to [[wikipedia:Gray_code|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf | |||
Building upon this work, chxu 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 | 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]]): | |||
<nowiki><math display="block">0^\infty \; 10^{n_1} \; 1 \; 10^{n_2} \; \dots 1 \; 10^{n_k} \textrm{ B> } \; 0^\infty</math></nowiki> | |||
< | where <nowiki><math>n_i</math></nowiki> represent a non-negative integer. Essentially, Skelet 17 operates with the <nowiki><math>1</math></nowiki>-separated lists of non-negative numbers (the <nowiki><math>k</math></nowiki> is the length of this list). | ||
</ | |||
[[Category:Stub]] | [[Category:Stub]] | ||
Revision as of 06:47, 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 it's resolution was made by savask, who shown the connection to Gray Code: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf
Building upon this work, chxu 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):
<math display="block">0^\infty \; 10^{n_1} \; 1 \; 10^{n_2} \; \dots 1 \; 10^{n_k} \textrm{ B> } \; 0^\infty</math>
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).