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. Both Skelet 26 and Skelet 15 are adjacent to Skelet 33.

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

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

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

Analyis by int-y1 and meithecatte

https://discuss.bbchallenge.org/t/skelet-26-and-15-do-not-halt-coq-proof/183

Here’s a summary of how Skelet #26 behaves:

    D(0, 0, *) ⊢* (D_finish) D(*, 0, 2^k - 1) ⊢^+ (start_reset0) E0(*, 1, 2^k) ⊢* (do_reset0) E0(0, 1, *) = D(0, 1, *)
    D(0, 1, *) ⊢* (D_finish) D(*, 1, 2^k - 1) ⊢^+ (start_reset1) E1(*, 0, 2^(k-1)) ⊢* (do_reset1) E0(0, *, *) = D(0, *, *)

The sections on D(n, a, m) and E0(n, a, m) are similar to Skelet #33’s proof. The sections on E1(n, a, m) and D0_nonhalt are completely new. Unlike Skelet #33, Skelet #26 reaches E1(n, a, m) often. The trickiest part was making reset_invariant(m) strong enough to handle E1(n, a, m).

Definitions

Firstly, here are a few definitions:

    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).
    K0(n) is a tape defined by K0(0) = 0^∞, K0(2n) = K0(n) 0000, and K0(2n+1) = K0(n) 0100. Note that L(n) = K0(n) 0 for all n. (This is the same as K(n) from my post on Skelet #33)
    K1(n) is a tape defined by K1(0) = 0^∞, K1(2n) = K1(n) 0000, and K1(2n+1) = K1(n) 0001. Note that L(n) = K1(n) 000 for all n.
    D(n, a, m) = L(n) <D 101a R(m).
    E0(n, a, m) = K0(n) <D 101a R(m).
    E1(n, a, m) = K1(n) <D 101a R(m).
    Let reset_invariant(m) be the statement that m ≥ 2, and b(m)+1 = 2^k (2n'+1) for some k ≥ 0 and n' ≥ 2.

The definitions for K1(n), E1(n, a, m), and reset_invariant(m) are completely new. The remaining definitions are copied or slightly modified from the Skelet #33 proof.

D(n, a, m) represents a counter phase configuration. E0(n, a, m) and E1(n, a, m) represent a reset phase configuration.

Counter phase - D(n, a, m)

Depending on a and m, the machine will follow either D_inc, start_reset0, or start_reset1.

    Lemma D_inc. If m contains a 0 in base-2, then D(n, a, m) ⊢* D(n+1, a, m+1).
    Theorem start_reset0. If m contains only 1’s in base-2, then D(n, 0, m) ⊢^+ E0(n+1, 1, m+1). (This is analogous to start_reset from my post on Skelet #33)
    Theorem start_reset1. If m contains only 1’s in base-2, then D(n, 1, m) ⊢^+ E1(2n+2, 0, (m+1)/2). (The Coq proof uses m' to represent (m+1)/2, because / is hard to use)

There is also Corollary D_finish. D(n, a, m) ⊢* D(n+b(m), a, m+b(m)). The proof is to repeatedly apply D_inc until it is no longer possible. □

In summary, if the machine starts on D(n, a, m), it will follow D_finish to get to D(n+b(m), a, m+b(m)). Since m+b(m) contains only 1’s in base-2, the machine will follow either start_reset0 or start_reset1 and enter the reset phase. Both E0 and E1 are part of the reset phase.

Reset phase - E0(n, a, m)

Theorem step_reset0. Let n > 0, m ≥ 1, and a ∈ {0,1}. Suppose n ≤ b(m). Then there exist 0 ≤ n' < n and m' ≥ 1 such that E0(n, a, m) ⊢* E0(n', 1, m'), n' ≤ b(m'), and reset_invariant(m') is true.

Proof

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

    Proof that n' < n. This follows from n = 2^k (2n'+1).
    Proof that m' ≥ 1. See the proof that m' ≥ 2.
    Proof that E0(n, a, m) ⊢* E0(n', 1, m'). This follows from a sequence of steps:
        E0(n, a, m) = E0(2^k (2n'+1), a, m) = K0(n') 0100 0000^k <D 101a R(m)
        K0(n') 0100 0000^k <D 101a R(m) ⊢* K0(n') 0100 1000^k <D 101a R(2^k - 1 + m) (see LaR_max). Also, the right side does not overflow because 2^k - 1 < n ≤ b(m).
        The machine runs on 0100 1000^k <D 101a until it reaches <D 1011 1010^k 111a. This configuration corresponds to E0(n', 1, m'). See eat_bin_max0 and drop_K0I for the Coq proof.
    Proof that n' ≤ b(m'). This is split into 2 parts.
        Proof that n' ≤ b(2^k - 1 + m). Since 2^k - 1 < n ≤ b(m), it follows that b(2^k - 1 + m) = b(m) - (2^k - 1). Also, b(m) - (2^k - 1) ≥ n - (2^k - 1) > 2^k (2n') ≥ n'.
        Proof that b(2^k - 1 + m) ≤ b(m'). On the right side, repeatedly apply b(2x) = 2b(x)+1 ≥ b(x) and b(2x+1) = 2b(x) ≥ b(x) until the inequality becomes b(2^k - 1 + m) ≤ b(2^k - 1 + m).
    Proof that m' ≥ 2. This follows from the definition of m'.
    Proof that b(m')+1 = 2^k' (2n''+1) for some k' ≥ 0 and n'' ≥ 2. We claim that k' = 2k and n'' = b(2(2^k - 1 + m) + a).
        Proof that b(m')+1 = 2^k' (2n''+1). Expand b(m') with b(2x) = 2b(x)+1 and b(2x+1) = 2b(x). Then the result follows.
        Proof that n'' ≥ 2. Note that n'' = b(2(2^k - 1 + m) + a) = 2b(2^k - 1 + m) + (1-a). Since 2^k - 1 < n ≤ b(m), it follows that b(2^k - 1 + m) > 0. So n'' ≥ 2*1+(1-1) = 2. □

Here’s a more useful version that repeatedly applies step_reset0 until n' = 0.

Corollary do_reset0. Let n > 0, m ≥ 1, and a ∈ {0,1}. Suppose n ≤ b(m). Then there exists m' ≥ 1 such that E0(n, a, m) ⊢* E0(0, 1, m') and reset_invariant(m') is true.
Proof. Use strong induction on n. Apply step_reset0 to obtain 0 ≤ n'' < n and m'' ≥ 1 such that E0(n, a, m) ⊢* E0(n'', 1, m''), n'' ≤ b(m''), and reset_invariant(m'') is true. If n'' = 0 then use m' = m'' and we’re done. Otherwise, apply the strong induction hypothesis on (n'', m'', 1) to obtain m'. Finish the proof with E0(n, a, m) ⊢* E0(n'', 1, m'') ⊢* E0(0, 1, m'). □

Reset phase - E1(n, a, m)

When Skelet #26 reaches E1(n, a, m), n is always even (see start_reset1), but the inequality “n ≤ b(m)” doesn’t always hold. As a result, I used the weaker statement that “n ≤ 4b(m), n = 2^(k+1) * (odd integer), and 2^(k+1) ≤ b(m)”.

Theorem step_reset1. Let n > 0, m ≥ 1, and a ∈ {0,1}. Suppose n ≤ 4b(m). Suppose n = 2^(k+1) (2n'+1) where k ≥ 0, 2^(k+1) ≤ b(m), and n' ≥ 0. Firstly, n' < n. Secondly, there exists m' ≥ 1 such that E1(n, a, m) ⊢* E0(n', 0, m'), n' ≤ b(m'), and reset_invariant(m') is true.

Proof

Define m' = (4(2^(k+1) - 1 + m) + 2a + 1) * 2 * 4^k. We claim that m' satisfies the theorem.

    Proof that n' < n. This follows from n = 2^(k+1) (2n'+1).
    Proof that m' ≥ 1. See the proof that m' ≥ 2.
    Proof that E1(n, a, m) ⊢* E0(n', 0, m'). This follows from a sequence of steps:
        E1(n, a, m) = E1(2^(k+1) (2n'+1), a, m) = K1(n') 0001 0000^(k+1) <D 101a R(m)
        K1(n') 0001 0000^(k+1) <D 101a R(m) ⊢* K1(n') 0001 1000^(k+1) <D 101a R(2^(k+1) - 1 + m) (see LaR_max). Also, the right side does not overflow because 2^(k+1) - 1 < 2^(k+1) ≤ b(m).
        The machine runs on 0001 1000^(k+1) <D 101a until it reaches 00 <D 10 1010^(k+1) 111a. Note that K1(n') 00 = K0(n'). This configuration corresponds to E0(n', 0, m'). See eat_bin_max1 and drop_K1I for the Coq proof.
    Proof that n' ≤ b(m'). Split the inequality into n' ≤ b(2^(k+1) - 1 + m) and b(2^(k+1) - 1 + m) ≤ b(m'), and do the same approach as step_reset0. The Coq proof is copy-pasted too, except I added unfold b.
    Proof that m' ≥ 2. This follows from the definition of m'.
    Proof that b(m')+1 = 2^k' (2n''+1) for some k' ≥ 0 and n'' ≥ 2. We claim that k' = 2k+1 and n'' = b(2(2^(k+1) - 1 + m) + a).
        Proof that b(m')+1 = 2^k' (2n''+1). Expand b(m') with b(2x) = 2b(x)+1 and b(2x+1) = 2b(x). Then the result follows.
        Proof that n'' ≥ 2. Note that n'' = b(2(2^(k+1) - 1 + m) + a) = 2b(2^(k+1) - 1 + m) + (1-a). Since 2^(k+1) - 1 < 2^(k+1) ≤ b(m), it follows that b(2^(k+1) - 1 + m) > 0. So n'' ≥ 2*1+(1-1) = 2. □

step_reset1 says that E1(n, a, m) ⊢* E0(n', 0, m'). If n' > 0, we can apply do_reset0 to get E0(n', 0, m') ⊢* E0(0, 1, m''). The full details are in Corollary do_reset1.

Corollary do_reset1. Let n > 0, m ≥ 1, and a ∈ {0,1}. Suppose n ≤ 4b(m). Suppose n = 2^(k+1) (2n'+1) where k ≥ 0, 2^(k+1) ≤ b(m), and n' ≥ 0. Then there exist m' ≥ 1 and a' ∈ {0,1} such that E1(n, a, m) ⊢* E0(0, a', m') and reset_invariant(m') is true.
Proof. Apply step_reset1 to obtain 0 ≤ n'' < n and m'' ≥ 1 such that E1(n, a, m) ⊢* E0(n'', 0, m''), n'' ≤ b(m''), and reset_invariant(m'') is true. Then do cases on n'':

    If n'' = 0 then use (m', a') = (m'', 0) and we’re done.
    If n'' > 0 then apply do_reset0 on (n'', m'', 1) to obtain m'. Use m' and a' = 1. □

Putting the results together - D0_nonhalt

Theorem D0_next. Let m ≥ 1. There exists m' ≥ 1 such that D(0, 0, m) ⊢^+ D(0, 1, m') and reset_invariant(m') is true.
Proof. Follow D_finish to reach D(b(m), 0, b(m)+m). Follow start_reset0 to reach E0(b(m)+1, 1, b(m)+m+1). Following do_reset0 is enough to finish the proof, because E0(0, 1, m') = D(0, 1, m'). However, we need to show that b(m)+1 ≤ b(b(m)+m+1). b(m)+m+1 is a power of 2, so let b(m)+m+1 = 2^k to obtain b(b(m)+m+1) = b(2^k) = 2^k-1 = b(m)+m ≥ b(m)+1. □

Theorem D1_next. Let m ≥ 1 and suppose reset_invariant(m) is true. There exist m' ≥ 1 and a' ∈ {0,1} such that D(0, 1, m) ⊢^+ D(0, a', m') and reset_invariant(m') is true.

Proof

Follow D_finish to reach D(b(m), 1, b(m)+m). Follow start_reset1 to reach E1(2b(m)+2, 0, (b(m)+m+1)/2). Following do_reset1 is enough to finish the proof, because E0(0, a', m') = D(0, a', m'). However, do_reset1 needs the following proofs:

    Proof that 2b(m)+2 ≤ 4b((b(m)+m+1)/2). Since b(m)+m+1 is a power of 2 and is at least 2, let b(m)+m+1 = 2^(x+1) for some x ≥ 0. Then 4b((b(m)+m+1)/2) = 4b(2^x) = 2(2^(x+1))-4 = 2(b(m)+m+1)-4 ≥ 2(b(m)+2+1)-4 = 2b(m)+2.
    Proof that 2b(m)+2 = 2^(k+1) (2n'+1) where k ≥ 0, 2^(k+1) ≤ b((b(m)+m+1)/2), and n' ≥ 0. From reset_invariant(m), we have b(m)+1 = 2^k (2n'+1) for some k ≥ 0 and n' ≥ 2. It remains to show 2^(k+1) ≤ b((b(m)+m+1)/2). Since 2b(m)+2 ≤ 4b((b(m)+m+1)/2), it is enough to show 2^(k+1) ≤ (b(m)+1)/2. This is true because 2^(k+1) * 2 < 2^k * 5 ≤ 2^k (2n'+1) = b(m)+1. □

Theorem D_next. Let m ≥ 1 and a ∈ {0,1}. Suppose reset_invariant(m) is true. There exist m' ≥ 1 and a' ∈ {0,1} such that D(0, a, m) ⊢^+ D(0, a', m') and reset_invariant(m') is true.
Proof. If a = 0 then apply D0_next. If a = 1 then apply D1_next. □

Theorem D0_nonhalt. For all m ≥ 1, D(0, 0, m) will not reach a halting configuration. (Thanks to @meithecatte for contributing this theorem!)
Proof. Follow D0_next to reach D(0, 1, m') where m' ≥ 1 and reset_invariant(m') is true. Then follow D_next indefinitely. □

Skelet #26 and #15 do not halt

Corollary nonhalt. Skelet #26 does not halt.
Proof. Simulate Skelet #26 until it reaches D(0, 0, 11). Then apply D0_nonhalt. □

Corollary nonhalt (in Skelet15.v). Skelet #15 does not halt. (Thanks to @meithecatte for contributing this proof!)
Proof. Permute the states and flip the left/right transitions. As a result, Skelet #15 is Skelet #26 with the starting state as E. Simulate Skelet #15 until it reaches D(0, 0, 1), then apply D0_nonhalt. □

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, except that it starts in configuration D(0, 0, 1) after 21 steps.

See also

• Skelet #34 is Infinite