1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---

In busycoq comment-block style:

1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---

K(d_1 .. d_m; a, b) := 0^inf <C (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf
d~(u,0,v) := (10)^v 00 (01)^u,   d~(u,1,v) := (10)^v (01)^u        (d_m least significant)

start from K((1,1,3); 4, 1)                                   (step 215, §4)

M  (carry; some bit is 0; j* = index of the LAST bit-0 digit, k = m - j*):
   K(.., (u,0,v), (u_j,1,v_j)_{j*<j<=m}; a, b)
     --> K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j*<j<=m}; a+1, b+2)
   steps 32 + 8a + 8b + 4v + sum_{j>j*} (8 u_j + 4 v_j)
   needs v >= 1 (u >= 0), u_j >= 1 and v_j >= 1 for j > j*, a >= 0, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, §1)
O  (overflow; all bits 1):
   K((u_1,1,v_1) .. (u_m,1,v_m); a, b)
     --> K((0,0,u_1), (v_1-1,0,u_2), .., (v_{m-1}-1,0,u_m), (v_m,1,a); b+3, 1)
   steps 89 - 4m + 8a + 20b + 4 sum u_j + 8 sum v_j
   needs m >= 1, all u_j, v_j >= 1, a >= 1, b >= 0

On the tape:

M:  0^inf <C (01)^b 000 (01)^a [(10)^v_j (01)^u_j]_{j=m..j*+1} (10)^v 00 (01)^u X
      --> 0^inf <C (01)^(b+2) 000 (01)^(a+1) [(10)^(v_j-1) 00 (01)^u_j]_{j=m..j*+1} (10)^(v-1) (01)^(u+1) X
O:  0^inf <C (01)^b 000 (01)^a [(10)^v_j (01)^u_j]_{j=m..1} 1001 0^inf
      --> 0^inf <C 01 000 (01)^(b+3) (10)^a (01)^v_m [(10)^u_j 00 (01)^(v_(j-1)-1)]_{j=m..2} (10)^u_1 00 1001 0^inf

Here X is everything right of d_{j*}, and M never reads it.

The M and O rules are not taken from simulation. §2.1 lists 20 window lemmas, and §2.2–2.3 derive M and O from them as chains of intermediate configurations. Each step count is the sum along its chain.

The same O chain with no digits (m = 0) gives

K(; a, b) --> K((1,1,a); b+3, 1)        in 89 + 8a + 20b steps   (a ≥ 1)

It occurs once, inside the initial segment (§4), and the invariant argument does not use it.

2.1 Building blocks

A window lemma w → w' says: started on the cells of w, the machine runs the stated number of steps without reading a cell outside w, and leaves w'. The last step may move the head onto a neighbouring cell. Such a lemma holds in every tape context.

• T1–T14 are exact finite runs on this table.
• For S1–S6, one block is a finite run, and induction on n gives every n.

For example, S5 is (one block, then the IH):

(10)^(n+1) 11 <D  =  (10)^n 1011 <D  →  (10)^n 11 <D 01  →  11 <D (01)^n 01

Each lemma is the reflection of the parent's lemma of the same name, so the names match the parent's .v (§6.1).

Shift lemmas

S5 and S6 are the back-bounces. Each block costs 6 steps for a 2-cell advance, because the head doubles back over cells it has just written (S5 moves L L R R L L, S6 moves L R R L L L).

Finite lemmas

Digit lemmas

These are compositions; u, v are those of one digit.

In Ro, S6 starts on the first 0 of (01)^u = 0 1 (01)^(u−1).

What each digit lemma does:

• Lb sweeps a bit-1 digit rightward.
• Lf flips the bit-0 digit.
• Rb restores a swept digit as bit 0 on M's way back.
• Ro does the same in O.

2.2 Derivation of M

Notation:

• X is everything right of d_{j*}. It is never read.
• (u*, v*) is d_{j*} = (u*,0,v*).
• Y = Π_{i=k..1} (10)^v_i (01)^u_i is the trailing bit-1 digits, written left to right. i = k is d_m, and i = 1 is d_{j*+1}.

The chain:

                                                                                        steps
    0^inf <C (01)^b 000 (01)^a Y (10)^v* 00 (01)^u* X
 Phase 1: left-edge preamble with a dip into the 000 gap                                4b+10
