Skelet 17: Difference between revisions
Jump to navigation
Jump to search
m (→TM Behavior: changed a word) |
m (added links to proofs) |
||
| Line 1: | Line 1: | ||
{{machine|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}} | {{machine|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}} | ||
https://bbchallenge.org/1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA | https://bbchallenge.org/1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA | ||
Skelet #17 was one of the last holdouts in BB(5). | |||
A full proof of its nonhalting can be found here: https://chrisxudoesmath.com/papers/skelet17.pdf | |||
A formal proof by mxdys can be found here: https://github.com/ccz181078/Coq-BB5/blob/main/Skelet17.md | |||
== TM Behavior == | == TM Behavior == | ||
S can be simulated with the following rules: | |||
<pre> | <pre> | ||
A(a0, a1, ..., an)=1 (10)^a0 1 (10)^a1 ... 1 (10)^an | A(a0, a1, ..., an)=1 (10)^a0 1 (10)^a1 ... 1 (10)^an | ||
</pre> | </pre> | ||
Revision as of 15:14, 2 July 2024
https://bbchallenge.org/1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA
Skelet #17 was one of the last holdouts in BB(5).
A full proof of its nonhalting can be found here: https://chrisxudoesmath.com/papers/skelet17.pdf
A formal proof by mxdys can be found here: https://github.com/ccz181078/Coq-BB5/blob/main/Skelet17.md
TM Behavior
S can be simulated with the following rules:
A(a0, a1, ..., an)=1 (10)^a0 1 (10)^a1 ... 1 (10)^an