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

Analysis by int-y1 and meithecatte

https://discuss.bbchallenge.org/t/skelet-33-doesnt-halt-coq-proof/180

Counter phase

These definitions were copied over:

    b(n) is the first non-negative integer such that n + b(n) contains only 1’s in base-2. For example, b(15) = 0 and b(16) = 15. (Note: b(0) is not defined)
    L(n) is a tape defined by L(0) = 0^∞, L(2n) = L(n) 0000, and L(2n+1) = L(n) 1000.
    R(n) is a tape defined by R(0) = 0^∞, R(2n) = 10 R(n), and R(2n+1) = 11 R(n).
    K(n) is a tape defined by K(0) = 0^∞, K(2n) = K(n) 0000, and K(2n+1) = K(n) 0100. Note that L(n) = K(n) 0 for all n.

These definitions were slightly modified to fit Skelet #33:

    D(n, m) = L(n) <C 101010 R(m). D(n, m) represents a counter phase configuration.
    E(n, m) = K(n) <C 1010 R(m). E(n, m) represents a reset phase configuration.

First, we analyze the configuration D(n, m). Depending on m, the machine will follow either D_inc or start_reset.

    Lemma D_inc. If m contains a 0 in base-2, then D(n, m) ⊢* D(n+1, m+1).
    Theorem start_reset. If m contains only 1’s in base-2, then D(n, m) ⊢* E(n+1, 2(m+1)+1).

In summary, if the machine starts on D(n, m), it will repeatedly follow D_inc to get to D(n+b(m), m+b(m)) (see D_inc and D_finish in the proof). Since m+b(m) contains only 1’s in base-2, the machine will follow start_reset.

Now that the counter phase D(*, *) is analyzed, let’s move on to the reset phase E(*, *).

Reset phase

E(n, m) is easy to analyze when n is odd.

Lemma step_reset_odd. Let n, m be positive integers. Then E(2n+1, m) ⊢* E(n, 4m+2).
Proof. Simulate the machine. E(2n+1, m) = K(n) 0100 <C 1010 R(m) ⊢* K(n) <C 1010 1011 R(m) = E(n, 4m+2). □

The general case requires more setup:

    Let leads(n) be the statement that either n = 1, or n starts with 11 in base-2.
    Suppose q ≥ 0 and 0 ≤ r < 2^q. Then leads(3 * 2^q + r).
    Let invariant(n, m) be the statement that leads(n) is true, and b(m) = 3 * 2^q + r for some q ≥ 0 and 2n ≤ r < 2^q.

Theorem step_reset. Let n > 1 and m ≥ 1. Suppose invariant(n, m) is true. Then there exist 1 ≤ n' < n and m' ≥ 1 such that E(n, m) ⊢* E(n', m') and invariant(n', m') is true.

Proof

Factor n as n = 2^k (2n'+1) for some k ≥ 0 and n' ≥ 0. Define m' = (2(2(2^k - 1) + m) + 1) * 4^k + 1. We claim that n' and m' satisfy the theorem.

    Proof that n' ≥ 1. For the sake of contradiction, suppose n' = 0. As a result, n = 2^k. Since n > 1, it follows that leads(n) is false. This contradicts invariant(n, m).
    Proof that n' < n. This follows from n = 2^k (2n'+1).
    Proof that m' ≥ 1. This follows from the definition of m'.
    Proof that E(n, m) ⊢* E(n', m'). This follows from a sequence of steps:
        E(n, m) = E(2^k (2n'+1), m) = K(n') 0100 0000^k <C 1010 R(m)
        K(n') 0100 0000^k <C 1010 R(m) ⊢* K(n') 0100 1000^k <C 1010 R(2(2^k - 1) + m) (see LaR_max). Also, the right side does not overflow because b(m) = 3 * 2^q + r > r ≥ 2n > 2(2^k - 1).
        The machine runs on 0100 1000^k <C 1010 and eventually reaches E(n', m'). See eat_bin_max and drop_KI for more details.
    Proof that leads(n') is true. Note that n = 2^k (2n'+1) and leads(n) is true. Trailing 0’s don’t matter, so leads(2n'+1) is true. Lastly, since n' ≥ 1, a little bit of work shows that leads(n') is true.
    Proof that b(m') = 3 * 2^q' + r' for some q' ≥ 0 and 2n' ≤ r' < 2^q'. For this proof, use q' = q+2k+2 and r' = 2^(2k+2) * (r-2(2^k - 1)) + 3 * 2^(2k) - 2. See the proof for more details. □

Here’s a more useful version of Theorem step_reset.

Corollary do_reset. Let n ≥ 1 and m ≥ 1. Suppose invariant(n, m) is true. Then there exists m' ≥ 1 such that E(n, m) ⊢* E(1, m') and leads(b(m')) is true.
Proof. Use strong induction on n. For n = 1, use m' = m. From invariant(1, m), it follows that b(m) = 3 * 2^q + r where r < 2^q, and therefore, leads(b(m)). This finishes the base case. For n > 1, apply step_reset to go to a smaller case. □

Here’s the theorem that brings all of the previous work together.

Theorem E_next. Let m ≥ 1 and suppose leads(b(m)) is true. Then there exists m' ≥ 1 such that E(1, m) ⊢^+ E(1, m') and leads(b(m')) is true.

Proof

Firstly, direct simulation shows that E(1, m) ⊢^+ D(0, 2m+1). Follow D_finish to reach D(b(2m+1), 2m+1+b(2m+1)). Follow start_reset to reach E(b(2m+1)+1, 4m+5+2b(2m+1)). This simplifies to E(2b(m)+1, 4(m+b(m)+1)+1). Follow step_reset_odd to reach E(b(m), 16(m+b(m)+1)+6). Following do_reset is enough to finish the proof, but we still need to show that invariant(b(m), 16(m+b(m)+1)+6) is true. Here’s the proof that the invariant is true:

    Proof that leads(b(m)) is true. This is already given.
    Proof that b(16(m+b(m)+1)+6) = 3 * 2^q + r for some q ≥ 0 and 2b(m) ≤ r < 2^q. First, let m+b(m)+1 = 2^k for some k ≥ 1. Then b(16(m+b(m)+1)+6) = b(2^(k+4)+6) = 2^(k+4)-7 = 3 * 2^(k+2) + (2^(k+2)-7). Therefore, q = k+2 and r = 2^(k+2)-7. Lastly, Coq proved the inequality 2b(m) ≤ r using just lia. □

Theorem nonhalt. Skelet #33 does not halt.
Proof. The machine reaches E(1, 17). Also, leads(b(17)) = leads(14) is true. The conditions of Theorem E_next are satisfied. Apply Theorem E_next infinitely. □

See also

• Skelet 26
• Skelet #34 is Infinite