Skelet 33

1LC1RD_1RE---_0LD0LC_1RB0RA_1RA1LE (bbch), called Skelet #33, was one of Skelet's 43 holdouts and one of the last holdouts in BB(5). It is a Shift overflow counter and has an individual proof of non-halting in Coq-BB5. It is adjacent to Skelet 34.

Skelet 33 was formally proven to be non-halting in December 2023 by int-y1 and meithecatte.

Analysis by Shawn Ligocki

b(n) is the number we have to add to n to reach the “next” power of 2 (strictly greater than n) or the smallest number which when added to n “expands” the binary representation to a larger length. 

L(2k)   = L(k) 0000
L(2k+1) = L(k) 0001

G(n, m) = L(n)     <A 010 R(m)
D(n, m) = L(n) 000 <A 010 R(m)

G(n, m) -> G(n+1, m+1)  (if b(m) > 1)
  L(n) <A -> L(n+1) B>
    0001 <A -> <A 1111
    0000 <A -> 0001 B>
  E> R(n) -> <C R(n+1)
    E> 11 -> 11 E>
    E> 10 -> <C 11
    11 <C -> <C 10
  B> 010 -> 111 E>
  111 <C -> <A 010


G(2n, 2^k - 1) -> D(n, 2^k)
  0 <A 010 11^k 0 -> <A 010 10^k 11

D(n, m) -> D(n', 0, 2 m' + 1)  (if b(m) > 2n) (n' < n)
  1000 0000^k <A 010 R(m) -> 1001 0001^k <A 010 R(m + 2^{k+1} - 1)
    -> <A 010 11 10 R(m + 2^{k+1} - 1)


Start -> G(0, 0, 0, 13)  @ Step 83

See also

• Skelet 26
• Skelet #34 is Infinite