(* 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE--- halts.
   Shift-overflow bouncer counter.  The table is that of SOBCv6 TM3
   (1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD---) under the state renaming
   ours A B C D E F = TM3 B C A E D F (no mirror), started in TM3's state B.
   Adapted from verify/SOBCv6.v, Module TM3.
   Proof structure.  The left part of the tape is a counter Lmp x, a list of the words
   W0 = 001 and W1 = 111; W1 W0 is a digit 0, W1 W1 a digit 1, a lone W0 a separator.
   TM3's rules (LInc, LOv, Incs, Ov) carry over verbatim after renaming the two head
   notations.  An abstract list (LD') holds blocks W10 l = (W1 W0)^(1+l+n) and
   W11 l = (W1 W1)^(1+l+n) with a lower bound l on the length; one counter cycle on
   abstract lists is [step_rec] (Incs, then the overflow LOv), proved sound by
   [step_rec_spec].  The overflow [LOv_rec] has a second block case ("peel") that splits the
   far pair off a W11 block when the deeper result starts with W1 (lemma [LOv_peel]),
   and [LInc_rec] can stop inside a W10 block (its first pair becomes W1 W1, at the cost of
   one unit of the bound).  The bound on the count is kept in binary and saturates at 256.
   From the blank tape, [init] reaches P x2 after 38,573 steps; 192 abstract cycles follow
   ([iter], checked by computation); in the next overflow the head walks to the far end of the
   counter ([walk0], [walk1]) and the far tail [x_far] halts ([far_halt]); [doom_rec] checks
   that the final counter is x_far preceded by separators, W1 W1 pairs and W11 blocks.
   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 halt: functional_extensionality_dep only. *)

From BusyCoq Require Import Individual62.
Require Import Lia.
Require Import ZArith.
Require Import NArith.
Require Import String.
Require Import List.
From BusyCoq Require Import BinaryCounter_v2.
From BusyCoq Require Import NatMod.
From BusyCoq Require Import SimplTape.
From BusyCoq Require Import Longitudinal.
From BusyCoq Require Import Eqb.

Open Scope list.

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

Definition tm' := flip tm.

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

Notation w0 := <[0;0;1].
Notation w1 := <[1;1;1].
Notation "l <| r" := (l <{{D}} [0;1;0] *> r) (at level 30).
Notation "l |> r" := (l {{A}}> r) (at level 30).

Inductive LD := W0 | W1.

Fixpoint Lmp(ls:list LD):side :=
match ls with
| [] => 0inf
| W0::t => Lmp t <* w0
| W1::t => Lmp t <* w1
end.

Inductive LInc: (list LD)->(list LD)->Prop :=
| LInc_w0 x x':
  LInc x x' ->
  LInc (W0::x) (W0::x')
| LInc_d0 x:
  LInc (W1::W0::x) (W1::W1::x)
| LInc_d1 x x':
  LInc x x' ->
  LInc (W1::W1::x) (W1::W0::x')
.

Lemma LInc_spec [x x']:
  LInc x x' ->
  forall r,
  Lmp x <| r -->*
  Lmp x' <* w0 |> r.
Proof.
  intros H.
  induction H; intros; cbn.
  all: repeat (er || follow).
Qed.

Inductive LOv: (list LD)->(list LD)->Prop :=
| LOv_O: LOv [] [W0;W1]
| LOv_d1_0 x x':
  LOv x (W0::x') ->
  LOv (W1::W1::x) (W0::W0::W1::x')
| LOv_d1_1 x x' x'':
  LOv x (W1::x') ->
  LInc x' x'' ->
  LOv (W1::W1::x) (W0::W0::W0::x'')
| LOv_w0 x x':
  LOv x x' ->
  LOv (W0::x) (W1::x')
.

Lemma LOv_spec [x x']:
  LOv x x' ->
  forall r,
  Lmp x <| [1] *> r -->*
  Lmp x' |> r.
Proof.
  intros H.
  induction H; intros; cbn.
  all: repeat (er || follow).
  follow (LInc_spec H0); er.
Qed.


Inductive LIncs: (list LD)->(list LD)->nat->Prop :=
| LIncs_O:
  LIncs [] [] O
| LIncs_w0 x x' n:
  LIncs x x' n ->
  LIncs (W0::x) (W0::x') n
| LIncs_d0 x x' n:
  LIncs x x' n ->
  LIncs (W1::W0::x) (W1::W1::x') (n*2+1)
| LIncs_d1 x x' n:
  LIncs x x' n ->
  LIncs (W1::W1::x) (W1::W1::x') (n*2+0)
.

Notation hR := (A,<[0;0;1]).
Notation hL := (D,[0;1;0]).
Notation hLR := [(hL,hR)].
Notation hRL := [(hR,hL)].

Lemma LIncs_spec [x x' n]:
  LIncs x x' n ->
  sideRLs tm' (hLR^^n) (Lmp x) (Lmp x').
Proof.
  intros H.
  induction H; cbn[Lmp].
  - solve_sideRLs.
  - eapply segRLs_sideRLs_concat.
    2: eassumption.
    eapply segRLs_wall.
    1: solve_seg.
    1: solve_seg.
  - do 2 rewrite <-Str_app_assoc.
    eapply segRLs_sideRLs_concat.
    2: eassumption.
    eapply segRLs_addmul''.
    1: solve_segRLs.
    1: solve_segRLs.
  - do 2 rewrite <-Str_app_assoc.
    eapply segRLs_sideRLs_concat.
    2: eassumption.
    eapply segRLs_addmul''.
    1: solve_segRLs.
    1: solve_segRLs.
Qed.

Definition RC n := [1] *> [0;1;1]^^n *> [0;1] *> 0inf.

Lemma RIncs n m:
  sideRLs tm (hRL^^n) (RC m) (RC (n+m)).
Proof.
  unfold RC.
  induction n.
  - solve_sideRLs.
  - replace (S n) with (n+1) by lia.
    rewrite lpow_add.
    eapply sideRLs_trans.
    1: apply IHn.
    simpl_tape; simpl_rotate.
    solve_sideRLs.
Qed.

Lemma Incs x x' n0:
  LIncs x x' (n0*2+1) ->
  Lmp x <| RC 1 -->*
  Lmp x' <| RC ((n0+1)*2).
Proof.
  intros HL.
  epose proof (LIncs_spec HL) as HL'.
  epose proof (RIncs (n0*2+1) 1) as HR.
  replace (n0*2+1+1) with ((n0+1)*2) in HR by lia.
  apply (sideRLs_concat_1L HR HL').
Qed.

Lemma Lmp_d0 x n:
  Lmp (x <+ <[W0;W1]^^n) = Lmp x <* (w0<+w1)^^n.
Proof.
  induction n; cbn.
  - trivial.
  - rewrite IHn; reflexivity.
Qed.

Lemma Lmp_d1 x n:
  Lmp (x <+ <[W1;W1]^^n) = Lmp x <* (w1<+w1)^^n.
Proof.
  induction n; cbn.
  - trivial.
  - rewrite IHn; reflexivity.
Qed.

Lemma Ov x x' m:
  LOv x (W0::x') ->
  Lmp x <| RC ((m+1)*2) -->*
  Lmp (x' <+ <[W1;W1] <+ <[W0;W1]^^m) <| RC 1.
Proof.
  rewrite Lmp_d0.
  intros HL.
  follow (LOv_spec HL).
  es.
Qed.

Lemma LIncs_lpow [x x' n0] n:
  LIncs x x' n0 ->
  LIncs (x <+ <[W0;W1]^^n) (x' <+ <[W1;W1]^^n) ((n0+1)*2^n-1).
Proof.
  intros H.
  induction n.
  - cbn.
    applys_eq H; lia.
  - epose proof (Nat.pow_nonzero 2 n).
    replace ((n0+1)*2^(S n)-1) with (((n0+1)*2^n-1)*2+1) by (cbn; lia).
    econstructor; eassumption.
Qed.

Lemma LIncs_lpow' [x x' n0] n:
  LIncs x x' n0 ->
  LIncs (x <+ <[W1;W1]^^n) (x' <+ <[W1;W1]^^n) ((n0)*2^n).
Proof.
  intros H.
  induction n.
  - cbn.
    applys_eq H; lia.
  - epose proof (Nat.pow_nonzero 2 n).
    replace ((n0)*2^(S n)) with (((n0)*2^n)*2+0) by (cbn; lia).
    econstructor; eassumption.
Qed.

Lemma LOv_lpow x x' n:
  LOv x (W0::W0::x') ->
  LOv (x <+ <[W1;W1]^^n) (x' <+ <[W0;W1]^^n <+ <[W0;W0]).
Proof.
  intros H.
  induction n.
  - eassumption.
  - econstructor; eassumption.
Qed.

(* New (L4 of the write-up): the far pair of a (W1 W1) block, seen by a deeper
   result W1 v, is split off and handled by LOv_d1_1; the rest is LOv_lpow. *)
Lemma LOv_peel x v v' k:
  LOv x (W1::v) ->
  LInc v v' ->
  LOv ([W1;W1]^^(1+k)++x) (W0::W0::[W1;W0]^^k++W0::v').
Proof.
  intros H1 H2.
  replace ([W1;W1]^^(1+k)++x) with ([W1;W1]^^k++(W1::W1::x)).
  2: {
    change (W1::W1::x) with ([W1;W1]++x).
    rewrite app_assoc, lpow_shift.
    reflexivity.
  }
  apply (LOv_lpow (W1::W1::x) (W0::v') k).
  eapply LOv_d1_1; eauto.
Qed.


(* Abstract lists: blocks with a lower bound l on their length. *)
Inductive LD' :=
| W0' | W1' | W10 (l:nat) | W11 (l:nat).

Inductive Lmp': list LD' -> list LD -> Prop :=
| Lmp'_W0' x x':
  Lmp' x x' ->
  Lmp' (W0'::x) (W0::x')
| Lmp'_W1' x x':
  Lmp' x x' ->
  Lmp' (W1'::x) (W1::x')
| Lmp'_W10 x x' l n:
  Lmp' x x' ->
  Lmp' (W10 l::x) ([W1;W0]^^(1+l+n)++x')
| Lmp'_W11 x x' l n:
  Lmp' x x' ->
  Lmp' (W11 l::x) ([W1;W1]^^(1+l+n)++x')
| Lmp'_O:
  Lmp' [] []
.

Fixpoint LInc_rec(x:list LD')(T:nat){struct T}:option (list LD') :=
match T with
| O => None
| S T0 =>
match x with
| W0'::t =>
  LInc_rec t T0 &&& (fun v => Some (W0'::v))
| W1'::W1'::t =>
  LInc_rec t T0 &&& (fun v => Some (W1'::W0'::v))
| W1'::W0'::t =>
  Some (W1'::W1'::t)
| W10 (S l)::t =>
  Some (W1'::W1'::W10 l::t)
| _ => None
end
end.

(* The lower bound on the count is kept in binary (N) and saturates at maxv. *)
Definition maxv:N := 256%N.

Definition upd (n:N) (m:nat) : N := N.min maxv (2*n + N.of_nat m)%N.

Lemma upd_le n m: N.to_nat (upd n m) <= N.to_nat n * 2 + m.
Proof. unfold upd. lia. Qed.

Fixpoint LIncs_rec(x:list LD')(T:nat){struct T}:option ((list LD')*N*nat) :=
match T with
| O => None
| S T0 =>
match x with
| W0'::t =>
  LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W0'::v,n,m))
| W1'::W1'::t =>
  LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W1'::W1'::v,upd n m,0%nat))
| W1'::W0'::t =>
  LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W1'::W1'::v,upd n m,1%nat))
| W11 l::t =>
  LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W11 l::v,upd n m,0%nat))
| W10 l::t =>
  LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W11 l::v,upd n m,1%nat))
| [] => Some ([],0%N,0%nat)
| _ => None
end
end.

Fixpoint LOv_rec(x:list LD')(T:nat){struct T}:option (list LD') :=
match T with
| O => None
| S T0 =>
match x with
| [] => Some [W0';W1']
| W0'::t =>
  LOv_rec t T0 &&& (fun v => Some (W1'::v))
| W1'::W1'::t =>
  LOv_rec t T0 &&& (fun v =>
  match v with
  | W0'::v0 => Some (W0'::W0'::W1'::v0)
  | W1'::v0 =>
    LInc_rec v0 T &&& (fun v1 => Some (W0'::W0'::W0'::v1))
  | _ => None
  end)
| W11 l::t =>
  LOv_rec t T0 &&& (fun v =>
  match v with
  | W0'::W0'::v0 => Some (W0'::W0'::W10 l::v0)
  | W1'::v0 =>
    match l with
    | O => None
    | S l0 => LInc_rec v0 T &&& (fun v1 => Some (W0'::W0'::W10 l0::W0'::v1))
    end
  | _ => None
  end)
| _ => None
end
end.

Hint Constructors LInc LIncs LOv Lmp' : core.

Ltac invs :=
repeat
match goal with
| [ H: Some _ = Some _ |- _ ] => inverts H
| [ H: Lmp' (_::_) _ |- _ ] => inverts H
| [ H: Lmp' [] _ |- _ ] => inverts H
end.

Ltac eic :=
repeat
match goal with
| |- exists _, _ => eexists
| |- _ /\ _ => econstructor
| |- _ -> _ => intros
end.

Lemma LInc_rec_spec x T x0 x':
  LInc_rec x T = Some x0 ->
  Lmp' x x' ->
  exists x0',
  LInc x' x0' /\
  Lmp' x0 x0'.
Proof with try congruence.
  gen x x0 x'.
  induction T; cbn in *; intros...
  unfold if_Some in *.
  destruct x as [|w x]...
  destruct w...
  - destruct (LInc_rec x T) eqn:E...
    invs.
    specialize (IHT _ _ _ E H1) as [x0' [I1 I2]].
    eic; eauto.
  - destruct x as [|w x]...
    destruct w...
    + invs.
      eic; eauto.
    + destruct (LInc_rec x T) eqn:E...
      invs.
      specialize (IHT _ _ _ E H0) as [x0' [I1 I2]].
      eic; eauto.
  - destruct l as [|l]...
    invs.
    exists (W1::W1::[W1;W0]^^(1+l+n)++x'0).
    split.
    + cbn. apply LInc_d0.
    + do 2 constructor.
      apply Lmp'_W10.
      assumption.
Qed.

Opaque LInc_rec.

Lemma LOv_rec_spec x T x0 x':
  LOv_rec x T = Some x0 ->
  Lmp' x x' ->
  exists x0',
  LOv x' x0' /\
  Lmp' x0 x0'.
Proof with try congruence.
  gen x x0 x'.
  induction T; cbn in *; intros...
  unfold if_Some in *.
  destruct x as [|w x]...
  - invs.
    eic; eauto.
  - destruct w...
    + destruct (LOv_rec x T) eqn:E...
      invs.
      specialize (IHT _ _ _ E H1) as [x0' [I1 I2]].
      eic; eauto.
    + destruct x as [|w x]...
      destruct w...
      destruct (LOv_rec x T) eqn:E...
      invs.
      specialize (IHT _ _ _ E H1) as [x0' [I1 I2]].
      destruct l as [|w l]...
      destruct w...
      * invs.
        eic; eauto.
      * invs.
        destruct (LInc_rec l (S T)) eqn:E1...
        epose proof (LInc_rec_spec _ _ _ _ E1 H2) as [x1' [I3 I4]].
        invs.
        eic; eauto.
    + destruct (LOv_rec x T) eqn:E...
      invs.
      match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ E HL) as [x0' [I1 I2]] end.
      destruct l0 as [|w l0]...
      destruct w...
      * destruct l0 as [|w l0]...
        destruct w...
        invs.
        eic.
        -- eapply LOv_lpow; eauto.
        -- repeat econstructor; eauto.
      * destruct l as [|l]...
        destruct (LInc_rec l0 (S T)) eqn:E1...
        invs.
        match goal with HL: Lmp' l0 _ |- _ => epose proof (LInc_rec_spec _ _ _ _ E1 HL) as [x1' [I3 I4]] end.
        exists (W0::W0::[W1;W0]^^(1+l+n)++W0::x1').
        split.
        -- apply (LOv_peel _ _ _ (1+l+n) I1 I3).
        -- do 2 constructor.
           apply Lmp'_W10.
           constructor.
           assumption.
Qed.

Transparent LInc_rec.

Opaque upd.

Lemma LIncs_rec_spec x T x0 x' n m:
  LIncs_rec x T = Some (x0,n,m) ->
  Lmp' x x' ->
  exists x0' n',
  LIncs x' x0' (n'*2+m) /\
  Lmp' x0 x0' /\
  n'>=N.to_nat n.
Proof with try congruence.
  gen x x0 x' n m.
  induction T; cbn in *; intros...
  unfold if_Some in *.
  destruct x as [|w x]...
  - invs.
    exists (@nil LD), 0%nat.
    split; [constructor|split; [constructor|cbn; lia]].
  - destruct w...
    + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E...
      invs.
      match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end.
      eic; eauto.
    + destruct x as [|w x]...
      destruct w...
      * destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E...
        invs.
        match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end.
        pose proof (upd_le n1 m1).
        eic; eauto; lia.
      * destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E...
        invs.
        match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end.
        pose proof (upd_le n1 m1).
        eic; eauto; lia.
    + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E...
      invs.
      match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end.
      match goal with |- context [ _^^(1+l+?k) ] =>
        replace (1+l+k) with (1+(l+k)) by lia; set (j:=l+k) end.
      pose proof (upd_le n1 m1).
      eic.
      * rewrite lpow_add; cbn.
        econstructor.
        eapply LIncs_lpow; eauto.
      * econstructor; eauto.
      * pose proof (Nat.pow_nonzero 2 j).
        rewrite Nat.mul_add_distr_r.
        pose proof (Nat.mul_le_mono_l 1 (2^j) (n'*2+m1)).
        lia.
    + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E...
      invs.
      match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end.
      match goal with |- context [ _^^(1+l+?k) ] =>
        replace (1+l+k) with (1+(l+k)) by lia; set (j:=l+k) end.
      pose proof (upd_le n1 m1).
      eic.
      * rewrite lpow_add; cbn.
        econstructor.
        eapply LIncs_lpow'; eauto.
      * econstructor; eauto.
      * pose proof (Nat.pow_nonzero 2 j).
        pose proof (Nat.mul_le_mono_l 1 (2^j) (n'*2+m1)).
        lia.
Qed.

Transparent upd.

(* One counter cycle on abstract lists.  The new block of (W1 W0) pairs made by the
   overflow is one abstract token W10 (n-1). *)
Definition step_rec(x:list LD'):option (list LD') :=
LIncs_rec x (S(length x)) &&& (fun '(x0,n,m) =>
if m =? 1 then
  match N.to_nat n with
  | O => None
  | S n0 =>
    LOv_rec x0 (S(length x0)) &&& (fun x1 =>
    match x1 with
    | W0'::x2 =>
      Some (W10 n0::W1'::W1'::x2)
    | _ => None
    end)
  end
else None).

Inductive P: (list LD')->Prop :=
| P_intro x x':
  Lmp' x x' ->
  c0 -->* Lmp x' <| RC 1 ->
  P x.

Lemma step_rec_spec x x':
  step_rec x = Some x' ->
  P x ->
  P x'.
Proof with try congruence.
  intros H.
  unfold step_rec in H.
  unfold if_Some in H.
  intros HP.
  inverts HP.
  destruct (LIncs_rec x (S(length x))) as [[[v n] m]|] eqn:E...
  destruct (Nat.eqb_spec m 1)...
  subst.
  destruct (N.to_nat n) as [|n0] eqn:En...
  destruct (LOv_rec v (S(length v))) eqn:E0...
  destruct l as [|w l]...
  destruct w...
  invs.
  epose proof (LIncs_rec_spec _ _ _ _ _ _ E H0) as [x0' [n' [I1 [I2 I3]]]].
  epose proof (LOv_rec_spec _ _ _ _ E0 I2) as [x1' [I4 I5]].
  invs.
  eapply P_intro with (x':=[W1;W0]^^(n')++[W1;W1]++x').
  - replace n' with (1+n0+(n'-S n0)) by lia.
    apply Lmp'_W10.
    cbn.
    eauto.
  - follow H1.
    follow Incs.
    follow Ov.
    finish.
Qed.

Fixpoint iter (k:nat) (x:list LD') : option (list LD') :=
match k with
| O => Some x
| S k0 => step_rec x &&& (fun y => iter k0 y)
end.

Lemma iter_spec k:
  forall x y,
  iter k x = Some y ->
  P x ->
  P y.
Proof.
  induction k; cbn; intros x y H HP.
  - inverts H. exact HP.
  - unfold if_Some in H.
    destruct (step_rec x) as [x1|] eqn:E; [|discriminate].
    eapply IHk.
    1: exact H.
    eapply step_rec_spec; eauto.
Qed.


(* The start: P x2 after 38,573 steps from the blank tape (two exact cycles from the
   counter 1000111011 reached after 847 steps). *)
Definition x2 : list LD :=
[W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0;
 W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0;
 W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W1; W0; W1; W0; W1; W0; W0; W1; W1;
 W0; W0; W0; W0; W1; W1; W1; W0; W1; W1].

Definition x2' : list LD' :=
map (fun x => match x with W0 => W0' | W1 => W1' end) x2.

Lemma init: P x2'.
Proof.
  apply P_intro with (x':=x2).
  - unfold x2', x2. cbn. repeat constructor.
  - unfold x2. cbn. solve_init.
Qed.


(* The halt.  A list x is doomed if the overflow run started on it halts. *)
Definition Doomed (x:list LD) := forall r, halts tm (Lmp x <| [1] *> r).

Lemma walk0 x r:
  Lmp x <* w0 <| [1] *> r -->*
  Lmp x <| [1] *> [0;1;1] *> r.
Proof. es. Qed.

Lemma walk1 x r:
  Lmp x <* w1 <* w1 <| [1] *> r -->*
  Lmp x <| [1] *> [0;1;0;1;0;1] *> r.
Proof. es. Qed.

Lemma doomed_w0 x: Doomed x -> Doomed (W0::x).
Proof.
  intros H r. cbn [Lmp].
  eapply halts_evstep.
  2: apply walk0.
  apply H.
Qed.

Lemma doomed_w1 x: Doomed x -> Doomed (W1::W1::x).
Proof.
  intros H r. cbn [Lmp].
  eapply halts_evstep.
  2: apply walk1.
  apply H.
Qed.

Lemma doomed_pow k x: Doomed x -> Doomed ([W1;W1]^^k++x).
Proof.
  intros H.
  induction k; cbn; auto.
  apply doomed_w1. exact IHk.
Qed.

Definition x_far : list LD :=
[W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W1;W1;W1;W1].

Lemma far_halt: Doomed x_far.
Proof.
  intros r.
  unfold x_far. cbn [Lmp].
  solve_halt.
Qed.

Definition x_far' : list LD' :=
[W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W1';W1';W1';W1'].

Definition tok_eqb (a b: LD') : bool :=
match a, b with
| W0', W0' => true
| W1', W1' => true
| _, _ => false
end.

Fixpoint ltok_eqb (a b: list LD') : bool :=
match a, b with
| [], [] => true
| x::a0, y::b0 => tok_eqb x y && ltok_eqb a0 b0
| _, _ => false
end.

Lemma ltok_eqb_spec a b: ltok_eqb a b = true -> a = b.
Proof.
  gen b.
  induction a as [|x a IH]; intros b H; destruct b as [|y b]; cbn in H; try congruence.
  apply and_true_iff in H as [H1 H2].
  destruct x, y; cbn in H1; try congruence; f_equal; auto.
Qed.

Fixpoint doom_rec (X: list LD') : bool :=
if ltok_eqb X x_far' then true else
match X with
| W0' :: t => doom_rec t
| W1' :: W1' :: t => doom_rec t
| W11 _ :: t => doom_rec t
| _ => false
end.

Lemma doom_rec_eq X:
  doom_rec X =
  if ltok_eqb X x_far' then true else
  match X with
  | W0' :: t => doom_rec t
  | W1' :: W1' :: t => doom_rec t
  | W11 _ :: t => doom_rec t
  | _ => false
  end.
Proof. destruct X; reflexivity. Qed.

Lemma doom_rec_spec n:
  forall X x,
  length X <= n ->
  doom_rec X = true ->
  Lmp' X x ->
  Doomed x.
Proof.
  induction n; intros X x Hl H HL.
  - destruct X; cbn in Hl; [|lia].
    cbn in H. congruence.
  - rewrite doom_rec_eq in H.
    destruct (ltok_eqb X x_far') eqn:E.
    + apply ltok_eqb_spec in E. subst X.
      unfold x_far' in HL.
      invs.
      apply far_halt.
    + destruct X as [|a X]; [discriminate|].
      cbn in Hl.
      destruct a.
      * invs. apply doomed_w0. eapply IHn; eauto; lia.
      * destruct X as [|a X]; [discriminate|].
        destruct a; try discriminate.
        invs. apply doomed_w1. cbn in Hl. eapply IHn; eauto; lia.
      * discriminate.
      * invs. apply doomed_pow. eapply IHn; eauto; lia.
Qed.

Definition final_check (k:nat) : bool :=
match iter k x2' with
| Some y =>
  match LIncs_rec y (S(length y)) with
  | Some (z,n,m) => if m =? 1 then doom_rec z else false
  | None => false
  end
| None => false
end.

Lemma final_check_ok: final_check 192 = true.
Proof. vm_compute. reflexivity. Qed.

Lemma final_check_spec k:
  final_check k = true ->
  exists y z n,
  iter k x2' = Some y /\
  LIncs_rec y (S(length y)) = Some (z,n,1%nat) /\
  doom_rec z = true.
Proof.
  unfold final_check.
  destruct (iter k x2') as [y|] eqn:E1; [|discriminate].
  destruct (LIncs_rec y (S(length y))) as [[[z n] m]|] eqn:E2; [|discriminate].
  destruct (Nat.eqb_spec m 1); [|discriminate].
  subst m. intros H. exists y, z, n.
  split; [reflexivity|split; [exact E2|exact H]].
Qed.

Lemma halt_from k: final_check k = true -> halts tm c0.
Proof.
  intros Hk.
  destruct (final_check_spec k Hk) as (y & z & n & E1 & E2 & H).
  pose proof (iter_spec _ _ _ E1 init) as HP.
  inverts HP as HL Hc.
  destruct (LIncs_rec_spec _ _ _ _ _ _ E2 HL) as [z' [n' [I1 [I2 I3]]]].
  pose proof (doom_rec_spec _ _ _ (le_n _) H I2) as HD.
  eapply halts_evstep with (c' := Lmp z' <| RC ((n'+1)*2)).
  - unfold RC. apply HD.
  - eapply evstep_trans.
    1: exact Hc.
    apply Incs. exact I1.
Qed.

Lemma halt: halts tm c0.
Proof. exact (halt_from 192 final_check_ok). Qed.

(*
```
1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
  = SOBCv6 TM3 1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD--- with ours A B C D E F = TM3 B C A E D F

words (paper order)  W0 = 001   W1 = 111
lists                head first: x = x_0 x_1 ... x_(k-1), x_0 next to the head
Lmp(x)               0^inf w(x_(k-1)) ... w(x_1) w(x_0)
RC(n)                1 (011)^n 01 0^inf
P(x)                 Lmp(x) <D 010 RC(1)
digits               W1 W0 = 0, W1 W1 = 1, a lone W0 = separator; lowest digit next to the head
count(x)             sum over the digit pairs p (p = 0 next to the head) of (1 - b_p) 2^p
ones(x)              x with every digit pair set to W1 W1

LInc     Lmp(x) <D 010 r           -->  Lmp(LInc x) 001 A> r
LOv      Lmp(x) <D 010 1 r         -->  Lmp(LOv x) A> r                       x in {W0, W1 W1}^n
Incs     Lmp(x) <D 010 RC(1)       -->  Lmp(ones x) <D 010 RC(c+1)            c = count(x) odd
Ov       Lmp(x) <D 010 RC(2m+2)    -->  Lmp((W1 W0)^m W1 W1 x') <D 010 RC(1)  LOv(x) = W0 x'
walk0    Lmp(x) 001 <D 010 1 r     -->  Lmp(x) <D 010 1 011 r                 (19 steps)
walk1    Lmp(x) 111 111 <D 010 1 r -->  Lmp(x) <D 010 1 010101 r              (12 steps)
far      Lmp(x_far) <D 010 1 r     -->  F reads 1 (halt)                      x_far = (W1 W1 W0)^5 (W1 W1)^3

LInc(W0 t) = W0 LInc(t)    LInc(W1 W0 t) = W1 W1 t    LInc(W1 W1 t) = W1 W0 LInc(t)
LOv([]) = W0 W1            LOv(W0 t) = W1 LOv(t)
LOv(W1 W1 t) = W0 W0 W1 v'          if LOv(t) = W0 v'
LOv(W1 W1 t) = W0 W0 W0 LInc(v')    if LOv(t) = W1 v'

blocks       W10 l = (W1 W0)^(1+l+n),  W11 l = (W1 W1)^(1+l+n),  n >= 0 free for each block
LInc_rec     W10 (l+1) t  ->  W1 W1 W10 l t
LOv_rec      W11 l t      ->  W0 W0 W10 l v'            if LOv_rec(t) = W0 W0 v'   (keep)
             W11 (l+1) t  ->  W0 W0 W10 l W0 LInc(v')   if LOv_rec(t) = W1 v'      (peel)
step_rec     x  ->  W10 (n-1) W1 W1 x2   where LIncs_rec x = (x0, n, 1), n >= 1, LOv_rec x0 = W0 x2

init     c0 -->(38,573) P(x2),  x2 = (W1 W0)^25 W1 W1 W0 W1 W0 W1 W0 W0 W1 W1 W0 W0 W0 W0 W1 W1 W1 W0 W1 W1
chain    x2 --(192 step_rec, bound 256)--> x194 (38,120 tokens)
halt     P(x194) --Incs--> Lmp(z) <D 010 RC(2N+2),  z = prefix ++ x_far,  prefix in {W0, W1 W1, W11 l}^n;
         walk0 / walk1 through the prefix, then far: F reads 1
```
*)