Lemma nonhalt: ~halts tm c0.
Proof.
  eapply multistep_nonhalt. 1: apply init0.
  change (K 1 0 0 1) with (St (false, 1%nat, 1%nat)).
  apply progress_nonhalt_cond with (P := I).
  - apply step_I.
  - cbn. lia.
Qed.

(*
1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF  (only E1 is undefined)

words: W(e,o): bit d of e at offset 2d, bit d of o at offset 2d+1 (offset 0 = the cell A reads)
std(N) = W(N,0);   pk(N) = W(N-2^(P+1), 2^P) for 2^(P+1) <= N < 2^(P+2)
K(w,n,m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf   (= w <| R n m);   S(typ,N,m) = K(typ(N),0,m)
phi(w): last cell 0 -> 1;  else (e,e+1) := lowest pair of adjacent 0 cells: cell e+1 := 1, cells 0..e := 0

R1  K(w,n,m) --> K(phi(w), n-1, m+1)       n >= 1
R2  K(w,0,m) --> K(x, m+1+u, 0)            phi(w) = x 1 0^(2u)
R3  K(w,0,m) --> K(x', 0, m+u+2)           phi(w) = x' 0 0 1 0^(2u+1)  (x'00 may be 0^inf)
R4  K(w,0,m) --> halt (E1)                 phi(w) = x 1 1 0^(2u+1)
R5  K(w,0,m) --> nested scan, no rule      phi(w) = x 1 0 1 0^(2u+1)

N+1 = (2k+1) 2^i,  b = m+1+i,  L = bitlen(k),  r = k - 2^(L-1)
S0  S(std,N,m) --> S(std, b, b)                k = 0
S1  S(std,N,m) --> S(pk, 2k+b, b)              k >= 1, and k = 2^(L-1) or 2k+b >= 2^(L+1)
S2  S(std,N,m) --> S(std, b+L+3, b+L+3)        2k+b+1 = 2^(L+1)
S3  S(std,N,m) --> S(std, D+n, n)              k < 3*2^(L-2), 3*2^(L-1) < 2k+b+1 < 2^(L+1)
P0  S(pk,N,m)  --> S(std, b+1, b+1)            k = 0
P1  S(pk,N,m)  --> S(std, k+b, b)              k = 2^(L-1)
P2  S(pk,N,m)  --> S(std, 2r+b, b)             r >= 1, 2r+b >= 2^L
P3  S(pk,N,m)  --> S(std, b+L+1, b+L+1)        r >= 1, 2r+b+1 = 2^L
P4  S(pk,N,m)  --> S(pk, D+n, n)               1 <= r < 2^(L-2), 2^(L-1) < 2r+b+1 < 2^L

invariant I(typ,N,m):   1 <= m <= N (pk: N >= 2), and
  N = m (mod 2):   std: 2N <= 3m+6 (N even), N <= 2m+3 (N odd);   pk: N <= 2m+3 (N even), 2N <= 5m+6 (N odd)
  N != m (mod 2):  N <= m+3

start: c0 -->(32) K(1,0,1) = S(std,1,1), which satisfies I
*)