A few weeks ago, I saw a few machines that weren’t formally proven yet, in particular, Skelet #15, #17, #26, and #33. @meithecatte and I finished formalizing the proof that Skelet #33 (11896833) doesn’t halt, and the proof is available here. Thanks to @meithecatte for proving `Theorem nonhalt`

and cleaning up the proof!

In the rest of this post, I will give an overview of the formal proof. The proof begins similarly to Skelet #34’s proof, but the proof diverged after I introduced `invariant(n, m)`

. This invariant made the TM configurations easier to reason about, and made the 3 theorems `step_reset`

+ `do_reset`

+ `E_next`

work properly.

## 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**If`D_inc`

.`m`

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

.**Theorem**If`start_reset`

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