T1  0^inf 10 E> (01)^b 000 (01)^a Y ..                                                  3
S4  0^inf (10)^(b+1) E> 000 (01)^a Y ..                                                 2b
T2  0^inf (10)^(b+1) <C 001 (01)^a Y ..                                                 5
S1  0^inf <C (01)^(b+1) 0 (01)^(a+1) Y ..                                               2b+2
 Phase 2: one long right sweep, up to the 00 of d_{j*}                                  2a+2b+9+4v*+Σ(2u_i+2v_i)
T1  0^inf 10 E> (01)^(b+1) 0 (01)^(a+1) Y ..                                            3
S4  0^inf (10)^(b+2) E> 0 (01)^(a+1) Y ..                                               2b+2
T3  0^inf (10)^(b+2) 110 E> (01)^a Y ..                                                 3
S4  0^inf (10)^(b+2) 110 (10)^a E> Y (10)^v* 00 (01)^u* X                               2a
Lb  0^inf (10)^(b+2) 110 (10)^a Y' E> (10)^v* 00 (01)^u* X        (i = k down to 1)     Σ(2u_i+2v_i)
                         Y' = Π_{i=k..1} 11 (01)^(v_i−1) (10)^u_i
Lf  0^inf (10)^(b+2) 110 (10)^a Y' 11 <D (10)^(v*−1) (01)^(u*+1) X                      4v*+1
 Phase 3: leftward pass with 2-cell back-bounces, then a plain run to the edge          6a+2b+13+Σ(6u_i+2v_i)
Rb  0^inf (10)^(b+2) 110 (10)^a 11 <D Y'' (10)^(v*−1) (01)^(u*+1) X   (i = 1 up to k)   Σ(6u_i+2v_i)
                         Y'' = Π_{i=k..1} (10)^(v_i−1) 00 (01)^u_i
S5  0^inf (10)^(b+2) 110 11 <D (01)^a Y'' ..                                            6a
T8  0^inf (10)^(b+2) <C 00001 (01)^a Y'' ..                                             9
S1  0^inf <C (01)^(b+2) 000 (01)^(a+1) Y'' (10)^(v*−1) (01)^(u*+1) X                    2b+4

The last line is

K(.., (u*+1,1,v*−1), (u_i,0,v_i−1)_i; a+1, b+2)

The sum is

(4b+10) + (2a+2b+9+4v*) + (6a+2b+13) + Σ(8u_i+4v_i) = 32 + 8a + 8b + 4v* + Σ(8u_i+4v_i)

Head path

• Phase 1 runs right only as far as the 000 gap, turns (T2) and returns to the edge.
• Phase 2 is the only long rightward leg. Its rightmost read is the right 0 of d_{j*}'s 00: T6 reads both cells, then moves left. So M is a side rule, and the tape X right of that 00 is never read.
• Phase 3 moves left. It doubles back once per 10 block (S5, on the swept digits' (10)^u_i and on (10)^a). It crosses the (01)^(v−1) blocks and the final (10)^(b+2) with plain sweeps (S2, S1).

Drops

When v* = 1, the flipped digit (u*+1,1,0) = (01)^(u*+1) drops (§1).

When some v_i = 1, the result has (u_i,0,0). That can happen only outside INV (§3.3).

2.3 Derivation of O

Let Y = Π_{i=m..1} (10)^v_i (01)^u_i, with all digits bit 1. The chain:

                                                                                        steps
    0^inf <C (01)^b 000 (01)^a Y 1001 0^inf
 Phases 1–2 as in M, with Lb on all m digits and no Lf                                  (4b+10)+(2a+2b+8)+Σ(2u_i+2v_i)
    0^inf (10)^(b+2) 110 (10)^a Y' E> 1001 0^inf              Y' = Π_{i=m..1} 11 (01)^(v_i−1) (10)^u_i
 Phase 3: turn at the far right
T9  0^inf (10)^(b+2) 110 (10)^a Y' <C 000 1001 0^inf                                    13
 Phase 4: leftward pass
Ro  0^inf (10)^(b+2) 110 (10)^a <C Y''' 000 1001 0^inf      (i = 1 up to m)             Σ(2u_i+6v_i−4)
                         Y''' = Π_{i=m..1} 000 (01)^(v_i−1) 1 (01)^(u_i−1)
 Phase 5: left end                                                                      2a+8b+30
S1  0^inf (10)^(b+2) 110 <C (01)^a Y''' ..                                              2a
T11 0^inf (10)^(b+2) 11 <D 1 (01)^a Y''' ..                                             1
S5  0^inf 11 <D (01)^(b+2) 1 (01)^a Y''' ..                                             6b+12
T12 0^inf 10110 E> (01)^(b+2) 1 (01)^a Y''' ..                                          13
S4  0^inf 10110 (10)^(b+2) E> 1 (01)^a Y''' ..                                          2b+4
 Phase 6: short right sweep over the a block, to the 000 that Ro left before d_m        2a+1
T13 0^inf 10110 (10)^(b+2) 110 E> (01)^(a−1) Y''' ..                                    3
S4  0^inf 10110 (10)^(b+2) 1 (10)^a E> 000 (01)^(v_m−1) ..                              2a−2
 Phase 7: turn in that 000, final run to the edge                                       2a+6b+27
T2  0^inf 1011 (01)^(b+3) (10)^a <C 001 (01)^(v_m−1) ..   (0 (10)^(b+2) 1 = (01)^(b+3))   5
S1  0^inf 1011 (01)^(b+3) <C (01)^a 001 (01)^(v_m−1) ..                                 2a
S6  0^inf 1011 <C 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) ..                         6b+18
T14 0^inf <C 0100 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) ..                         4

