(* 1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB--- never halts.
   A base-4 counter (sheet class Skelet 1-like Class 1).  At every D-record the tape is
     0^inf [1100] w_1 w_2 ... w_m D> 0^inf
   where each w_i is a sea word s = 100 or a digit word P0 = 11001100, P1 = 110000,
   P2 = 1001100, P3 = 10000, the least significant digit is the rightmost one, and the
   wall 1100 is optional.  One sweep adds 1: the head runs left, every digit 3 on the way
   wraps to 0 and eats the first sea word to its right, the first digit below 3 steps up
   (a digit 1 also eats a sea word), and the head runs back and appends s s.  When every
   digit is 3 the carry reaches the left end: a wall is erased (O1); without a wall, a wall
   is built and a new digit 3 is born at the right end (O2).
   Adapted from verify/Sk1Machines.v, Module Sk1Counter, in part: the same view of a digit
   counter on fixed words in a periodic sea that pays one sea word per carry step.  Its batch
   rule does not fit here (a wrap moves its digit by 2 cells, a carry eats through empty
   fields, and O2 is a second kind of pass), so the sweep is modelled on token lists instead.
   Section 1: the pass lemmas, each one plain es (busycoq finds the shift rules itself).
   Section 2: tokens, the tape encoding, and the sweep as a function lpass on token lists;
   during the left pass the processed tail is a list of X = 10101010 and s.
   Section 3: soundness: a defined sweep is a run of the machine from one D-record to the next.
   Section 4: the invariant JL: in every suffix of the word list that starts with a digit,
   and in the whole list, the sea words outnumber the digits 1 and 3 by at least 2.  It makes
   every sweep defined, and every sweep preserves it: the suffix that starts at the stop
   digit, and every longer one, gains at least 1 (sea words minus odd digits), while the
   words written right of the stop digit are digits 0 and sea words ending in s s (or, in O2,
   P3 s s s).  This replaces the write-up's epoch theorem (its section 5): the formal proof
   needs no count of sweeps per epoch and no bound on the newborn digit's field.
   Section 5: 108 steps from the blank tape to 0^inf P1 s s s D> 0^inf, then nonhalt by
   progress_nonhalt_cond.
   Informal proof: the accompanying write-up (proof.md).
   Formalized with Claude Code (AI-assisted).
   Checked: compiles against unmodified busycoq BB6 (commit 0940bb9) with Coq 8.20.1;
   Print Assumptions nonhalt: Closed under the global context. *)

From BusyCoq Require Import Individual62.
Require Import Lia.
Require Import String.
Require Import List.
Require Import Arith.
Import ListNotations.

Definition tm := Eval compute in (TM_from_str "1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---").

