(* 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF never halts.
   Recursive run-length counter (sheet class Counter Class 4). The tape is a stack of runs of
   1s, conf L R. A big-step frame semantics Life x R o (a frame of value x on top, right word R)
   is lifted to the TM by Life_tm, through push/pop rules that are instances of tR1/tR2/tR3
   (each one plain es). An edge epoch Ep W c W' is the life of the edge frame (value 4). On a
   T-word it replays the orbit of its own marker tail (replay, ruleT, ruleX); translation (TL)
   is the monotonicity lemma Life_shape. The absorption law and the orbit invariant Inv of
   proof.md section 3, with marker words given by their absorption indices, are proved by
   induction on n + #markers (main). The top level is the marker-free orbit, whose epochs all
   cost 2, so the edge frame never runs out of budget.
   Informal proof: the accompanying write-up (proof.md).
   Formalized with Claude Code (AI-assisted).
   Checked: compiles against unmodified busycoq (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.

Definition tm := Eval compute in (TM_from_str "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF").

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.

(* R1: l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r --> l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r *)
Lemma tR1 n m x l r :
  l <* [1]^^(S (S n)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> [1]^^x *> [0] *> r -->+
  l <* [1]^^(S n) <* [0] <* [1]^^(S m) <{{A}} [0] *> [1]^^(S x) *> [0;0] *> r.
Proof. es. Qed.

(* R3: l 0 <A 0 1^(k+1) 0 0 1^m 0 r --> l 1^(k+2) <A 0 1^(m+1) 0 0 r *)
Lemma tR3 k m l r :
  l <* [0] <{{A}} [0] *> [1]^^(S k) *> [0;0] *> [1]^^m *> [0] *> r -->+
  l <* [1]^^(S (S k)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> r.
Proof. es. Qed.

(* R2: l 0 1^(k+1) 0 1 <A 0 r --> l <A 0 1^(k+2) 0 0 r *)
Lemma tR2 k l r :
  l <* [0] <* [1]^^(S k) <* [0] <* [1] <{{A}} [0] *> r -->+
  l <{{A}} [0] *> [1]^^(S (S k)) *> [0;0] *> r.
Proof. es. Qed.

Lemma tR3c k m r :
  const 0 <{{A}} [0] *> [1]^^(S k) *> [0;0] *> [1]^^m *> [0] *> r -->+
  const 0 <* [1]^^(S (S k)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> r.
Proof. rewrite (const_unfold _ S0) at 1. es. Qed.

(* ---------- tape encoding of the run model ---------- *)
Fixpoint lsep (L : list nat) : side :=
  match L with
  | [] => const 0
  | y :: L' => lsep L' <* [1]^^y <* [0]
  end.

Definition lside (L : list nat) : side :=
  match L with
  | [] => const 0
  | x :: L' => lsep L' <* [1]^^x
  end.

Fixpoint rside (R : list nat) : side :=
  match R with
  | [] => const 0
  | [c] => [1]^^c *> const 0
  | c :: g :: R' => [1]^^c *> [0]^^g *> rside R'
  end.

Definition conf (L R : list nat) : Q * tape := lside L <{{A}} [0] *> rside R.

Lemma c0_1 : 0 >> const 0 = const 0.
Proof. symmetry. apply const_unfold. Qed.

Lemma lsep_eq L : lsep L = lside L <* [0].
Proof. destruct L; cbn; [apply const_unfold | reflexivity]. Qed.

Open Scope nat_scope.

(* ---------- the run model ---------- *)
(* A push reads the right word h :: R': it creates a child frame of value h and
   the word right of the head becomes [updt R'] (proof.md Lemma RM). *)
Definition updt (R' : list nat) : option (list nat) :=
  match R' with
  | [] => Some [1]
  | g :: R'' =>
    match g with
    | 0 | 1 => None
    | 2 => match R'' with
           | [] => None
           | c2 :: R3 => match R3 with
                         | [] => Some [S c2]
                         | 0 :: _ => None
                         | S g2 :: rest => Some (S c2 :: S (S g2) :: rest)
                         end
           end
    | S (S (S g')) => Some (1 :: S (S g') :: R'')
    end
  end.

Lemma updt_shape m R' R1 : updt R' = Some R1 ->
  exists x r, rside (S m :: R') = [S1]^^(S m) *> [S0;S0] *> [S1]^^x *> [S0] *> r /\
              rside R1 = [S1]^^(S x) *> [S0;S0] *> r.
Proof.
  intros H. destruct R' as [|g R'']; cbn in H.
  - inversion H; subst. exists 0, (const S0). cbn. rewrite !c0_1. split; reflexivity.
  - destruct g as [|[|[|g']]]; try discriminate.
    + destruct R'' as [|c2 R3]; try discriminate.
      destruct R3 as [|[|g2] rest]; try discriminate; inversion H; subst.
      * exists c2, (const S0). cbn. rewrite !c0_1. split; reflexivity.
      * exists c2, ([S0]^^g2 *> rside rest). cbn. split; reflexivity.
    + inversion H; subst. exists 0, ([S0]^^g' *> rside R''). cbn. split; reflexivity.
Qed.

Lemma push_ok y h R' R1 L : updt R' = Some R1 -> 1 <= y -> 1 <= h ->
  conf (S y :: L) (h :: R') -->+ conf (h :: y :: L) R1.
Proof.
  intros Hu Hy Hh. destruct y as [|n]; [lia|]. destruct h as [|m]; [lia|].
  destruct (updt_shape m R' R1 Hu) as (x & r & E1 & E2).
  unfold conf. change (lside (S (S n) :: L)) with (lsep L <* [S1]^^(S (S n))).
  change (lside (S m :: S n :: L)) with (lsep L <* [S1]^^(S n) <* [S0] <* [S1]^^(S m)).
  rewrite E1, E2. apply tR1.
Qed.

Lemma push0_ok h R' R1 : updt R' = Some R1 -> 1 <= h ->
  conf [] (h :: R') -->+ conf [S h] R1.
Proof.
  intros Hu Hh. destruct h as [|m]; [lia|].
  destruct (updt_shape m R' R1 Hu) as (x & r & E1 & E2).
  unfold conf. change (lside []) with (const S0).
  change (lside [S (S m)]) with (const S0 <* [S1]^^(S (S m))).
  rewrite E1, E2. apply tR3c.
Qed.

Lemma pop_ok y L R : 1 <= y -> conf (1 :: y :: L) R -->+ conf L (S y :: 2 :: R).
Proof.
  intros Hy. destruct y as [|k]; [lia|].
  unfold conf. change (lside (1 :: S k :: L)) with (lsep L <* [S1]^^(S k) <* [S0] <* [S1]^^1).
  rewrite lsep_eq.
  change (rside (S (S k) :: 2 :: R)) with ([S1]^^(S (S k)) *> [S0;S0] *> rside R).
  apply tR2.
Qed.

(* ---------- frame semantics ---------- *)
Inductive outcome := Fin (R : list nat) | Pop (c : nat) (R : list nat).

(* Life x R o: a frame of value x is on top with right word R.
   Fin R'  : it comes back on top with value 1 (it finishes; its parent is popped next);
   Pop c R': it created c children, and its last child finished, which popped it;
             R' is the right word after that pop (it starts with its value+1, then 2). *)
Inductive Life : nat -> list nat -> outcome -> Prop :=
| L_fin R : Life 1 R (Fin R)
| L_cf y h R' R1 Rc : 1 <= y -> updt R' = Some R1 -> Life h R1 (Fin Rc) ->
    Life (S y) (h :: R') (Pop 1 (S y :: 2 :: Rc))
| L_cpf y h R' R1 c' R2 Rf : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) ->
    Life y R2 (Fin Rf) -> Life (S y) (h :: R') (Fin Rf)
| L_cpp y h R' R1 c' R2 c Rf : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) ->
    Life y R2 (Pop c Rf) -> Life (S y) (h :: R') (Pop (S c) Rf).

Lemma Life_pos x R o : Life x R o -> 1 <= x.
Proof. destruct 1; lia. Qed.

Lemma Life_tm x R o : Life x R o -> forall L,
  match o with
  | Fin Rf => conf (x :: L) R -->* conf (1 :: L) Rf
  | Pop _ Rf => conf (x :: L) R -->+ conf L Rf
  end.
Proof.
  induction 1 as [R|y h R' R1 Rc Hy Hu H1 IH1|y h R' R1 c' R2 Rf Hy Hu H1 IH1 H2 IH2
                 |y h R' R1 c' R2 c Rf Hy Hu H1 IH1 H2 IH2]; intros L.
  - apply evstep_refl.
  - eapply progress_trans. { apply push_ok; eauto using Life_pos. }
    eapply evstep_progress_trans. { apply (IH1 (y :: L)). }
    apply pop_ok; lia.
  - apply progress_evstep. eapply progress_trans. { apply push_ok; eauto using Life_pos. }
    eapply progress_evstep_trans. { apply (IH1 (y :: L)). }
    apply IH2.
  - eapply progress_trans. { apply push_ok; eauto using Life_pos. }
    eapply progress_trans. { apply (IH1 (y :: L)). }
    apply IH2.
Qed.

(* ---------- epochs ---------- *)
(* Ep W c W': from Edge(W) = conf [] (3::2::W) the edge frame (value 4) creates c
   children and the epoch ends at conf [] ((5-c)::2::W'). *)
Definition Ep (W : list nat) (c : nat) (W' : list nat) : Prop :=
  exists R0, updt (2 :: W) = Some R0 /\ Life 4 R0 (Pop c ((5 - c) :: 2 :: W')).

Lemma Ep_tm W c W' : Ep W c W' -> conf [] (3 :: 2 :: W) -->+ conf [] ((5 - c) :: 2 :: W').
Proof.
  intros (R0 & Hu & HL).
  eapply progress_trans. { apply push0_ok; [exact Hu | lia]. }
  exact (Life_tm _ _ _ HL []).
Qed.

Lemma Life_shape x R o : Life x R o -> forall c Rf, o = Pop c Rf ->
  exists W', Rf = (x - c + 1) :: 2 :: W' /\ c + 1 <= x /\
    forall z, c + 1 <= z -> Life z R (Pop c ((z - c + 1) :: 2 :: W')).
Proof.
  induction 1 as [R|y h R' R1 Rc Hy Hu H1 IH1|y h R' R1 c' R2 Rf Hy Hu H1 IH1 H2 IH2
                 |y h R' R1 c' R2 c Rf Hy Hu H1 IH1 H2 IH2]; intros c0 Rf0 E; try discriminate.
  - inversion E; subst. exists Rc. split; [f_equal; lia|]. split; [lia|].
    intros z Hz. destruct z as [|z]; [lia|].
    replace (S z - 1 + 1) with (S z) by lia. eapply L_cf; eauto; lia.
  - inversion E; subst. destruct (IH2 c Rf0 eq_refl) as (W' & -> & Hc & Hm).
    exists W'. split; [f_equal; lia|]. split; [lia|].
    intros z Hz. destruct z as [|z]; [lia|].
    replace (S z - S c + 1) with (z - c + 1) by lia. eapply L_cpp; eauto; [lia | apply Hm; lia].
Qed.

Definition bump (o : outcome) : outcome :=
  match o with Fin W => Fin W | Pop c W => Pop (S c) W end.

Lemma L_cp y h R' R1 c' R2 o : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) ->
  Life y R2 o -> Life (S y) (h :: R') (bump o).
Proof. intros. destruct o; cbn; [eapply L_cpf | eapply L_cpp]; eauto. Qed.

Lemma updt_cons2 W R0 : updt (2 :: W) = Some R0 -> exists c2 W1, W = c2 :: W1.
Proof. destruct W; cbn; [discriminate | eauto]. Qed.

(* one child of a replay frame: the child runs a translated epoch (proof.md TL) *)
Lemma frame_step y z W c W' o y' z' : Ep W c W' -> 2 <= y -> c + 1 <= z ->
  y' = y - 1 -> z' = z - c + 1 ->
  Life y' (z' :: 2 :: W') o -> Life y (z :: 2 :: W) (bump o).
Proof.
  intros (R0 & Hu & HL) Hy Hz -> -> H.
  destruct (Life_shape _ _ _ HL c _ eq_refl) as (W'' & E & Hc & Hm).
  injection E as E. subst W''.
  destruct y as [|y]; [lia|].
  eapply L_cp; [lia | exact Hu | apply Hm; exact Hz | ].
  replace y with (S y - 1) by lia. exact H.
Qed.

(* ---------- concrete epoch rules (proof.md section 2) ---------- *)
Ltac lf :=
  first
  [ eassumption
  | apply L_fin
  | eapply L_cf; [lia | reflexivity | lf]
  | eapply L_cpf; [lia | reflexivity | lf | lf]
  | eapply L_cpp; [lia | reflexivity | lf | lf] ].

Ltac ep := eexists; split; [reflexivity | lf].

Definition tail_ok (N : list nat) : Prop := N = [] \/ exists g rest, N = S (S g) :: rest.

Lemma U0 : Ep [1] 2 [2;2;1].
Proof. ep. Qed.

Lemma U1 g rest : Ep (1 :: S (S (S (S g))) :: rest) 2 (2 :: 2 :: 1 :: S (S g) :: rest).
Proof. ep. Qed.

Lemma U2 b N : tail_ok N -> Ep (1 :: 2 :: S b :: N) 2 (S (S (S b)) :: 2 :: 1 :: N).
Proof. intros [-> | (g & rest & ->)]; ep. Qed.

Lemma ruleS a b N : tail_ok N ->
  Ep (2 :: 2 :: S a :: 2 :: S b :: N) 2 (S (S a) :: 2 :: S (S (S b)) :: 2 :: 1 :: N).
Proof. intros [-> | (g & rest & ->)]; ep. Qed.

Lemma TRF a b N Rc : tail_ok N -> 2 <= a ->
  Life a (S (S (S b)) :: 2 :: 1 :: N) (Fin Rc) -> Ep (a :: 2 :: S b :: N) 2 Rc.
Proof. intros [-> | (g & rest & ->)] Ha H; ep. Qed.

Lemma Xin0 a'' b'' : 1 <= a'' ->
  Life 2 [2; 2; a''; 2; b''] (Pop 1 [2; 2; S a''; 2; S b'']).
Proof. intros. lf. Qed.

Lemma Xin1 a'' b'' g rest : 1 <= a'' ->
  Life 2 (2 :: 2 :: a'' :: 2 :: b'' :: S g :: rest) (Pop 1 (2 :: 2 :: S a'' :: 2 :: S b'' :: S (S g) :: rest)).
Proof. intros. lf. Qed.

Lemma TRX0 a b N c a'' b'' : tail_ok N -> 2 <= a ->
  Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c [2; 2; S a''; 2; S b'']) ->
  Ep (a :: 2 :: S b :: N) 3 [S (S a''); 2; S (S b'')].
Proof. intros [-> | (g & rest & ->)] Ha H; ep. Qed.

Lemma TRX1 a b N c a'' b'' g rest : tail_ok N -> 2 <= a ->
  Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c (2 :: 2 :: S a'' :: 2 :: S b'' :: S g :: rest)) ->
  Ep (a :: 2 :: S b :: N) 3 (S (S a'') :: 2 :: S (S b'') :: S (S g) :: rest).
Proof. intros [-> | (g' & rest' & ->)] Ha H; ep. Qed.

(* ---------- marker words, orbits, replay ---------- *)
(* A marker word is given by its absorption indices P = [I_1; ...; I_m] (proof.md section 0):
   gaps g_j = I_j - I_(j-1) + 1, each followed by a lone 1. *)
Fixpoint mwf (s : nat) (P : list nat) : list nat :=
  match P with
  | [] => []
  | p :: P' => (p - s + 1) :: 1 :: mwf p P'
  end.
Definition mw (P : list nat) : list nat := mwf 0 P.

(* even gaps: each index is odd above the previous one *)
Fixpoint valid_from (s : nat) (P : list nat) : Prop :=
  match P with
  | [] => True
  | p :: P' => (exists t, p = s + 2 * t + 1) /\ valid_from p P'
  end.
Definition valid (P : list nat) : Prop := valid_from 0 P.

Definition cnt (Q : list nat) (n : nat) : nat := length (filter (fun q => q <? n) Q).
Definition ind (Q : list nat) (n : nat) : nat := cnt Q (S n) - cnt Q n.
Definition cost (Q : list nat) (n : nat) : nat := 2 + ind Q n.

Inductive Orb (Q : list nat) : nat -> list nat -> Prop :=
| O0 : Orb Q 0 (1 :: mw Q)
| OS n W W' : Orb Q n W -> Ep W (cost Q n) W' -> Orb Q (S n) W'.

Fixpoint bumpn (k : nat) (o : outcome) : outcome :=
  match k with 0 => o | S k => bumpn k (bump o) end.

Lemma bumpn_fin k W : bumpn k (Fin W) = Fin W.
Proof. induction k; cbn; auto. Qed.

Lemma bumpn_pop k c W : bumpn k (Pop c W) = Pop (k + c) W.
Proof. revert c. induction k; intros c; cbn; [reflexivity|]. rewrite IHk. f_equal. lia. Qed.

Lemma cnt_0 Q : cnt Q 0 = 0.
Proof. unfold cnt. induction Q; cbn [filter length]; auto. Qed.

Lemma cnt_mono Q n : cnt Q n <= cnt Q (S n).
Proof.
  unfold cnt. induction Q as [|q Q IH]; cbn [filter length]; [lia|].
  destruct (Nat.ltb_spec q n), (Nat.ltb_spec q (S n)); cbn [length]; lia.
Qed.

Lemma cnt_mono' Q n m : n <= m -> cnt Q n <= cnt Q m.
Proof. induction 1; [lia|]. pose proof (cnt_mono Q m). lia. Qed.

Lemma replay Q k Wk : Orb Q k Wk -> forall y z o, k + 1 <= y -> (k = 0 \/ k + 2 + cnt Q k <= z) ->
  Life (y - k) ((z - k - cnt Q k) :: 2 :: Wk) o -> Life y (z :: 2 :: 1 :: mw Q) (bumpn k o).
Proof.
  induction 1 as [|n W W' HO IH HE]; intros y z o Hy Hz H.
  - cbn in *. rewrite cnt_0, !Nat.sub_0_r in H. exact H.
  - cbn [bumpn]. pose proof (cnt_mono Q n) as Hm. unfold cost, ind in HE.
    apply IH; [lia | right; lia | ].
    eapply frame_step; [exact HE | lia | lia | | | exact H]; lia.
Qed.

Lemma mw_tail_ok Q : valid Q -> tail_ok (mw Q).
Proof.
  destruct Q as [|q Q]; [left; reflexivity|].
  intros [[t Ht] _]. right. exists (q - 1), (1 :: mwf q Q). cbn. f_equal. lia.
Qed.

Lemma ruleT a b Q W' : Orb Q (a - 1) W' -> 2 <= a -> 1 <= b -> valid Q ->
  a - 1 + cnt Q (a - 1) <= b ->
  Ep (a :: 2 :: b :: mw Q) 2 ((b + 3 - a - cnt Q (a - 1)) :: 2 :: W').
Proof.
  intros HO Ha Hb HV Hc. destruct b as [|b]; [lia|].
  apply TRF; [apply mw_tail_ok; exact HV | exact Ha | ].
  rewrite <- (bumpn_fin (a - 1)).
  apply (replay Q (a - 1) W' HO); [lia | lia | ].
  replace (a - (a - 1)) with 1 by lia.
  replace (S (S (S b)) - (a - 1) - cnt Q (a - 1)) with (S b + 3 - a - cnt Q (a - 1)) by lia.
  apply L_fin.
Qed.

Lemma mwf_shift s k P : mwf (s + k) (map (fun p => p + k) P) = mwf s P.
Proof.
  revert s. induction P as [|p P IH]; intros s; cbn; [reflexivity|].
  rewrite IH. f_equal. lia.
Qed.

Lemma ruleX a b Q a'' Q'' : Orb Q (a - 2) (a'' :: 2 :: b :: mw Q'') -> 3 <= a -> 1 <= b ->
  1 <= a'' -> valid Q -> valid Q'' -> b = a - 2 + cnt Q (a - 2) ->
  Ep (a :: 2 :: b :: mw Q) 3 (S (S a'') :: 2 :: S (S b) :: mw (map (fun q => q + 2) Q'')).
Proof.
  intros HO Ha Hb Ha'' HV HV'' Hbe. destruct b as [|b0]; [lia|].
  assert (Hz : S (S (S b0)) - (a - 2) - cnt Q (a - 2) = 2) by lia.
  assert (Hy : a - (a - 2) = 2) by lia.
  destruct Q'' as [|q Q2].
  - cbn. eapply TRX0 with (c := a - 2 + 1); [apply mw_tail_ok; exact HV | lia | ].
    rewrite <- bumpn_pop.
    apply (replay Q (a - 2) _ HO); [lia | lia | ].
    rewrite Hz, Hy. apply Xin0. exact Ha''.
  - change (mw (q :: Q2)) with ((q - 0 + 1) :: 1 :: mwf q Q2) in HO.
    replace (q - 0 + 1) with (S q) in HO by lia.
    cbn [mw mwf map]. replace (q + 2 - 0 + 1) with (S (S (S q))) by lia.
    replace (q + 2) with (q + 2) by reflexivity. rewrite mwf_shift.
    eapply TRX1 with (c := a - 2 + 1); [apply mw_tail_ok; exact HV | lia | ].
    rewrite <- bumpn_pop.
    apply (replay Q (a - 2) _ HO); [lia | lia | ].
    rewrite Hz, Hy. apply Xin1. exact Ha''.
Qed.

(* ---------- list lemmas ---------- *)
Lemma valid_gt s P : valid_from s P -> Forall (fun p => s < p) P.
Proof.
  revert s. induction P as [|p P IH]; intros s H; [constructor|].
  destruct H as [[t Ht] HP]. constructor; [lia|].
  specialize (IH p HP). eapply Forall_impl; [|exact IH]. intros x Hx; cbn in *; lia.
Qed.

Lemma cnt_cons_lt q Q n : q < n -> cnt (q :: Q) n = S (cnt Q n).
Proof. intros H. unfold cnt. cbn [filter]. rewrite (proj2 (Nat.ltb_lt q n) H). reflexivity. Qed.

Lemma cnt_cons_ge q Q n : n <= q -> cnt (q :: Q) n = cnt Q n.
Proof. intros H. unfold cnt. cbn [filter]. rewrite (proj2 (Nat.ltb_ge q n) H). reflexivity. Qed.

Lemma cnt_app X Y n : cnt (X ++ Y) n = cnt X n + cnt Y n.
Proof. unfold cnt. rewrite filter_app, length_app. reflexivity. Qed.

Lemma cnt_all_lt X n : Forall (fun q => q < n) X -> cnt X n = length X.
Proof.
  induction 1 as [|q X Hq HX IH]; [reflexivity|].
  rewrite cnt_cons_lt by exact Hq. cbn [length]. lia.
Qed.

Lemma cnt_all_ge X n : Forall (fun q => n <= q) X -> cnt X n = 0.
Proof.
  induction 1 as [|q X Hq HX IH]; [reflexivity|].
  rewrite cnt_cons_ge by exact Hq. exact IH.
Qed.

Lemma cnt_S_nin Q n : ~ In n Q -> cnt Q (S n) = cnt Q n.
Proof.
  induction Q as [|q Q IH]; intros H; [reflexivity|].
  assert (q <> n) by (intro; apply H; left; auto).
  assert (~ In n Q) by (intro; apply H; right; auto).
  destruct (Nat.lt_ge_cases q n).
  - rewrite !cnt_cons_lt by lia. f_equal. auto.
  - rewrite !cnt_cons_ge by lia. auto.
Qed.

Lemma cnt_S_in s Q n : valid_from s Q -> In n Q -> cnt Q (S n) = S (cnt Q n).
Proof.
  revert s. induction Q as [|q Q IH]; intros s HV H; [destruct H|].
  destruct HV as [_ HV]. pose proof (valid_gt _ _ HV) as Hg. rewrite Forall_forall in Hg.
  destruct H as [<- | H].
  - rewrite cnt_cons_lt by lia. rewrite cnt_cons_ge by lia. f_equal. apply cnt_S_nin.
    intro Hin. specialize (Hg _ Hin). lia.
  - pose proof (Hg _ H). rewrite !cnt_cons_lt by lia. f_equal. eapply IH; eauto.
Qed.

Lemma ind_in Q n : valid Q -> In n Q -> ind Q n = 1.
Proof. intros HV H. unfold ind. rewrite (cnt_S_in 0 Q n HV H). lia. Qed.

Lemma ind_nin Q n : ~ In n Q -> ind Q n = 0.
Proof. intros H. unfold ind. rewrite (cnt_S_nin Q n H). lia. Qed.

Lemma ind_iff P Q k k' : valid P -> valid Q -> (In k P <-> In k' Q) -> ind P k = ind Q k'.
Proof.
  intros HP HQ E. destruct (in_dec Nat.eq_dec k P) as [H|H].
  - rewrite (ind_in P k HP H), (ind_in Q k' HQ (proj1 E H)). reflexivity.
  - rewrite (ind_nin P k H), (ind_nin Q k'); [reflexivity|]. intro H'. apply H, E, H'.
Qed.

Lemma parity_in s P n : valid_from s P -> In n P -> exists u, n + cnt P n + s = 2 * u + 1.
Proof.
  revert s. induction P as [|p P IH]; intros s HV H; [destruct H|].
  destruct HV as [[t Ht] HV]. pose proof (valid_gt _ _ HV) as Hg. rewrite Forall_forall in Hg.
  destruct H as [<- | H].
  - rewrite cnt_cons_ge by lia. rewrite cnt_all_ge.
    + exists (s + t). lia.
    + apply Forall_forall. intros x Hx. specialize (Hg _ Hx). lia.
  - pose proof (Hg _ H). rewrite cnt_cons_lt by lia. destruct (IH p HV H) as [u Hu].
    exists (u - t). lia.
Qed.

Lemma filter_lt_app X Y k : Forall (fun q => q <= k) X ->
  filter (fun q => k <? q) (X ++ Y) = filter (fun q => k <? q) Y.
Proof.
  intros H. rewrite filter_app. replace (filter (fun q => k <? q) X) with (@nil nat); [reflexivity|].
  induction H as [|q X Hq HX IH]; cbn [filter]; [reflexivity|].
  rewrite (proj2 (Nat.ltb_ge k q) Hq). exact IH.
Qed.

Lemma filter_filter_lt P k k' : k <= k' ->
  filter (fun p => k' <? p) (filter (fun p => k <? p) P) = filter (fun p => k' <? p) P.
Proof.
  intros Hk. induction P as [|p P IH]; cbn [filter]; [reflexivity|].
  destruct (Nat.ltb_spec k p); cbn [filter]; destruct (Nat.ltb_spec k' p); try lia; rewrite IH; reflexivity.
Qed.

Lemma filter_all P k : Forall (fun p => k < p) P -> filter (fun p => k <? p) P = P.
Proof.
  induction 1 as [|p P Hp HP IH]; cbn [filter]; [reflexivity|].
  rewrite (proj2 (Nat.ltb_lt k p) Hp). rewrite IH. reflexivity.
Qed.

Lemma filter_gt P k p : In p (filter (fun p => k <? p) P) -> k < p.
Proof. intros Hp. apply filter_In in Hp. destruct Hp as [_ Hp]. apply Nat.ltb_lt. exact Hp. Qed.

Lemma filter_in P k p : k < p -> (In p (filter (fun p => k <? p) P) <-> In p P).
Proof.
  intros H. rewrite filter_In. split; [tauto|]. intros Hp. split; [exact Hp | apply Nat.ltb_lt; exact H].
Qed.

Lemma filter_cnt_len P n : length (filter (fun p => n <? p) P) + cnt P (S n) = length P.
Proof.
  induction P as [|p P IH]; [reflexivity|]. cbn [filter length].
  destruct (Nat.ltb_spec n p).
  - rewrite cnt_cons_ge by lia. cbn [length]. lia.
  - rewrite cnt_cons_lt by lia. lia.
Qed.

(* shifted copies of index lists *)
Definition Sh (u v : nat) (Q P : list nat) : Prop := Forall2 (fun q p => q + u = p + v) Q P.

Lemma Sh_len u v Q P : Sh u v Q P -> length Q = length P.
Proof. apply Forall2_length. Qed.

Lemma Sh_eq u v u' v' Q P : Sh u v Q P -> u = u' -> v = v' -> Sh u' v' Q P.
Proof. intros H -> ->. exact H. Qed.

Lemma Sh_filter u v Q P k k' : Sh u v Q P -> k + u = k' + v ->
  Sh u v (filter (fun q => k <? q) Q) (filter (fun p => k' <? p) P).
Proof.
  unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hk; cbn [filter]; [constructor|].
  destruct (Nat.ltb_spec k q), (Nat.ltb_spec k' p); try lia.
  - constructor; auto.
  - auto.
Qed.

Lemma Sh_in u v Q P k k' : Sh u v Q P -> k + u = k' + v -> (In k Q <-> In k' P).
Proof.
  unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hk; cbn [In]; [tauto|].
  specialize (IH Hk). split; (intros [H|H]; [left; lia | right; tauto]).
Qed.

Lemma Sh_trans u1 v1 u2 v2 u v w X Y Z : Sh u1 v1 X Y -> Sh u2 v2 Y Z ->
  u1 + u2 = u + w -> v1 + v2 = v + w -> Sh u v X Z.
Proof.
  unfold Sh. intros H1. revert Z. induction H1 as [|x y X Y Hxy HXY IH]; intros Z H2 E1 E2;
    inversion H2; subst; constructor; [lia | auto].
Qed.

Lemma Sh_map u v d Q P : Sh u v Q P -> Sh u (v + d) (map (fun q => q + d) Q) P.
Proof. unfold Sh. induction 1; cbn [map]; constructor; [lia | auto]. Qed.

Lemma Sh_unmap v k P : Forall (fun p => k <= p) P -> Sh (v + k) v (map (fun p => p - k) P) P.
Proof. unfold Sh. induction 1; cbn [map]; constructor; [lia | auto]. Qed.

Lemma Sh_ge u v Q P k k' : Sh u v Q P -> (forall p, In p P -> k' <= p) -> k + u <= k' + v ->
  Forall (fun q => k <= q) Q.
Proof.
  unfold Sh. induction 1 as [|q p Q P Hqp HQP IH]; intros Hp Hk; constructor.
  - specialize (Hp p (or_introl eq_refl)). lia.
  - apply IH; [intros x Hx; apply Hp; right; exact Hx | exact Hk].
Qed.

Lemma valid_shift s k P : valid_from s P -> valid_from (s + k) (map (fun p => p + k) P).
Proof.
  revert s. induction P as [|p P IH]; intros s H; [exact I|].
  destruct H as [[t Ht] H]. cbn [map valid_from]. split; [exists t; lia | apply IH; exact H].
Qed.

Lemma valid_map2 s P : valid_from s P -> valid_from s (map (fun p => p + 2) P).
Proof.
  destruct P as [|p P]; intros H; [exact I|]. destruct H as [[t Ht] H].
  cbn [map valid_from]. split; [exists (S t); lia | apply valid_shift; exact H].
Qed.

Lemma valid_cons1 Q : valid Q -> valid (1 :: map (fun q => q + 1) Q).
Proof. intros H. cbn [valid valid_from]. split; [exists 0; lia | apply (valid_shift 0 1 Q H)]. Qed.

Lemma valid_unshift s k P : valid_from (s + k) P -> valid_from s (map (fun p => p - k) P).
Proof.
  revert s. induction P as [|p P IH]; intros s H; [exact I|].
  destruct H as [[t Ht] H]. cbn [map valid_from]. split; [exists t; lia|].
  apply IH. replace (p - k + k) with p by lia. exact H.
Qed.

Lemma valid_app_l X Y : valid (X ++ Y) -> Forall (fun q => 1 <= q) X.
Proof.
  intros H. apply valid_gt in H. apply Forall_app in H. destruct H as [H _].
  eapply Forall_impl; [|exact H]. intros; lia.
Qed.

Lemma mwf_unshift s k P : k <= s -> Forall (fun p => k <= p) P ->
  mwf (s - k) (map (fun p => p - k) P) = mwf s P.
Proof.
  intros Hs H. revert s Hs. induction H as [|p P Hp HP IH]; intros s Hs; cbn [map mwf]; [reflexivity|].
  rewrite (IH p Hp). f_equal. lia.
Qed.

Lemma mw_cons1 Q : 2 :: 1 :: mw Q = mw (1 :: map (fun q => q + 1) Q).
Proof. unfold mw. cbn [mwf]. rewrite <- (mwf_shift 0 1 Q). reflexivity. Qed.

Lemma valid_tail_ok s P : valid_from s P -> tail_ok (mwf s P).
Proof.
  destruct P as [|p P]; [left; reflexivity|].
  intros [[t Ht] _]. right. exists (2 * t), (1 :: mwf p P). cbn [mwf]. f_equal. lia.
Qed.

Lemma cnt1_valid P : valid P -> cnt P 1 = 0.
Proof.
  intros H. apply cnt_all_ge. apply valid_gt in H. eapply Forall_impl; [|exact H]. intros; cbn in *; lia.
Qed.

Lemma in_transfer Qi Qe P k k' u v kf : Forall (fun q => q < k) Qi ->
  Sh u v Qe (filter (fun p => kf <? p) P) -> k + u = k' + v -> kf < k' ->
  (In k (Qi ++ Qe) <-> In k' P).
Proof.
  intros HQi Hsh E Hk. rewrite in_app_iff, (Sh_in _ _ _ _ k k' Hsh E), (filter_in P kf k' Hk).
  rewrite Forall_forall in HQi.
  split; [intros [H|H]; [specialize (HQi _ H); lia | exact H] | intros H; right; exact H].
Qed.

Lemma sh_compose Qi Qe Qe' P n a a' k k' : Forall (fun q => q <= k) Qi -> n <= k' ->
  k + (n + 3) = k' + a ->
  Sh (k + 3) a' Qe' (filter (fun q => k <? q) (Qi ++ Qe)) ->
  Sh (n + 3) a Qe (filter (fun p => n <? p) P) ->
  Sh (k' + 3) a' Qe' (filter (fun p => k' <? p) P).
Proof.
  intros HQi Hn E H1 H2. rewrite (filter_lt_app _ _ _ HQi) in H1.
  pose proof (Sh_filter _ _ _ _ k k' H2 E) as H3. rewrite (filter_filter_lt P n k' Hn) in H3.
  apply (Sh_trans _ _ _ _ _ _ a _ _ _ H1 H3); lia.
Qed.

(* ---------- the orbit invariant and the absorption law (proof.md section 3) ---------- *)
(* Core P k a b Q: the marker tail Q of a T(a,b)/S(a,b) word splits into Qi (internal
   markers within reach, plus the one being absorbed when k is in P) and Qe (the
   unabsorbed original markers of P, at their exact shifted positions). *)
Definition Core (P : list nat) (k a b : nat) (Q : list nat) : Prop :=
  valid Q /\ 2 <= a /\ exists Qi Qe, Q = Qi ++ Qe /\ length Qi + a = b + 1 + ind P k /\
    Forall (fun q => q + 2 + ind P k <= a) Qi /\ Sh (k + 3) a Qe (filter (fun p => k <? p) P).

(* Inv(M,n), with alpha = cnt P n; T-word when n+alpha is odd, S-word when even *)
Definition Inv (P : list nat) (n : nat) (W : list nat) : Prop :=
  (Nat.Odd (n + cnt P n) /\ exists a Q, W = a :: 2 :: (n + cnt P n) :: mw Q /\
     Core P n a (n + cnt P n) Q) \/
  (Nat.Even (n + cnt P n) /\ exists a Q, W = 2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q /\
     Core P (S n) a (n + cnt P n - 1) Q).

Definition Claim (Lm : nat) : Prop :=
  forall Q k, k + length Q <= Lm -> valid Q -> exists W, Orb Q k W /\ (1 <= k -> Inv Q k W).

Lemma stepU P : valid P -> exists W', Ep (1 :: mw P) (cost P 0) W' /\ Inv P 1 W'.
Proof.
  intros HV0. assert (Hc : cost P 0 = 2).
  { unfold cost, ind. rewrite (cnt1_valid P HV0), cnt_0. reflexivity. }
  rewrite Hc. unfold Inv. rewrite (cnt1_valid P HV0).
  destruct P as [|p P'].
  - exists [2;2;1]. split; [apply U0|]. left. split; [exists 0; reflexivity|].
    exists 2, (@nil nat). split; [reflexivity|]. split; [exact I|]. split; [lia|]. exists (@nil nat), (@nil nat).
    split; [reflexivity|]. split; [reflexivity|]. split; constructor.
  - pose proof HV0 as HV. destruct HV as [[t Ht] HV']. pose proof (valid_gt _ _ HV') as Hg.
    destruct t as [|t].
    + replace p with 1 in * by lia.
      exists (3 :: 2 :: 1 :: mwf 1 P'). split.
      { apply (U2 0 (mwf 1 P')). apply valid_tail_ok. exact HV'. }
      left. split; [exists 0; reflexivity|].
      exists 3, (map (fun p => p - 1) P'). split.
      { unfold mw. rewrite <- (mwf_unshift 1 1 P'); [reflexivity | lia |].
        eapply Forall_impl; [|exact Hg]. cbn; intros; lia. }
      split; [apply (valid_unshift 0 1 P' HV')|]. split; [lia|].
      exists (@nil nat), (map (fun p => p - 1) P'). split; [reflexivity|].
      rewrite (ind_in (1 :: P') 1 HV0 (or_introl eq_refl)).
      split; [reflexivity|]. split; [constructor|].
      cbn [filter]. change (1 <? 1) with false. cbv iota.
      rewrite (filter_all P' 1 Hg).
      apply (Sh_unmap 3 1 P'). eapply Forall_impl; [|exact Hg]. cbn; intros; lia.
    + exists (2 :: 2 :: 1 :: S (S (2 * t)) :: 1 :: mwf p P'). split.
      { change (mw (p :: P')) with ((p - 0 + 1) :: 1 :: mwf p P').
        replace (p - 0 + 1) with (S (S (S (S (2 * t))))) by lia. apply U1. }
      left. split; [exists 0; reflexivity|].
      exists 2, (map (fun q => q - 2) (p :: P')). split.
      { unfold mw. cbn [map mwf]. rewrite (mwf_unshift p 2 P'); [| lia |].
        - do 4 f_equal. lia.
        - eapply Forall_impl; [|exact Hg]. cbn; intros; lia. }
      split.
      { apply (valid_unshift 0 2 (p :: P')). cbn [valid_from]. split; [exists t; lia | exact HV']. }
      split; [lia|].
      exists (@nil nat), (map (fun q => q - 2) (p :: P')). split; [reflexivity|].
      assert (Hn1 : ~ In 1 (p :: P')).
      { intros [H|H]; [lia|]. rewrite Forall_forall in Hg. specialize (Hg _ H). lia. }
      rewrite (ind_nin _ _ Hn1). split; [reflexivity|]. split; [constructor|].
      rewrite filter_all.
      * apply (Sh_unmap 2 2 (p :: P')). constructor; [lia|].
        eapply Forall_impl; [|exact Hg]. cbn; intros; lia.
      * constructor; [lia|]. eapply Forall_impl; [|exact Hg]. cbn; intros; lia.
Qed.

Lemma stepS P n a Q : valid P -> 1 <= n -> Nat.Even (n + cnt P n) ->
  Core P (S n) a (n + cnt P n - 1) Q ->
  exists W', Ep (2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.
Proof.
  intros HV Hn [e He] (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh).
  assert (Hnin : ~ In n P).
  { intro Hin. destruct (parity_in 0 P n HV Hin) as [u Hu]. lia. }
  assert (HcS : cnt P (S n) = cnt P n) by (apply cnt_S_nin; exact Hnin).
  assert (Hcost : cost P n = 2) by (unfold cost, ind; lia).
  rewrite Hcost.
  assert (Ha3 : 2 + ind P (S n) <= a).
  { destruct Qi as [|q Qi'].
    - cbn [length] in Hlen. lia.
    - pose proof (valid_app_l _ _ HVQ) as Hq1. inversion Hq1; subst. inversion Hfa; subst. lia. }
  destruct a as [|a']; [lia|].
  destruct (n + cnt P n - 1) as [|b'] eqn:Hb; [lia|].
  exists (S (S a') :: 2 :: S (S (S b')) :: 2 :: 1 :: mw (Qi ++ Qe)). split.
  { apply ruleS. apply mw_tail_ok. exact HVQ. }
  left. split.
  { exists e. rewrite HcS. lia. }
  exists (S (S a')), (1 :: map (fun q => q + 1) (Qi ++ Qe)). split.
  { rewrite mw_cons1. rewrite HcS. do 3 f_equal. lia. }
  split; [apply valid_cons1; exact HVQ|]. split; [lia|].
  exists (1 :: map (fun q => q + 1) Qi), (map (fun q => q + 1) Qe).
  split; [rewrite map_app; reflexivity|].
  split; [cbn [length]; rewrite length_map; rewrite HcS; lia|].
  split.
  { constructor; [lia|]. apply Forall_map. eapply Forall_impl; [|exact Hfa]. cbn; intros; lia. }
  eapply Sh_eq; [apply Sh_map with (d := 1); exact Hsh | reflexivity | lia].
Qed.

Lemma stepT_nabs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm ->
  Nat.Odd (n + cnt P n) -> ~ In n P -> Core P n a (n + cnt P n) Q ->
  exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.
Proof.
  intros IH HV Hn HL [e He] Hnin (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh).
  assert (HcS : cnt P (S n) = cnt P n) by (apply cnt_S_nin; exact Hnin).
  assert (Hi0 : ind P n = 0) by (apply ind_nin; exact Hnin).
  rewrite Hi0 in Hlen, Hfa.
  assert (Hcost : cost P n = 2) by (unfold cost; lia). rewrite Hcost.
  assert (Hnin1 : ~ In (S n) P).
  { intro Hin. destruct (parity_in 0 P (S n) HV Hin) as [u Hu]. lia. }
  assert (HQe : Forall (fun q => a - 1 <= q) Qe).
  { apply (Sh_ge _ _ _ _ (a - 1) (S (S n)) Hsh); [|lia].
    intros p Hp. pose proof (filter_gt _ _ _ Hp) as H1. apply filter_In in Hp. destruct Hp as [Hp _].
    assert (p <> S n) by (intros ->; contradiction). lia. }
  assert (HQi : Forall (fun q => q < a - 1) Qi) by (eapply Forall_impl; [|exact Hfa]; cbn; intros; lia).
  assert (HcQ : cnt (Qi ++ Qe) (a - 1) = length Qi).
  { rewrite cnt_app, (cnt_all_lt _ _ HQi), (cnt_all_ge _ _ HQe). lia. }
  pose proof (filter_cnt_len P n) as HlP. pose proof (Sh_len _ _ _ _ Hsh) as HlQe.
  destruct (IH (Qi ++ Qe) (a - 1)) as (W1 & HO1 & HI1).
  { rewrite length_app. lia. }
  { exact HVQ. }
  specialize (HI1 ltac:(lia)).
  unfold Inv in HI1. rewrite HcQ in HI1.
  destruct HI1 as [[_ (a' & Q' & -> & HC')] | [[e' He'] _]]; [| exfalso; lia].
  assert (Hb : a - 1 + length Qi = n + cnt P n) by lia.
  rewrite Hb in *.
  exists (2 :: 2 :: a' :: 2 :: (n + cnt P n) :: mw Q'). split.
  { pose proof (ruleT a (n + cnt P n) (Qi ++ Qe) _ HO1 Ha ltac:(lia) HVQ ltac:(lia)) as HT.
    rewrite HcQ in HT. replace (n + cnt P n + 3 - a - length Qi) with 2 in HT by lia. exact HT. }
  right. split.
  { exists (e + 1). rewrite HcS. lia. }
  exists a', Q'. split.
  { rewrite HcS. do 5 f_equal. lia. }
  replace (S n + cnt P (S n) - 1) with (n + cnt P n) by lia.
  destruct HC' as (HVQ' & Ha' & Qi' & Qe' & -> & Hlen' & Hfa' & Hsh').
  assert (Hind : ind (Qi ++ Qe) (a - 1) = ind P (S (S n))).
  { apply ind_iff; [exact HVQ | exact HV | ].
    apply (in_transfer Qi Qe P (a - 1) (S (S n)) (n + 3) a n HQi Hsh); lia. }
  split; [exact HVQ'|]. split; [exact Ha'|].
  exists Qi', Qe'. split; [reflexivity|]. rewrite <- Hind. split; [lia|]. split; [exact Hfa'|].
  apply (sh_compose Qi Qe Qe' P n a a' (a - 1) (S (S n))); try assumption; try lia.
  eapply Forall_impl; [|exact HQi]. cbn; intros; lia.
Qed.

Lemma stepT_abs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm ->
  Nat.Odd (n + cnt P n) -> In n P -> Core P n a (n + cnt P n) Q ->
  exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.
Proof.
  intros IH HV Hn HL [e He] Hin (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh).
  assert (HcS : cnt P (S n) = S (cnt P n)) by (apply (cnt_S_in 0); assumption).
  assert (Hi1 : ind P n = 1) by (apply ind_in; assumption).
  rewrite Hi1 in Hlen, Hfa.
  assert (Hcost : cost P n = 3) by (unfold cost; lia). rewrite Hcost.
  assert (Ha3 : 3 <= a).
  { destruct Qi as [|q Qi'].
    - cbn [length] in Hlen. lia.
    - pose proof (valid_app_l _ _ HVQ) as Hq1. inversion Hq1; subst. inversion Hfa; subst. lia. }
  assert (HQe : Forall (fun q => a - 2 <= q) Qe).
  { apply (Sh_ge _ _ _ _ (a - 2) (S n) Hsh); [|lia].
    intros p Hp. apply filter_gt in Hp. lia. }
  assert (HQi : Forall (fun q => q < a - 2) Qi) by (eapply Forall_impl; [|exact Hfa]; cbn; intros; lia).
  assert (HcQ : cnt (Qi ++ Qe) (a - 2) = length Qi).
  { rewrite cnt_app, (cnt_all_lt _ _ HQi), (cnt_all_ge _ _ HQe). lia. }
  pose proof (filter_cnt_len P n) as HlP. pose proof (Sh_len _ _ _ _ Hsh) as HlQe.
  destruct (IH (Qi ++ Qe) (a - 2)) as (W2 & HO2 & HI2).
  { rewrite length_app. lia. }
  { exact HVQ. }
  specialize (HI2 ltac:(lia)).
  unfold Inv in HI2. rewrite HcQ in HI2.
  destruct HI2 as [[_ (a'' & Q'' & -> & HC'')] | [[e' He'] _]]; [| exfalso; lia].
  assert (Hb : a - 2 + length Qi = n + cnt P n) by lia.
  rewrite Hb in *.
  destruct HC'' as (HVQ'' & Ha'' & Qi'' & Qe'' & -> & Hlen'' & Hfa'' & Hsh'').
  exists (S (S a'') :: 2 :: S (S (n + cnt P n)) :: mw (map (fun q => q + 2) (Qi'' ++ Qe''))). split.
  { apply ruleX; try assumption; lia. }
  left. split.
  { exists (e + 1). rewrite HcS. lia. }
  exists (S (S a'')), (map (fun q => q + 2) (Qi'' ++ Qe'')). split.
  { rewrite HcS. do 3 f_equal. lia. }
  replace (S n + cnt P (S n)) with (S (S (n + cnt P n))) by lia.
  assert (Hind : ind (Qi ++ Qe) (a - 2) = ind P (S n)).
  { apply ind_iff; [exact HVQ | exact HV | ].
    apply (in_transfer Qi Qe P (a - 2) (S n) (n + 3) a n HQi Hsh); lia. }
  split; [apply valid_map2; exact HVQ''|]. split; [lia|].
  exists (map (fun q => q + 2) Qi''), (map (fun q => q + 2) Qe''). split; [apply map_app|].
  rewrite length_map. rewrite <- Hind. split; [lia|]. split.
  { apply Forall_map. eapply Forall_impl; [|exact Hfa'']. cbn; intros; lia. }
  assert (Hc : Sh (S n + 3) a'' Qe'' (filter (fun p => S n <? p) P)).
  { apply (sh_compose Qi Qe Qe'' P n a a'' (a - 2) (S n)); try assumption; try lia.
    eapply Forall_impl; [|exact HQi]. cbn; intros; lia. }
  eapply Sh_eq; [apply Sh_map with (d := 2); exact Hc | reflexivity | lia].
Qed.

Lemma step_lemma Lm : Claim Lm -> forall P n W, n + length P <= Lm -> valid P -> Orb P n W ->
  (1 <= n -> Inv P n W) -> exists W', Ep W (cost P n) W' /\ Inv P (S n) W'.
Proof.
  intros IH P n W HL HV HO HI. destruct n as [|n'].
  - inversion HO; subst. apply stepU; exact HV.
  - specialize (HI ltac:(lia)).
    destruct HI as [[Ho (a & Q & -> & HC)] | [He (a & Q & -> & HC)]].
    + destruct (in_dec Nat.eq_dec (S n') P) as [Hin | Hnin].
      * eapply stepT_abs; eauto; lia.
      * eapply stepT_nabs; eauto; lia.
    + eapply stepS; eauto; lia.
Qed.

Theorem main Lm : Claim Lm.
Proof.
  induction Lm as [|Lm IHL]; intros Q k Hk HV.
  - assert (k = 0) by lia. subst. exists (1 :: mw Q). split; [constructor | lia].
  - destruct k as [|k].
    + exists (1 :: mw Q). split; [constructor | lia].
    + destruct (IHL Q k ltac:(lia) HV) as (W & HO & HI).
      destruct (step_lemma Lm IHL Q k W ltac:(lia) HV HO HI) as (W' & HE & HI').
      exists W'. split; [econstructor; eauto | intros; exact HI'].
Qed.

(* ---------- top level ---------- *)
Lemma init : c0 -->* conf [] [3; 2; 1].
Proof. unfold conf, lside, rside. cbn [lpow app]. solve_init. Qed.

Lemma nonhalt: ~halts tm c0.
Proof.
  eapply multistep_nonhalt; [apply init |].
  apply (progress_nonhalt_cond tm (nat * list nat) (0, [1]) (fun i => conf [] (3 :: 2 :: snd i))
           (fun i => Orb [] (fst i) (snd i) /\ (1 <= fst i -> Inv [] (fst i) (snd i)))).
  - intros [n W] [HO HI]. cbn [fst snd] in *.
    destruct (step_lemma n (main n) [] n W ltac:(cbn; lia) I HO HI) as (W' & HE & HI').
    exists (S n, W'). cbn [fst snd]. split.
    + apply Ep_tm in HE. replace (cost [] n) with 2 in HE by reflexivity. exact HE.
    + split; [econstructor; eauto | intros; exact HI'].
  - cbn [fst snd]. split; [exact (O0 []) | lia].
Qed.


(*
```
1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF

conf L R := 0^inf 1^a_1 0 1^a_2 0 .. 0 1^a_p <A 0 1^c_1 0^g_1 1^c_2 .. 1^c_r 0^inf
            (L = [a_p; ..; a_1] top first, R = [c_1; g_1; c_2; ..; c_r])
tR1   l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r  -->+  l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r
tR3   l 0 <A 0 1^(k+1) 0 0 1^m 0 r        -->+  l 1^(k+2) <A 0 1^(m+1) 0 0 r
tR2   l 0 1^(k+1) 0 1 <A 0 r              -->+  l <A 0 1^(k+2) 0 0 r
push  conf (x::L) (h::R')  -->+  conf (h::x-1::L) (updt R')     x >= 2      (tR1)
push0 conf [] (h::R')      -->+  conf [h+1] (updt R')                       (tR3)
pop   conf (1::y::L) R     -->+  conf L (y+1::2::R)              y >= 1      (tR2)
updt [] = [1],  updt [2;c] = [c+1],  updt (2::c::g::R) = c+1::g+1::R,  updt (g::R) = 1::g-1::R (g >= 3)

Edge W := conf [] (3::2::W);   Ep W c W' :  Edge W -->+ conf [] (5-c::2::W')
U0   Ep [1]                = (2, [2;2;1])
U1   Ep (1::g::rest)       = (2, 2::2::1::g-2::rest)                     g >= 4
U2   Ep (1::2::b::N)       = (2, b+2::2::1::N)                           b >= 1
S    Ep (2::2::a::2::b::N) = (2, a+1::2::b+2::2::1::N)                   a, b >= 1
T    Ep (a::2::b::mw Q)    = (2, b+3-a-#{q<a-1}::2::O_(a-1)(Q))          a-1+#{q<a-1} <= b
X    Ep (a::2::b::mw Q)    = (3, a''+2::2::b+2::mw (Q''+2))              O_(a-2)(Q) = a''::2::b::mw Q'',
                                                                         b = a-2+#{q<a-2}
mw [I_1;..;I_m] = (I_1+1) 1 (I_2-I_1+1) 1 ..        (marker word from its absorption indices)
O_0(Q) = 1::mw Q,  O_(n+1)(Q) = Ep(O_n(Q)) at cost 2+[n in Q]           (Orb)
Inv P n: al = #{p in P | p < n};  n+al odd:  O_n(P) = T(a, n+al)+mw Q,  k = n
                                  n+al even: O_n(P) = S(a, n+al-1)+mw Q, k = n+1
         Q = Qi ++ Qe, |Qi| = b+1-a+[k in P], every q in Qi <= a-2-[k in P],
         Qe = the indices of P above k, each shifted by a-k-3
start:  c0 -->* Edge [1] = Edge (O_0([]))                                (50 steps)
top:    O_n([]) has no markers, so Edge (O_n([])) -->+ Edge (O_(n+1)([])) for every n
```
*)