Re-read the final tape with the two identities

1 (01)^(n−1) 0 = (10)^n          01 (01)^(n−1) = (01)^n

splitting each 000 of Y''' as 0 | 00:

0^inf <C 0100 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) 1 (01)^(u_m−1) [000 (01)^(v_i−1) 1 (01)^(u_i−1)]_{i=m−1..1} 000 1001 0^inf
  = 0^inf <C 01 000 (01)^(b+3) (10)^a (01)^v_m [(10)^u_(i+1) 00 (01)^(v_i−1)]_{i=m−1..1} (10)^u_1 00 1001 0^inf
  = K((0,0,u_1), (v_1−1,0,u_2), .., (v_{m−1}−1,0,u_m), (v_m,1,a); b+3, 1)

The sum is

(4b+10) + (2a+2b+8) + 13 + (2a+8b+30) + (2a+1) + (2a+6b+27) + Σ(4u_i+8v_i−4) = 89 − 4m + 8a + 20b + 4Σu_i + 8Σv_i

Domain

• Lb and Ro need u_i, v_i ≥ 1.
• T13 and the S6 of phase 7 use the first 0 1 of (01)^a, so a ≥ 1.
• T9 needs 0^inf on the right. It reads the three blank cells right of 1001 and moves the marker three cells right, so the rightmost cell visited moves 3 cells per overflow.

O has two long rightward legs: phase 2, and the short phase 6.

O at m = 0 (the init, §4)

The same chain with no digits works: phase 4 is empty, and phase 6 ends on T9's 000. The final tape is

0^inf <C 01 000 (01)^(b+3) 1 (01)^(a−1) 001 1001 0^inf
  = 0^inf <C 01 000 (01)^(b+3) (10)^a 01 1001 0^inf
  = K((1,1,a); b+3, 1)

The step count is 89 + 8a + 20b.

2.4 What the rules do, in words

The digits form a binary counter, and each M is one increment.

• M flips the trailing 1s to 0 and the last 0 to 1. Every digit it touches pays one 10 from its v, and a digit flipping 0→1 also gains a 01.
• When all bits are 1, O swaps the two halves of every digit. Each (01)^u becomes the (10)^u fuel of a new bit-0 digit, and each (10)^v becomes the next digit's (01)^(v−1). The counter restarts at value 1 with one more digit.
• When a digit flipping 0→1 has spent its last 10 (v = 1), it drops: its 01s merge into the next digit, and the counter loses that digit.

The only way the rules can fail is the failure mode: a carry reaches a bit-0 digit with v = 0, where Lf's first lemma T4 has no 10 to read. That happens if a carry flips a bit-1 digit with v = 1 to 0.

Every macro step is an exact run of at least 32 steps, so every macro step makes progress.