Notation "c --> c'" := (c -[ tm ]-> c')   (at level 40).
Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

Open Scope list.

(* ===================================================================== *)
(* Section 1. Pass lemmas (write-up section 3), each one plain es.       *)
(* s = 100, X = 10101010, P0..P3 the digit words; <[..] is a left-side   *)
(* word written in tape order.                                           *)
(* ===================================================================== *)

(* S0: 100 D> 0^inf --> 100 <B 1010 0^inf  (9 steps): a sweep starts *)
Lemma S0 l : l <* <[1;0;0] {{D}}> 0inf -->+ l <* <[1;0;0] <{{B}} [1;0;1;0] *> 0inf.
Proof. es. Qed.

(* L1: 100 <B --> <B 100  (5 steps): the left pass crosses a sea word *)
Lemma L1 l r : l <* <[1;0;0] <{{B}} r -->+ l <{{B}} [1;0;0] *> r.
Proof. es. Qed.

(* L2: 10000 <B X^j 100 --> <B X^(j+1)  (19 + 20j steps): a digit 3 wraps; X = 10101010 *)
Lemma L2 l j r : l <* <[1;0;0;0;0] <{{B}} [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> r -->+
  l <{{B}} [1;0;1;0;1;0;1;0]^^(S j) *> r.
Proof. es. Qed.

(* L3: 11001100 <B --> 110000 10 A>  (9 steps): stop at phase 0 *)
Lemma L3 l r : l <* <[1;1;0;0;1;1;0;0] <{{B}} r -->+ l <* <[1;1;0;0;0;0] <* <[1;0] {{A}}> r.
Proof. es. Qed.

(* L4: 1001100 <B --> 10000 10 A>  (9 steps): stop at phase 2 *)
Lemma L4 l r : l <* <[1;0;0;1;1;0;0] <{{B}} r -->+ l <* <[1;0;0;0;0] <* <[1;0] {{A}}> r.
Proof. es. Qed.

(* L5: 110000 <B X^j 100 X^i 100 --> 1001100 P0^(i+j) 100 10 A>  (59 + 56j + 36i steps): stop at phase 1 *)
Lemma L5 l j i r : l <* <[1;1;0;0;0;0] <{{B}} [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> [1;0;1;0;1;0;1;0]^^i *> [1;0;0] *> r -->+
  l <* <[1;0;0;1;1;0;0] <* <[1;1;0;0;1;1;0;0]^^(i+j) <* <[1;0;0] <* <[1;0] {{A}}> r.
Proof. es. Qed.

(* L5e: 110000 <B X^j 100 X^i 1010 0^inf --> 1001100 P0^(i+j) 100 100 D> 0^inf  (62 + 56j + 36i steps) *)
Lemma L5e l j i : l <* <[1;1;0;0;0;0] <{{B}} [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> [1;0;1;0;1;0;1;0]^^i *> [1;0;1;0] *> 0inf -->+
  l <* <[1;0;0;1;1;0;0] <* <[1;1;0;0;1;1;0;0]^^(i+j) <* <[1;0;0] <* <[1;0;0] {{D}}> 0inf.
Proof. es. Qed.

(* L6: 0^inf 1100 <B --> 0^inf 10 A>  (9 steps): the carry erases the wall (O1) *)
Lemma L6 r : 0inf <* <[1;1;0;0] <{{B}} r -->+ 0inf <* <[1;0] {{A}}> r.
Proof. es. Qed.

(* L7: 0^inf <B X^j 100 --> 0^inf 1100 P0^j 100 1 E>  (38 + 56j steps): the carry builds a wall (O2) *)
Lemma L7 j r : 0inf <{{B}} [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> r -->+
  0inf <* <[1;1;0;0] <* <[1;1;0;0;1;1;0;0]^^j <* <[1;0;0] <* <[1] {{E}}> r.
Proof. es. Qed.

(* RA1: 10 A> X^j 100 --> P0^j 100 10 A>  (3 + 36j steps): right pass, one group *)
Lemma RA1 l j r : l <* <[1;0] {{A}}> [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> r -->+
  l <* <[1;1;0;0;1;1;0;0]^^j <* <[1;0;0] <* <[1;0] {{A}}> r.
Proof. es. Qed.

(* RA3: 10 A> X^j 1010 0^inf --> P0^j 100 100 D> 0^inf  (6 + 36j steps): right pass ends *)
Lemma RA3 l j : l <* <[1;0] {{A}}> [1;0;1;0;1;0;1;0]^^j *> [1;0;1;0] *> 0inf -->+
  l <* <[1;1;0;0;1;1;0;0]^^j <* <[1;0;0] <* <[1;0;0] {{D}}> 0inf.
Proof. es. Qed.

(* RE1: 100 1 E> X^j 100 --> P0^j 100 100 1 E>  (5 + 36j steps): O2 right pass, one group *)
Lemma RE1 l j r : l <* <[1;0;0] <* <[1] {{E}}> [1;0;1;0;1;0;1;0]^^j *> [1;0;0] *> r -->+
  l <* <[1;1;0;0;1;1;0;0]^^j <* <[1;0;0] <* <[1;0;0] <* <[1] {{E}}> r.
Proof. es. Qed.

(* RE2: 100 100 1 E> 1010 0^inf --> 10000 100 100 100 D> 0^inf  (49 steps): birth of a digit 3 *)
Lemma RE2 l : l <* <[1;0;0] <* <[1;0;0] <* <[1] {{E}}> [1;0;1;0] *> 0inf -->+
  l <* <[1;0;0;0;0] <* <[1;0;0] <* <[1;0;0] <* <[1;0;0] {{D}}> 0inf.
Proof. es. Qed.

(* ===================================================================== *)
(* Section 2. Tokens, encodings and the sweep.                           *)
(* A configuration is (w, ts): w says whether the wall 1100 is present,  *)
(* ts lists the words left of the head, leftmost first.  K w ts is the   *)
(* D-record 0^inf [1100] ts D> 0^inf.  lpass runs the left pass on Lr    *)
(* (the unread words, nearest first) and the processed tail T (tX = X,   *)
(* tS = s, followed by 1010 0^inf), then the turn and the right pass.    *)
(* ===================================================================== *)

Inductive dg := d0 | d1 | d2 | d3.
Inductive tok := Dg (d : dg) | Sw.
Inductive tt := tX | tS.

Definition rdw (d : dg) : list Sym :=
  match d with
  | d0 => [0;0;1;1;0;0;1;1]
  | d1 => [0;0;0;0;1;1]
  | d2 => [0;0;1;1;0;0;1]
  | d3 => [0;0;0;0;1]
  end.

Definition rtw (t : tok) : list Sym := match t with Dg d => rdw d | Sw => [0;0;1] end.

Definition lsd (l : side) (ts : list tok) : side := fold_left (fun l t => l <* rtw t) ts l.

Definition base (w : bool) : side := if w then const 0 <* [0;0;1;1] else const 0.

Definition K (w : bool) (ts : list tok) : Q * tape := lsd (base w) ts {{D}}> const 0.

Definition xw : list Sym := [1;0;1;0;1;0;1;0].

Fixpoint renc (T : list tt) (r : side) : side :=
  match T with
  | [] => r
  | tX :: T' => xw *> renc T' r
  | tS :: T' => [1;0;0] *> renc T' r
  end.

Definition tend : side := [1;0;1;0] *> const 0.

Definition tok_of (x : tt) : tok := match x with tX => Dg d0 | tS => Sw end.

Fixpoint rmS (T : list tt) : option (list tt) :=
  match T with
  | [] => None
  | tS :: T' => Some T'
  | tX :: T' => match rmS T' with Some T1 => Some (tX :: T1) | None => None end
  end.

Fixpoint lpass (w : bool) (Lr : list tok) (T : list tt) : option (bool * list tok) :=
  match Lr with
  | [] =>
      if w then Some (false, map tok_of T ++ [Sw; Sw])
      else match rmS T with
           | Some T1 =>
               match rev T1 with
               | tS :: Rv => Some (true, map tok_of (rev Rv) ++ [Dg d3; Sw; Sw; Sw])
               | _ => None
               end
           | None => None
           end
  | Sw :: Lr' => lpass w Lr' (tS :: T)
  | Dg d3 :: Lr' => match rmS T with Some T1 => lpass w Lr' (tX :: T1) | None => None end
  | Dg d0 :: Lr' => Some (w, rev Lr' ++ Dg d1 :: map tok_of T ++ [Sw; Sw])
  | Dg d1 :: Lr' =>
      match rmS T with
      | Some T1 => Some (w, rev Lr' ++ Dg d2 :: map tok_of T1 ++ [Sw; Sw])
      | None => None
      end
  | Dg d2 :: Lr' => Some (w, rev Lr' ++ Dg d3 :: map tok_of T ++ [Sw; Sw])
  end.

Definition sweep (w : bool) (ts : list tok) := lpass w (rev ts) [].

(* Tape algebra. *)

Lemma lsd_app l a b : lsd l (a ++ b) = lsd (lsd l a) b.
Proof. unfold lsd. apply fold_left_app. Qed.

Lemma lsd_cons l t ts : lsd l (t :: ts) = lsd (l <* rtw t) ts.
Proof. reflexivity. Qed.

Lemma lsd_nil l : lsd l [] = l.
Proof. reflexivity. Qed.

Lemma lsd_rep0 j : forall l, lsd l (repeat (Dg d0) j) = l <* [0;0;1;1;0;0;1;1]^^j.
Proof.
  induction j as [|j IH]; intros l; [reflexivity|].
  cbn [repeat]. rewrite lsd_cons, IH. cbn [rtw rdw lpow].
  rewrite Str_app_assoc. apply lpow_shift'.
Qed.

Lemma lsd_map_rep j l : lsd l (map tok_of (repeat tX j)) = l <* [0;0;1;1;0;0;1;1]^^j.
Proof. rewrite map_repeat. apply lsd_rep0. Qed.

Lemma renc_app a b r : renc (a ++ b) r = renc a (renc b r).
Proof. induction a as [|[] a IH]; cbn; [reflexivity | rewrite IH; reflexivity | rewrite IH; reflexivity]. Qed.

Lemma renc_rep j r : renc (repeat tX j) r = xw^^j *> r.
Proof. induction j as [|j IH]; cbn [repeat renc lpow]; [reflexivity|]. rewrite IH, Str_app_assoc. reflexivity. Qed.

Lemma decomp T : exists j rest, T = repeat tX j ++ rest /\ (rest = [] \/ exists T', rest = tS :: T').
Proof.
  induction T as [|[] T IH].
  - exists O, (@nil tt). auto.
  - destruct IH as (j & rest & -> & H). exists (S j), rest. auto.
  - exists O, (tS :: T). eauto.
Qed.

Lemma rmS_spec T T1 : rmS T = Some T1 ->
  exists j T', T = repeat tX j ++ tS :: T' /\ T1 = repeat tX j ++ T'.
Proof.
  revert T1; induction T as [|[] T IH]; intros T1 H; cbn in H; try discriminate.
  - destruct (rmS T) as [T2|] eqn:E; [|discriminate]. injection H as <-.
    destruct (IH T2 eq_refl) as (j & T' & -> & ->). exists (S j), T'. auto.
  - injection H as <-. exists O, T. auto.
Qed.

Lemma notin_rep j U : ~ (repeat tX j = U ++ [tS]).
Proof.
  intros H. assert (Hin : In tS (repeat tX j)) by (rewrite H; apply in_or_app; right; left; reflexivity).
  apply repeat_spec in Hin. discriminate.
Qed.

Lemma split_end j : forall T' V, repeat tX j ++ T' = V ++ [tS] ->
  exists U, T' = U ++ [tS] /\ V = repeat tX j ++ U.
Proof.
  intros T' V H.
  destruct (rev T') as [|x Rv] eqn:ER;
    apply (f_equal (@rev tt)) in ER; rewrite rev_involutive in ER; cbn in ER; subst T'.
  - rewrite app_nil_r in H. exfalso. exact (notin_rep j V H).
  - rewrite app_assoc in H. apply app_inj_tail in H. destruct H as [HV Hx]. subst x.
    exists (rev Rv). split; [reflexivity | symmetry; exact HV].
Qed.

(* ===================================================================== *)
(* Section 3. Soundness: every defined sweep is a run of the machine.    *)
(* ===================================================================== *)

(* The A-pass (RA1, RA3): 10 A> T 1010 0^inf --> T' s s D> 0^inf, where T' is T with each X
   read as P0.  The E-pass of O2 (RE1, RE2): s 1 E> U s 1010 0^inf --> U' P3 s s s D> 0^inf. *)

Lemma Apass n : forall T l, length T <= n ->
  l <* [0;1] {{A}}> renc T tend -->+ lsd l (map tok_of T ++ [Sw; Sw]) {{D}}> const 0.
Proof.
  induction n as [|n IH]; intros T l Hn;
    destruct (decomp T) as (j & rest & -> & [-> | (T' & ->)]).
  1,3: rewrite !app_nil_r, renc_rep, lsd_app, lsd_map_rep;
       exact (RA3 l j).
  - rewrite length_app in Hn. cbn in Hn. lia.
  - rewrite renc_app, renc_rep. cbn [renc].
    rewrite map_app, <- app_assoc, lsd_app, lsd_map_rep. cbn [map app].
    rewrite lsd_cons.
    eapply progress_trans; [exact (RA1 l j (renc T' tend)) |].
    apply IH. rewrite length_app in Hn. cbn in Hn. lia.
Qed.

Lemma Epass n : forall T l U, length T <= n -> T = U ++ [tS] ->
  l <* [0;0;1] <* [1] {{E}}> renc T tend -->+
  lsd l (map tok_of U ++ [Dg d3; Sw; Sw; Sw]) {{D}}> const 0.
Proof.
  induction n as [|n IH]; intros T l U Hn HT;
    destruct (decomp T) as (j & rest & -> & [-> | (T' & ->)]).
  1,3: rewrite app_nil_r in HT; exfalso; exact (notin_rep j U HT).
  - rewrite length_app in Hn. cbn in Hn. lia.
  - rewrite renc_app, renc_rep. cbn [renc].
    eapply progress_trans; [exact (RE1 l j (renc T' tend)) |].
    assert (HT2 : (repeat tX j ++ [tS]) ++ T' = U ++ [tS]) by (rewrite <- app_assoc; exact HT).
    destruct (rev T') as [|x Rv] eqn:ER;
      apply (f_equal (@rev tt)) in ER; rewrite rev_involutive in ER; cbn in ER; subst T'.
    + rewrite app_nil_r in HT2. apply app_inj_tail in HT2. destruct HT2 as [HU _]. subst U.
      cbn [renc]. rewrite lsd_app, lsd_map_rep. exact (RE2 (l <* [0;0;1;1;0;0;1;1]^^j)).
    + rewrite app_assoc in HT2. apply app_inj_tail in HT2. destruct HT2 as [HU Hx]. subst x U.
      rewrite !map_app, <- !app_assoc, lsd_app, lsd_map_rep. cbn [map app]. rewrite lsd_cons.
      apply IH; [| reflexivity].
      clear - Hn. rewrite !length_app in Hn. cbn [length] in Hn. rewrite length_app in Hn.
      rewrite length_app. cbn [length] in Hn |- *. lia.
Qed.

(* The left pass, the turn and the right pass (write-up 4.1-4.3). *)

Lemma lsd_snoc l a t : lsd l (a ++ [t]) = lsd l a <* rtw t.
Proof. rewrite lsd_app. reflexivity. Qed.

Lemma lpass_sound : forall Lr T w w' ts', lpass w Lr T = Some (w', ts') ->
  lsd (base w) (rev Lr) <{{B}} renc T tend -->+ K w' ts'.
Proof.
  induction Lr as [|[[] | ] Lr IH]; intros T w w' ts' H; cbn [lpass] in H.
  - destruct w.
    + (* O1: the wall is erased *)
      injection H as <- <-.
      eapply progress_trans; [exact (L6 (renc T tend)) |].
      exact (Apass (length T) T (const 0) (le_n _)).
    + (* O2: a wall and a new digit 3 *)
      destruct (rmS T) as [T1|] eqn:E; [|discriminate].
      destruct (rev T1) as [|[] Rv] eqn:ER; try discriminate. injection H as <- <-.
      destruct (rmS_spec _ _ E) as (j & T' & -> & ->).
      apply (f_equal (@rev tt)) in ER. rewrite rev_involutive in ER. cbn in ER.
      destruct (split_end j T' (rev Rv) ER) as (U & -> & HU).
      rewrite renc_app, renc_rep. cbn [renc].
      eapply progress_trans; [exact (L7 j (renc (U ++ [tS]) tend)) |].
      rewrite HU. unfold K. cbn [base]. rewrite map_app, <- app_assoc, lsd_app, lsd_map_rep.
      apply (Epass (length (U ++ [tS]))); [lia | reflexivity].
  - (* stop at phase 0 *)
    injection H as <- <-. cbn [rev]. rewrite lsd_snoc.
    eapply progress_trans; [exact (L3 (lsd (base w) (rev Lr)) (renc T tend)) |].
    unfold K. rewrite lsd_app, lsd_cons.
    exact (Apass (length T) T _ (le_n _)).
  - (* stop at phase 1 *)
    destruct (rmS T) as [T1|] eqn:E; [|discriminate]. injection H as <- <-.
    destruct (rmS_spec _ _ E) as (j & T' & -> & ->).
    cbn [rev]. rewrite lsd_snoc. unfold K. rewrite lsd_app, lsd_cons.
    destruct (decomp T') as (i & rest & -> & [-> | (T'' & ->)]).
    + rewrite !app_nil_r, renc_app, renc_rep. cbn [renc]. rewrite renc_rep.
      rewrite <- repeat_app, lsd_app, lsd_map_rep, Nat.add_comm.
      exact (L5e (lsd (base w) (rev Lr)) j i).
    + rewrite renc_app, renc_rep. cbn [renc]. rewrite renc_app, renc_rep. cbn [renc].
      rewrite app_assoc, <- repeat_app, map_app, <- app_assoc, lsd_app, lsd_map_rep.
      cbn [map app]. rewrite lsd_cons, (Nat.add_comm j i).
      eapply progress_trans; [exact (L5 (lsd (base w) (rev Lr)) j i (renc T'' tend)) |].
      exact (Apass (length T'') T'' _ (le_n _)).
  - (* stop at phase 2 *)
    injection H as <- <-. cbn [rev]. rewrite lsd_snoc.
    eapply progress_trans; [exact (L4 (lsd (base w) (rev Lr)) (renc T tend)) |].
    unfold K. rewrite lsd_app, lsd_cons.
    exact (Apass (length T) T _ (le_n _)).
  - (* a digit 3 wraps *)
    destruct (rmS T) as [T1|] eqn:E; [|discriminate].
    destruct (rmS_spec _ _ E) as (j & T' & -> & ->).
    cbn [rev]. rewrite lsd_snoc, renc_app, renc_rep. cbn [renc].
    eapply progress_trans; [exact (L2 (lsd (base w) (rev Lr)) j (renc T' tend)) |].
    specialize (IH _ _ _ _ H). cbn [renc] in IH. rewrite renc_app, renc_rep in IH. exact IH.
  - (* a sea word *)
    cbn [rev]. rewrite lsd_snoc.
    eapply progress_trans; [exact (L1 (lsd (base w) (rev Lr)) (renc T tend)) |].
    exact (IH _ _ _ _ H).
Qed.

Lemma sweep_sound w ts w' ts' : (exists u, ts = u ++ [Sw]) -> sweep w ts = Some (w', ts') ->
  K w ts -->+ K w' ts'.
Proof.
  intros [u ->] H. unfold sweep in H. apply lpass_sound in H. rewrite rev_involutive, lsd_snoc in H.
  unfold K at 1. rewrite lsd_snoc.
  eapply progress_trans; [exact (S0 (lsd (base w) u)) | exact H].
Qed.

(* ===================================================================== *)
(* Section 4. The invariant.                                              *)
(* JL Lr n reads the words nearest first, with n = (sea words) - (digits *)
(* 1 and 3) of the part already read; each digit needs n >= 2 after it,  *)
(* and so does the whole list.  cS counts the s in a processed tail.     *)
(* ===================================================================== *)

Open Scope nat_scope.

Definition odd (d : dg) : nat := match d with d1 | d3 => 1 | _ => 0 end.

Fixpoint JL (Lr : list tok) (n : nat) : Prop :=
  match Lr with
  | [] => 2 <= n
  | Sw :: Lr' => JL Lr' (S n)
  | Dg d :: Lr' => odd d + 2 <= n /\ JL Lr' (n - odd d)
  end.

Fixpoint cS (T : list tt) : nat :=
  match T with [] => 0 | tS :: T' => S (cS T') | tX :: T' => cS T' end.

Lemma JL_mono Lr : forall n m, n <= m -> JL Lr n -> JL Lr m.
Proof.
  induction Lr as [|[d|] Lr IH]; cbn [JL]; intros n m Hnm H.
  - lia.
  - destruct H as [H1 H2]. split; [lia|]. apply (IH (n - odd d)); [lia | exact H2].
  - apply (IH (S n)); [lia | exact H].
Qed.

Lemma cS_app a b : cS (a ++ b) = cS a + cS b.
Proof. induction a as [|[] a IH]; cbn [app cS]; lia. Qed.

Lemma cS_rev T : cS (rev T) = cS T.
Proof. induction T as [|[] T IH]; cbn [rev]; rewrite ?cS_app; cbn [cS]; lia. Qed.

Lemma JL_map V : forall n Lr, 2 <= n -> JL Lr (n + cS V) -> JL (map tok_of V ++ Lr) n.
Proof.
  induction V as [|[] V IH]; cbn [map app cS JL tok_of odd]; intros n Lr Hn H.
  - rewrite Nat.add_0_r in H. exact H.
  - split; [lia|]. rewrite Nat.sub_0_r. apply IH; assumption.
  - apply IH; [lia|]. rewrite Nat.add_succ_r in H. exact H.
Qed.

Lemma JL_out Lr d T : odd d + 2 <= 2 + cS T -> JL Lr (2 + cS T - odd d) ->
  JL (rev (rev Lr ++ Dg d :: map tok_of T ++ [Sw; Sw])) 0.
Proof.
  intros H1 H2.
  rewrite rev_app_distr, rev_involutive. cbn [rev]. rewrite rev_app_distr. cbn [rev app].
  rewrite <- map_rev, <- !app_assoc. cbn [app JL].
  apply JL_map; [lia|]. rewrite cS_rev. cbn [JL]. split; [lia | exact H2].
Qed.

Lemma rmS_cS T T1 : rmS T = Some T1 -> cS T = S (cS T1).
Proof.
  intros H. destruct (rmS_spec _ _ H) as (j & T' & -> & ->). rewrite !cS_app. cbn [cS]. lia.
Qed.

Lemma rmS_some T : 1 <= cS T -> exists T1, rmS T = Some T1.
Proof.
  induction T as [|[] T IH]; cbn [cS rmS]; intros H; [lia | | eauto].
  destruct (IH H) as (T1 & ->). eauto.
Qed.

Lemma rmS_snoc U : 1 <= cS U -> exists U1, rmS U = Some U1 /\ rmS (U ++ [tS]) = Some (U1 ++ [tS]).
Proof.
  induction U as [|[] U IH]; cbn [cS rmS app]; intros H; [lia | | eauto].
  destruct (IH H) as (U1 & -> & ->). eauto.
Qed.

Definition Eend (T : list tt) := T = [] \/ exists U, T = U ++ [tS].

Lemma lpass_inv : forall Lr T w, JL Lr (cS T) -> Eend T ->
  exists w' ts', lpass w Lr T = Some (w', ts') /\ JL (rev ts') 0.
Proof.
  induction Lr as [|[[] | ] Lr IH]; intros T w HJ HE; cbn [JL odd] in HJ; cbn [lpass].
  - destruct w.
    + eexists _, _. split; [reflexivity|].
      rewrite rev_app_distr. cbn [rev app]. rewrite <- map_rev, <- (app_nil_r (map tok_of (rev T))).
      cbn [JL]. apply JL_map; [lia|]. cbn [JL]. rewrite cS_rev. lia.
    + destruct HE as [-> | (U & ->)]; [cbn [cS] in HJ; lia|].
      rewrite cS_app in HJ. cbn [cS] in HJ.
      destruct (rmS_snoc U) as (U1 & _ & ->); [lia|].
      rewrite rev_app_distr. cbn [rev app].
      eexists _, _. split; [reflexivity|].
      rewrite rev_involutive, rev_app_distr. cbn [rev app].
      rewrite <- map_rev, <- (app_nil_r (map tok_of (rev U1))).
      cbn [JL odd]. split; [lia|]. apply JL_map; [lia|]. cbn [JL]. lia.
  - eexists _, _. split; [reflexivity|].
    apply JL_out; cbn [odd]; [lia|]. apply (JL_mono _ (cS T - 0)); [lia | tauto].
  - destruct (rmS_some T) as (T1 & E); [lia|]. rewrite E. pose proof (rmS_cS _ _ E) as HC.
    eexists _, _. split; [reflexivity|].
    apply JL_out; cbn [odd]; [lia|]. apply (JL_mono _ (cS T - 1)); [lia | tauto].
  - eexists _, _. split; [reflexivity|].
    apply JL_out; cbn [odd]; [lia|]. apply (JL_mono _ (cS T - 0)); [lia | tauto].
  - destruct HE as [-> | (U & ->)]; [cbn [cS] in HJ; lia|].
    rewrite cS_app in HJ. cbn [cS] in HJ.
    destruct (rmS_snoc U) as (U1 & HU & ->); [lia|]. pose proof (rmS_cS _ _ HU) as HC.
    apply IH.
    + cbn [cS]. rewrite cS_app. cbn [cS]. apply (JL_mono _ (cS U + 1 - 1)); [lia | tauto].
    + right. exists (tX :: U1). reflexivity.
  - apply IH; [exact HJ|].
    destruct HE as [-> | (U & ->)]; right; [exists (@nil tt); reflexivity | exists (tS :: U); reflexivity].
Qed.

Lemma JL_ends ts : JL (rev ts) 0 -> exists u, ts = u ++ [Sw].
Proof.
  intros H. destruct (rev ts) as [|[d|] Lr] eqn:E; cbn [JL] in H; [lia | destruct H; lia |].
  exists (rev Lr). apply (f_equal (@rev tok)) in E. rewrite rev_involutive in E. exact E.
Qed.

Lemma step_ok w ts : JL (rev ts) 0 -> exists w' ts', K w ts -->+ K w' ts' /\ JL (rev ts') 0.
Proof.
  intros HJ.
  destruct (lpass_inv (rev ts) [] w HJ (or_introl eq_refl)) as (w' & ts' & H & HI).
  exists w', ts'. split; [| exact HI].
  apply sweep_sound; [apply JL_ends; exact HJ | exact H].
Qed.

(* ===================================================================== *)
(* Section 5. The start and nonhalt.                                     *)
(* ===================================================================== *)

(* 108 steps: c0 --> 0^inf 110000 100 100 100 D> 0^inf (P1 s s s, no wall). *)
Lemma init : c0 -->* K false [Dg d1; Sw; Sw; Sw].
Proof. unfold K, lsd, base. cbn. solve_init. Qed.

Lemma nonhalt : ~ halts tm c0.
Proof.
  eapply multistep_nonhalt; [exact init|].
  apply (progress_nonhalt_cond tm (bool * list tok) (false, [Dg d1; Sw; Sw; Sw])
           (fun i => K (fst i) (snd i)) (fun i => JL (rev (snd i)) 0)).
  - intros [w ts] HI. destruct (step_ok w ts HI) as (w' & ts' & H1 & H2).
    exists (w', ts'). split; [exact H1 | exact H2].
  - cbn. lia.
Qed.

(*
      0     1
 A   1RB   0RD
 B   0LC   0RA
 C   1LA   1LC
 D   1RE   0LF
 E   0RA   1RF
 F   1LB   ---

 words      s = 100, P0 = 11001100, P1 = 110000, P2 = 1001100, P3 = 10000, wall 1100;
            X = 10101010 (a digit 3 that has wrapped and eaten one s, during a sweep)
 D-record   K(w, ts) = 0^inf [1100 if w] ts D> 0^inf, ts a list of digit words and s

 S0   s D> 0^inf                    --> s <B 1010 0^inf                 9
 L1   s <B                          --> <B s                            5
 L2   P3 <B X^j s                   --> <B X^(j+1)                      19 + 20j
 L3   P0 <B                         --> P1 10 A>                        9
 L4   P2 <B                         --> P3 10 A>                        9
 L5   P1 <B X^j s X^i s             --> P2 P0^(i+j) s 10 A>             59 + 56j + 36i
 L5e  P1 <B X^j s X^i 1010 0^inf    --> P2 P0^(i+j) s s D> 0^inf        62 + 56j + 36i
 L6   0^inf 1100 <B                 --> 0^inf 10 A>                     9
 L7   0^inf <B X^j s                --> 0^inf 1100 P0^j s 1 E>          38 + 56j
 RA1  10 A> X^j s                   --> P0^j s 10 A>                    3 + 36j
 RA3  10 A> X^j 1010 0^inf          --> P0^j s s D> 0^inf               6 + 36j
 RE1  s 1 E> X^j s                  --> P0^j s s 1 E>                   5 + 36j
 RE2  s s 1 E> 1010 0^inf           --> P3 s s s D> 0^inf               49

 sweep      left pass from the right end: s moves into the tail; P3 wraps and eats the
            first s of the tail; P0 and P2 step up; P1 steps up and eats the first s of
            the tail.  At the left end: O1 (wall erased) or O2 (wall built; the tail loses
            its first and its last s, and P3 s s s is appended).
 invariant  every suffix of ts that starts with a digit, and ts itself:
            #s >= #(P1, P3) + 2
 start      c0 -->(108) K(no wall, P1 s s s)
*)