Skelet 17

1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA (bbch), called 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 non-halting that can be found here: https://chrisxudoesmath.com/papers/skelet17.pdf

Adapting the above, a formal proof of its non-halting by mxdys can be found here: https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/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 delimited with individual cells imprinted with a 1.

The most common transformation (frequency tends to 1 as the number of steps increases) occuring between such configurations is described by Increment rule, similar to the Lucal form of Gray Code: the value at the last index is decremented and the value to the left of the rightmost index with odd value is incremented.

It is useful to consider the following state variables:

• Gray Code value (denoted by $n$): the integer that is obtained by calculating the parity of each number (except the last) in the list, considering the result as a Gray Code bitstring corresponding to some integer and "recovering" this integer.
• Increment value (denoted by $\sigma$): the parity of the entire sequence, mapped to $\{-1,1\}$. Dirung Increment steps, Skelet 17 counts forwards when $\sigma =+1$ or backwards if $\sigma =-1$.
• Length of the sequence (including leading zeros).

When started on a blank tape, the machine visits configurations of the form $(0,2,4,...,2^{2k+2},0)$ infinitely often (the step numbers where it occurs approximately equal power of 16: 14, 251, 4088, 65537, 1048646, 16777607, 268437188, etc).

Analysis by bisimulation

Chris Xu found it useful to divide some tape transformations into two phases, one of them is "virtual" or "invisible", as it does not actually occur on the tape. Indeed, the intermediate step involves negative numbers (the last number being decremented to -1 from 0), which of course cannot correspond to the $10^{a_{i}}$ written on the tape.

Such skipped intermediate steps are denoted by asterisks in the table to preserve the "real" step counts (e.g. steps 7* and 7**).