Skelet 10

1LC0LA_---0LC_0RD1LA_1LB1RE_1RD0RE (bbch), called Skelet #10, was one of Skelet's 43 holdouts and one of the last holdouts in BB(5). It is a double fibonacci counter. It is one of the few TMs to have required an individual proof of non-halting in Coq-BB5.

Behavior

Skelet 10 implements two base fibonacci counters, one on the right tape side and one on the left tape side. The TM halts if these counters become desynchronised. The right side counter can be described by the following rules:

A>  0 10^k 0 --> <D 0^2k   10
B> 10 10^k 0 --> <D 0^2k+1 10

These rules are equivalent to the Zeckendorf increment rules:

Z(n) = 0  10^k 0 w ==> Z(n+1) = 0^2k   10 w
Z(n) = 10 10^k 0 w =0> Z(n+1) = 0^2k+1 10 w
Where Z(n) represents n in the little-endian (least significant digit is on the left) representation of Zeckendorf notation.

and can be restated as:

Z(n) = 0 w ==> A> Z(n) --> <D Z(n+1)
Z(n) = 1 w ==> B> Z(n) --> <D Z(n+1)
Where Z(n) = 0 w means that the least-significant bit in Z(n) is 0.

The left side counter encodes base fibonacci differently and is also reversed, with the least-significant digit being on the right. The two least-significant symbols are also omitted. These differences can be described using the following definitions:

T(0w)    = T(w)00
T(10w)   = T(w)1010
T(empty) = empty
where w is any valid Zeckendorf expression.
--> This encodes the Zeckendorf representations in a way consistent with the left fibonacci counter by encoding 10 as 1010 and 0 as 00. This also reverses the order of the Zeckendorf representation to big-endian.

L(n) is defined in the following way:
T(Z(n)) = v ab ==> L(n) = v
where v is any valid Zeckendorf expression.
--> This removes the two least-significant tape symbols.

The TM follows these rules on the left:

        00 <D -->         10 B>
00 10^k 00 <D --> 10 10 00^k A>

See also

• Skelet 1
• Skelet 17
• Finned 3