Skelet 26

1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC--- (bbch), called Skelet #26, 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 equivalent to Skelet 15.

Skelet 26 was proven to be non-halting in January 2024 by int-y1 and meithecatte.

Analysis by Shawn Ligocki

https://www.sligocki.com/2023/02/05/shift-overflow.html

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

D(n, a, m) = L(n) 000 <C 101a R(m)
E(n, a, m) = L(n) 00  <C 101a R(m)
F(n, a, m) = L(n) 0   <C 101a R(m)
G(n, a, m) = L(n)     <C 101a R(m)

D(n, a, m) -> D(n+1, a, m+1)  (if b(m) > 1)
  L(n) 000 <C -> L(n+1) 000 B>
    1000 <C -> <C 1111
    0000 <C -> 1000 B>
  E> R(n) -> <C R(n+1)
    E> 11 -> 11 E>
    E> 10 -> <C 11
    11 <C -> <C 10
  B> 1010 -> 1111 E>
  1111 <C -> <C 1010
  B> 1011 -> 0111 E>
  0111 <C -> <C 1011


D(n-1, 0, 2^k - 1) -> E(n, 1, 2^k)
  0 1111 E> 11^k 0 -> <C 1011 10^k 11

E(n, a, m) -> E(n', 1, m')  (if b(m) > n) (n' < n)
  0100 0000^k <C 101a R(m) -> 0100 1000^k <C 101a R(m + 2^k - 1)
  0100 1000^k <C 101a R(m + 2^k - 1) -> <C 1011 10^2k 11 1a R(m + 2^k - 1)


D(n-1, 1, 2^k - 1) -> G(2n, 0, 2^{k-1})
 1000 0000^n 0111 E> 11^m+1 0 -> 01 0000^n+1 <C 1010 10^m 11

G(n, a, m) -> E(n', a', m')  (if b(m) > n) (n' < n)
  01 0000^k <C 101a R(m) -> <C 10 10^2k 11 1a R(m + 2^k - 1)

Start -> D(0, 0, 11)  @ Step 85

Skelet 15

1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC (bbch), also called Skelet #15, was proven to be non-halting together with Skelet 26 in January 2024 by int-y1 and meithecatte and has an individual proof of non-halting in Coq-BB5. It is a permutation of Skelet 26, achieved by starting Skelet 26 in state E and then normalizing to TNF. Its analysis is equivalent to that of Skelet 26, starting in configuration D(0, 0, 1) after 21 steps.