Skelet 17

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

	5	4	3	2	1	0	value	length	$\sigma$
0	-	-	-	0	0	1	0	3	+1
1	-	-	-	0	1	0	1	3	+1
1*	-	-	-	1	1	-1	2	3	+1
2	-	-	-	-	1	1	1	2	-1
3	-	-	-	-	2	0	0	2	-1
3*	-	-	-	-	2	0	0	2	-1
4	-	-	-	0	0	3	0	3	+1
5	-	-	-	0	1	2	1	3	+1
6	-	-	-	1	1	1	2	3	+1
7	-	-	-	1	2	0	3	3	+1
7*	-	-	0	2	2	0	0	4	-1
7**	0	0	1	2	2	-1	7	6	-1
8	-	0	0	1	2	2	3	5	+1
9	-	0	1	1	2	1	4	5	+1
10	-	0	1	1	3	0	5	5	+1
10*	-	0	1	2	3	-1	6	5	+1
11	-	-	0	1	2	3	3	4	-1
12	-	-	0	1	3	2	2	4	-1
13	-	-	0	2	3	1	1	4	-1
14	-	-	0	2	4	0	0	4	-1
14*	-	0	1	2	4	0	7	5	+1
14**	0	0	1	2	4	-1	7	6	-1
15	-	0	0	1	2	4	3	5	+1
16	-	0	1	1	2	3	4	5	+1
17	-	0	1	1	3	2	5	5	+1
18	-	0	1	2	3	1	6	5	+1
19	-	0	1	2	4	0	7	5	+1
19*	-	1	1	2	4	-1	8	5	+1
20	-	-	1	1	2	4	4	4	-1
21	-	-	2	1	2	3	3	4	-1
22	-	-	2	1	3	2	2	4	-1
23	-	-	2	2	3	1	1	4	-1
24	-	-	2	2	4	0	0	4	-1

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):

$0^{\infty }\;10^{n_{1}}\;1\;10^{n_{2}}\;\dots 1\;10^{n_{k}}{\textrm {B>}}\;0^{\infty }$,

where $n_{i}$ represents a non-negative integer. Essentially, Skelet 17 builds $k$-length lists of non-negative numbers with individual cells imprinted with a 1 acting as the delimiter.