@meithecatte and I finished formalizing the proof that Skelet #26 (13134219) doesn’t halt, and the proof is available here. Thanks to @meithecatte for cleaning up the proof! Also thanks to @meithecatte for creating `D0_nonhalt`

and using it to show that Skelet #15 (2204428, proof) doesn’t halt!

The only machine that doesn’t have a formal proof is Skelet #17.

In the rest of this post, I will give an overview of the formal proof. 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**If`D_inc`

.`m`

contains a 0 in base-2, then`D(n, a, m) ⊢* D(n+1, a, m+1)`

.**Theorem**If`start_reset0`

.`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**If`start_reset1`

.`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
- 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`

. □

- Proof that

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`

. □

- Proof that

`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`

. □