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.[1] It is adjacent to Skelet 34.[2]
Skelet 33 was formally proven to be non-halting in December 2023 by int-y1[3] and meithecatte.[4]
Analysis by Shawn Ligocki[2]
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. □