(** * 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF never halts

    Machine: 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF ("Bell eats counter").
    Adapted from verify/BECv5.v, Module TM1 / Module TM2 (same table except F1):
    the right side R n m, the right step and the standard counter are as there;
    the left side is a word W(e,o) (bit d of e on cell 2d, bit d of o on cell 2d+1),
    the left step is the relation PA/PF below, and the counter alternates between a
    standard and a packed encoding.  The informal proof is the accompanying write-up
    (proof.md); the macro rules S0..S3, P0..P4 and the invariant I are its 3.4 and 4.

    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 ZifyNat Lia.
Require Import ZArith.
Require Import String.

Open Scope list.

Definition tmP := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC").

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

Definition R n m := [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^(m) *> const 0.

(** ** Words W(e,o): bit d of e on cell 2d, bit d of o on cell 2d+1 (cell 0 is read by A) *)

Definition bt (x:nat) : Sym := if Nat.odd x then 1 else 0.

Fixpoint wd (n e o : nat) : list Sym :=
  match n with
  | O => []
  | S n' => bt e :: bt o :: wd n' (Nat.div2 e) (Nat.div2 o)
  end.

Definition WS e o : side := wd (e+o) e o *> const 0.

Lemma bt_even e: bt (2*e) = 0.
Proof. unfold bt. rewrite Nat.odd_even. reflexivity. Qed.

Lemma bt_odd e: bt (2*e+1) = 1.
Proof. unfold bt. rewrite Nat.odd_odd. reflexivity. Qed.

Lemma div2_even e: Nat.div2 (2*e) = e.
Proof. apply Nat.div2_double. Qed.

Lemma div2_odd e: Nat.div2 (2*e+1) = e.
Proof. rewrite Nat.add_1_r. apply Nat.div2_succ_double. Qed.

Lemma wd_pad n: forall e o k,
  e < 2^n -> o < 2^n ->
  wd (n+k) e o *> const 0 = wd n e o *> const 0.
Proof.
  induction n; intros e o k He Ho.
  - cbn in He,Ho. assert (e=0)%nat by lia. assert (o=0)%nat by lia. subst.
    cbn. induction k.
    + reflexivity.
    + change (wd (S k) 0 0) with (0 :: 0 :: wd k 0 0). cbn [Str_app]. rewrite IHk. rewrite <-!const_unfold. reflexivity.
  - cbn [wd Nat.add Str_app]. f_equal. f_equal.
    apply IHn.
    + rewrite Nat.div2_div. cbn in He. apply Nat.Div0.div_lt_upper_bound; lia.
    + rewrite Nat.div2_div. cbn in Ho. apply Nat.Div0.div_lt_upper_bound; lia.
Qed.

Lemma lt_pow2_self x: x < 2^x.
Proof. apply Nat.pow_gt_lin_r. lia. Qed.

Lemma wd_WS n e o:
  e < 2^n -> o < 2^n ->
  wd n e o *> const 0 = WS e o.
Proof.
  intros He Ho. unfold WS.
  assert (e < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). pose proof (Nat.pow_le_mono_r 2 e (e+o)). lia. }
  assert (o < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). lia. }
  destruct (Nat.le_ge_cases n (e+o)) as [H1|H1].
  - replace (e+o) with (n+(e+o-n)) by lia. rewrite wd_pad; auto.
  - replace n with ((e+o)+(n-(e+o))) by lia. rewrite wd_pad; auto.
Qed.

Lemma WS_split e o:
  WS e o = [bt e; bt o] *> WS (Nat.div2 e) (Nat.div2 o).
Proof.
  rewrite <-(wd_WS (S (e+o)) e o).
  2,3: pose proof (lt_pow2_self (e+o)); pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))); lia.
  cbn [wd Str_app].
  rewrite (wd_WS (e+o)). 1: reflexivity.
  - rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound.
    pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia.
  - rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound.
    pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia.
Qed.

Lemma WS_00 e o: WS (2*e) (2*o) = [0;0] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_even, div2_even, div2_even. reflexivity. Qed.
Lemma WS_10 e o: WS (2*e+1) (2*o) = [1;0] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed.
Lemma WS_01 e o: WS (2*e) (2*o+1) = [0;1] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed.
Lemma WS_11 e o: WS (2*e+1) (2*o+1) = [1;1] *> WS e o.
Proof. rewrite WS_split, bt_odd, bt_odd, div2_odd, div2_odd. reflexivity. Qed.

Lemma WS_0x e o: WS (2*e) o = [0; bt o] *> WS e (Nat.div2 o).
Proof. rewrite WS_split, bt_even, div2_even. reflexivity. Qed.
Lemma WS_1x e o: WS (2*e+1) o = [1; bt o] *> WS e (Nat.div2 o).
Proof. rewrite WS_split, bt_odd, div2_odd. reflexivity. Qed.

(** ** The left step phi, as a relation (A scanning an E-cell / F scanning an E-cell) *)

Inductive PA : nat -> nat -> nat -> nat -> Prop :=
| PA0 e o : PA (2*e) o (2*e+1) o
| PA1 e o e' o' : PA e o e' o' -> PA (2*e+1) (2*o) (2*e') (2*o')
| PA2 e o e' o' : PF e o e' o' -> PA (2*e+1) (2*o+1) (2*e') (2*o')
with PF : nat -> nat -> nat -> nat -> Prop :=
| PF0 e o : PF (2*e) (2*o) (2*e) (2*o+1)
| PF1 e o e' o' : PF e o e' o' -> PF (2*e) (2*o+1) (2*e') (2*o')
| PF2 e o e' o' : PA e o e' o' -> PF (2*e+1) (2*o) (2*e') (2*o')
| PF3 e o e' o' : PF e o e' o' -> PF (2*e+1) (2*o+1) (2*e') (2*o').

Scheme PA_mind := Induction for PA Sort Prop
with PF_mind := Induction for PF Sort Prop.
Combined Scheme PAF_mind from PA_mind, PF_mind.

Lemma TA0 l a r: [0;a] *> l <{{A}} r -->+ [1;a] *> l {{B}}> r.
Proof. es. Qed.
Lemma TA1 l r: [1;0] *> l <{{A}} r -->+ l <{{A}} [1;1] *> r.
Proof. es. Qed.
Lemma TA2 l r: [1;1] *> l <{{A}} r -->+ l <{{F}} [1;1] *> r.
Proof. es. Qed.
Lemma TF0 l r: [0;0] *> l <{{F}} r -->+ [0;1] *> l {{B}}> r.
Proof. es. Qed.
Lemma TF1 l r: [0;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r.
Proof. es. Qed.
Lemma TF2 l r: [1;0] *> l <{{F}} [1] *> r -->+ l <{{A}} [1;1] *> [1] *> r.
Proof. es. Qed.
Lemma TF3 l r: [1;1] *> l <{{F}} [1] *> r -->+ l <{{F}} [1;1] *> [1] *> r.
Proof. es. Qed.
Lemma TB l r: l {{B}}> [1;1] *> r -->+ [0;0] *> l {{B}}> r.
Proof. es. Qed.

Lemma phi_spec:
  (forall e o e' o', PA e o e' o' -> forall r, WS e o <{{A}} r -->+ WS e' o' {{B}}> r) /\
  (forall e o e' o', PF e o e' o' -> forall r, WS e o <{{F}} [1] *> r -->+ WS e' o' {{B}}> [1] *> r).
Proof.
  apply PAF_mind.
  all: intros.
  all: try (rewrite WS_0x, WS_1x; apply TA0).
  all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TA1|]; eapply progress_trans; [apply H|]; apply TB).
  all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TA2|]; eapply progress_trans; [apply (H ([1] *> r))|]; apply TB).
  all: try (rewrite WS_00, WS_01; apply TF0).
  all: try (rewrite WS_01, WS_00; eapply progress_trans; [apply TF1|]; eapply progress_trans; [apply (H ([1] *> [1] *> r))|]; apply (TB _ ([1] *> r))).
  all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TF2|]; eapply progress_trans; [apply H|]; apply (TB _ ([1] *> r))).
  all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TF3|]; eapply progress_trans; [apply (H ([1] *> [1] *> r))|]; apply (TB _ ([1] *> r))).
Qed.

Definition PA_spec := proj1 phi_spec.

(** ** Iterates, shape lemmas *)

Inductive PAs : nat -> nat -> nat -> nat -> nat -> Prop :=
| PAs0 e o : PAs 0 e o e o
| PAsS j e o e1 o1 e2 o2 : PA e o e1 o1 -> PAs j e1 o1 e2 o2 -> PAs (S j) e o e2 o2.

Lemma PA_eq e o e' o' e2 o2 e2' o2':
  PA e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PA e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PF_eq e o e' o' e2 o2 e2' o2':
  PF e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PF e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PAs_eq j e o e' o' j2 e2 o2 e2' o2':
  PAs j e o e' o' -> j = j2 -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PAs j2 e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PAs_1 e o e' o': PA e o e' o' -> PAs 1 e o e' o'.
Proof. intros. econstructor; eauto. constructor. Qed.

Lemma PAs_trans j1 j2 e o e1 o1 e2 o2:
  PAs j1 e o e1 o1 -> PAs j2 e1 o1 e2 o2 -> PAs (j1+j2) e o e2 o2.
Proof.
  induction 1; intros; cbn; auto.
  econstructor; eauto.
Qed.

Lemma PAs_split j1 j2 e o e2 o2:
  PAs (j1+j2) e o e2 o2 -> exists e1 o1, PAs j1 e o e1 o1 /\ PAs j2 e1 o1 e2 o2.
Proof.
  gen e o. induction j1; intros e o H.
  - exists e, o. split; [constructor|auto].
  - cbn in H. inversion H; subst.
    destruct (IHj1 _ _ H2) as [e3 [o3 [H3 H4]]].
    exists e3, o3. split; auto. econstructor; eauto.
Qed.

Lemma PAs_dbl j e o e' o':
  PAs j e o e' o' -> PAs (2*j) (2*e) (2*o) (2*e') (2*o').
Proof.
  induction 1.
  - constructor.
  - replace (2 * S j) with (S (S (2*j))) by lia.
    econstructor. 1: apply PA0.
    econstructor. 1: apply PA1; eassumption.
    assumption.
Qed.

Lemma PAs_dbl1 j e o e' o':
  PAs (S j) e o e' o' -> PAs (2*j+1) (2*e+1) (2*o) (2*e') (2*o').
Proof.
  intros H. inversion H; subst.
  replace (2*j+1) with (S (2*j)) by lia.
  econstructor. 1: apply PA1; eassumption.
  apply PAs_dbl; assumption.
Qed.

(** ** Increments *)

Lemma INC_std N: PA N 0 (N+1) 0.
Proof.
  induction N as [N IH] using lt_wf_ind.
  destruct (Nat.Even_or_Odd N) as [[N' HN]|[N' HN]]; subst N.
  - eapply PA_eq. 1: apply (PA0 N' 0). all: lia.
  - eapply PA_eq. 1: apply (PA1 N' 0 (N'+1) 0), IH. all: lia.
Qed.

Lemma INC_stds j N: PAs j N 0 (N+j) 0.
Proof.
  gen N. induction j; intros N.
  - eapply PAs_eq. 1: apply (PAs0 N 0). all: lia.
  - econstructor. 1: apply INC_std.
    eapply PAs_eq. 1: apply (IHj (N+1)). all: lia.
Qed.

Lemma PF_inc0 o: PF 0 o 0 (o+1).
Proof.
  induction o as [o IH] using lt_wf_ind.
  destruct (Nat.Even_or_Odd o) as [[o' Ho]|[o' Ho]]; subst o.
  - eapply PF_eq. 1: apply (PF0 0 o'). all: lia.
  - eapply PF_eq. 1: apply (PF1 0 o' 0 (o'+1)), IH. all: lia.
Qed.

Lemma Gap P: forall c E o1,
  c+1 < 2^(S P) ->
  PA (c + 2^(S P)*E) (2^P*(2*o1+1)) (c + 1 + 2^(S P)*E) (2^P*(2*o1+1)).
Proof.
  induction P; intros c E o1 Hc.
  - cbn in *. eapply PA_eq. 1: apply (PA0 E (2*o1+1)). all: lia.
  - rewrite !Nat.pow_succ_r' in *.
    destruct (Nat.Even_or_Odd c) as [[c' Hc']|[c' Hc']]; subst c.
    + eapply PA_eq. 1: apply (PA0 (c' + 2*2^P*E) (2*2^P*(2*o1+1))). all: lia.
    + eapply PA_eq. 1: apply (PA1 (c' + 2*2^P*E) (2^P*(2*o1+1)) (c'+1+2*2^P*E) (2^P*(2*o1+1))), IHP.
      all: lia.
Qed.

Lemma Gaps P j: forall c E o1,
  c+j < 2^(S P) ->
  PAs j (c + 2^(S P)*E) (2^P*(2*o1+1)) (c + j + 2^(S P)*E) (2^P*(2*o1+1)).
Proof.
  induction j; intros c E o1 Hc.
  - eapply PAs_eq. 1: apply (PAs0 (c + 2^(S P)*E) (2^P*(2*o1+1))). all: lia.
  - econstructor. 1: apply Gap; lia.
    eapply PAs_eq. 1: apply (IHj (c+1) E o1). all: lia.
Qed.

Lemma F_inc h: forall E o O,
  o + 1 < 2^h ->
  PF (2^h*E) (o + 2^h*O) (2^h*E) (o + 1 + 2^h*O).
Proof.
  induction h; intros E o O Ho.
  - cbn in Ho. lia.
  - rewrite !Nat.pow_succ_r' in *.
    destruct (Nat.Even_or_Odd o) as [[o' Ho']|[o' Ho']]; subst o.
    + eapply PF_eq. 1: apply (PF0 (2^h*E) (o' + 2^h*O)). all: lia.
    + eapply PF_eq. 1: apply (PF1 (2^h*E) (o' + 2^h*O) (2^h*E) (o'+1+2^h*O)), IHh.
      all: lia.
Qed.

Lemma F_carry h: forall E O E' O',
  PF E O E' O' ->
  PF (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O').
Proof.
  induction h; intros E O E' O' H.
  - cbn. eapply PF_eq. 1: apply H. all: lia.
  - rewrite !Nat.pow_succ_r' in *.
    pose proof (Nat.pow_nonzero 2 h).
    eapply PF_eq. 1: apply (PF1 (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O')), IHh, H.
    all: lia.
Qed.


Lemma lowbit (x:nat): x <> 0%nat -> exists P o, x = 2^P*(2*o+1).
Proof.
  induction x as [x IH] using lt_wf_ind. intros Hx.
  destruct (Nat.Even_or_Odd x) as [[x' Hx']|[x' Hx']]; subst x.
  - destruct (IH x') as [P [o Ho]]; [lia|lia|].
    exists (S P), o. rewrite Nat.pow_succ_r'. lia.
  - exists 0%nat, x'. cbn. lia.
Qed.

Lemma pow_pos P: 1 <= 2^P.
Proof. pose proof (Nat.pow_nonzero 2 P). lia. Qed.

Lemma pow_odd_pos P o1: 2^P <= 2^P*(2*o1+1).
Proof. replace (2^P) with (2^P*1) at 1 by lia. apply Nat.mul_le_mono_l. lia. Qed.

Lemma pow_odd_room P o1 h: 2^P*(2*o1+1) < 2^h -> 2^P*(2*o1+1) + 2^P <= 2^h.
Proof.
  intros H.
  pose proof (pow_pos P). pose proof (pow_odd_pos P o1).
  assert (P < h). {
    destruct (Nat.lt_ge_cases P h) as [|H2]; auto.
    pose proof (Nat.pow_le_mono_r 2 h P ltac:(lia) H2). lia. }
  replace (2^h) with (2^P * 2^(h-P)) in *.
  2: { rewrite <-Nat.pow_add_r. f_equal. lia. }
  assert (2*o1+1 < 2^(h-P)). { apply (Nat.mul_lt_mono_pos_l (2^P)); lia. }
  replace (2^P*(2*o1+1) + 2^P) with (2^P*(2*o1+2)) by lia.
  apply Nat.mul_le_mono_l. lia.
Qed.

(** The sweep: a low part (c, o) of h digit pairs, o = 2^P(2 o1+1), c < 2^(P+1), counts its
    T-count 2o+c up to 2^(h+1); then the carry enters the high part (E,O) in F mode. *)
Lemma Sweep h: forall P o1 c E O E' O',
  2^P*(2*o1+1) < 2^h -> c < 2^(S P) -> PF E O E' O' ->
  PAs (2^(S h) - 2^(S P)*(2*o1+1) - c) (c + 2^h*E) (2^P*(2*o1+1) + 2^h*O) (2^h*E') (2^h*O').
Proof.
  induction h; intros P o1 c E O E' O' Ho Hc HF.
  - pose proof (pow_odd_pos P o1). cbn in Ho. lia.
  - destruct P as [|P'].
    + (* o odd *)
      cbn [Nat.pow] in *. rewrite Nat.mul_1_l in *.
      assert (H1: PAs (2^(S (S h)) - 2*(2*o1+1) - 1) (1 + 2^(S h)*E) ((2*o1+1) + 2^(S h)*O) (2^(S h)*E') (2^(S h)*O')).
      { rewrite !Nat.pow_succ_r' in *.
        destruct (Nat.eq_dec (o1+1) (2^h)) as [Eo|Eo].
        - apply PAs_eq with 1%nat (2*(2^h*E)+1)%nat (2*(2^h - 1 + 2^h*O)+1)%nat (2*(2^h*E'))%nat (2*(2^h*O'))%nat.
          + apply PAs_1. apply PA2. apply F_carry. assumption.
          + lia.
          + lia.
          + lia.
          + lia.
          + lia.
        - destruct (lowbit (o1+1)) as [P2 [o2 Ho2]]; [lia|].
          pose proof (IHh P2 o2 0%nat E O E' O') as IH.
          try rewrite Nat.pow_succ_r' in IH.
          rewrite <-Ho2 in IH.
          specialize (IH ltac:(lia) ltac:(pose proof (pow_pos P2); lia) HF).
          apply PAs_dbl in IH.
          apply PAs_eq with (1 + 2 * (2 * 2 ^ h - 2 * 2 ^ P2 * (2 * o2 + 1) - 0))%nat (2*(2^h*E)+1)%nat (2*(o1 + 2^h*O)+1)%nat (2*(2^h*E'))%nat (2*(2^h*O'))%nat.
          + econstructor. 1: apply PA2, F_inc; lia.
            eapply PAs_eq. 1: apply IH. all: lia.
          + lia.
          + lia.
          + lia.
          + lia.
          + lia. }
      destruct (Nat.eq_dec c 1%nat) as [->|Hc1].
      * exact H1.
      * assert (c = 0%nat) as -> by lia.
        apply PAs_eq with (1 + (2^(S (S h)) - 2*(2*o1+1) - 1))%nat (0 + 2^(S h)*E)%nat (2*o1+1+2^(S h)*O)%nat (2^(S h)*E')%nat (2^(S h)*O')%nat.
        -- econstructor. 2: apply H1.
           rewrite Nat.pow_succ_r'. eapply PA_eq. 1: apply (PA0 (2^h*E) (2*o1+1+2*2^h*O)). all: lia.
        -- rewrite !Nat.pow_succ_r' in *. lia.
        -- rewrite !Nat.pow_succ_r' in *. lia.
        -- rewrite !Nat.pow_succ_r' in *. lia.
        -- rewrite !Nat.pow_succ_r' in *. lia.
        -- rewrite !Nat.pow_succ_r' in *. lia.
    + (* o even *)
      rewrite (Nat.pow_succ_r' 2 (S P')) in *.
      rewrite (Nat.pow_succ_r' 2 P') in *.
      rewrite (Nat.pow_succ_r' 2 (S h)) in *.
      rewrite (Nat.pow_succ_r' 2 h) in *.
      destruct (Nat.Even_or_Odd c) as [[c' Hc']|[c' Hc']]; subst c.
      * pose proof (IHh P' o1 c' E O E' O') as IH.
        try rewrite !Nat.pow_succ_r' in IH.
        specialize (IH ltac:(lia) ltac:(lia) HF).
        apply PAs_dbl in IH.
        eapply PAs_eq. 1: apply IH. all: lia.
      * pose proof (IHh P' o1 c' E O E' O') as IH.
        try rewrite !Nat.pow_succ_r' in IH.
        specialize (IH ltac:(lia) ltac:(lia) HF).
        pose proof (pow_odd_pos P' o1).
        pose proof (pow_odd_room P' o1 h ltac:(lia)).
        remember (2 * 2 ^ h - 2 * 2 ^ P' * (2 * o1 + 1) - c') as n eqn:En.
        destruct n as [|n']. 1: lia.
        apply PAs_dbl1 in IH.
        eapply PAs_eq. 1: apply IH. all: lia.
Qed.

(** ** The right step and the overflows *)

Lemma RS l n m:
  l {{B}}> R (S n) m -->+ l <{{A}} R n (S m).
Proof.
  unfold R. es.
Qed.

Lemma shift01 u (r:side): [0;1]^^u *> [0] *> r = [0] *> [1;0]^^u *> r.
Proof.
  induction u.
  - reflexivity.
  - cbn [lpow]. rewrite !Str_app_assoc. rewrite IHu. reflexivity.
Qed.

Lemma OVe l u m:
  ([0;0]^^u *> [1] *> l) {{B}}> R 0 m -->+ l <{{A}} R (1+u+m) 0.
Proof.
  unfold R. es.
Qed.

Lemma OVo l u m:
  ([0;0]^^u *> [0;1;0;0] *> l) {{B}}> R 0 m -->+ l <{{A}} R 0 (u+2+m).
Proof.
  unfold R. es.
Qed.

Definition K e o n m := WS e o <{{A}} R n m.

(** ** Words on the tape *)

Lemma WS_shift: forall n a c, a + c < n -> WS a c = [bt a] *> WS c (Nat.div2 a).
Proof.
  induction n; intros a c Hn. 1: lia.
  destruct (Nat.eq_dec (a+c) 0%nat) as [E|E].
  - assert (a = 0%nat) as -> by lia. assert (c = 0%nat) as -> by lia.
    unfold WS. cbn. rewrite <-const_unfold. reflexivity.
  - rewrite WS_split. rewrite (WS_split c).
    rewrite (IHn (Nat.div2 a) (Nat.div2 c)).
    + reflexivity.
    + rewrite !Nat.div2_div.
      pose proof (Nat.Div0.div_le_upper_bound a 2 (a/2)).
      pose proof (Nat.div_mod a 2). pose proof (Nat.div_mod c 2).
      pose proof (Nat.mod_upper_bound a 2). pose proof (Nat.mod_upper_bound c 2). lia.
Qed.

Lemma WS_1 a c: WS (2*a+1) c = [1] *> WS c a.
Proof.
  rewrite (WS_shift (S (2*a+1+c))) by lia. rewrite bt_odd, div2_odd. reflexivity.
Qed.

Lemma WS_pow x y u: WS (x*2^u) (y*2^u) = [0;0]^^u *> WS x y.
Proof.
  induction u.
  - cbn. rewrite !Nat.mul_1_r. reflexivity.
  - rewrite Nat.pow_succ_r'.
    replace (x*(2*2^u)) with (2*(x*2^u)) by lia.
    replace (y*(2*2^u)) with (2*(y*2^u)) by lia.
    rewrite WS_00, IHu. cbn [lpow]. rewrite Str_app_assoc. reflexivity.
Qed.

(** ** Composite rules on K configurations *)

Lemma bounces j e o e' o' n m:
  PAs j e o e' o' -> K e o (j+n) m -->* K e' o' n (j+m).
Proof.
  intros H. gen n m. induction H; intros n m.
  - finish.
  - apply evstep_trans with (K e1 o1 (j+n) (S m)).
    + apply progress_evstep. unfold K.
      eapply progress_trans. 1: apply PA_spec; eassumption.
      cbn [Nat.add]. apply RS.
    + eapply evstep_trans. 1: apply IHPAs. finish.
Qed.

Lemma OV_even e o a c u m:
  PA e o ((2*a+1)*2^u) (c*2^u) -> K e o 0 m -->+ K c a (1+u+m) 0.
Proof.
  intros H. unfold K.
  eapply progress_trans. 1: apply PA_spec, H.
  rewrite WS_pow, WS_1.
  apply OVe.
Qed.

Lemma OV_odd e o a c u m:
  PA e o (c*2^(u+2)) ((4*a+1)*2^u) -> K e o 0 m -->+ K c a 0 (u+2+m).
Proof.
  intros H. unfold K.
  eapply progress_trans. 1: apply PA_spec, H.
  replace (c*2^(u+2)) with ((2*(2*c))*2^u) by (rewrite Nat.pow_add_r; cbn; lia).
  replace (4*a+1) with (2*(2*a)+1) by lia.
  rewrite WS_pow, WS_01, WS_00.
  apply OVo.
Qed.

(** ** Packed counter *)

Definition pkE N := N - 2^(Nat.log2 N).
Definition pkO N := 2^(Nat.log2 N - 1).

Lemma pk_eq P N: 2^(S P) <= N < 2^(S (S P)) -> pkE N = N - 2^(S P) /\ pkO N = 2^P.
Proof.
  intros H. unfold pkE, pkO.
  rewrite (Nat.log2_unique N (S P)); [|lia|lia].
  split; [reflexivity|]. f_equal. lia.
Qed.

Lemma PAs_1_inv e o e2 o2: PAs 1 e o e2 o2 -> PA e o e2 o2.
Proof.
  intros H. inversion H as [|j' e' o' e1 o1 e3 o3 HA HB]; subst.
  inversion HB; subst. assumption.
Qed.

Lemma PAs_last j e o e2 o2:
  PAs (S j) e o e2 o2 -> exists e1 o1, PAs j e o e1 o1 /\ PA e1 o1 e2 o2.
Proof.
  intros H. replace (S j) with (j+1) in H by lia.
  destruct (PAs_split _ _ _ _ _ _ H) as [e1 [o1 [H1 H2]]].
  exists e1, o1. split; auto. apply PAs_1_inv, H2.
Qed.

Lemma INC_pk N: 2 <= N -> PA (pkE N) (pkO N) (pkE (S N)) (pkO (S N)).
Proof.
  intros HN.
  pose proof (Nat.log2_spec N ltac:(lia)) as HL.
  assert (Hl1: 1 <= Nat.log2 N). { pose proof (Nat.log2_le_mono 2 N HN) as Hm. cbn in Hm. lia. }
  remember (Nat.log2 N - 1) as P.
  replace (Nat.log2 N) with (S P) in HL by lia.
  destruct (pk_eq P N HL) as [E1 E2]. rewrite E1, E2.
  rewrite (Nat.pow_succ_r' 2 (S P)) in HL.
  destruct (Nat.eq_dec (S N) (2^(S (S P)))) as [Ec|Ec].
  - destruct (pk_eq (S P) (S N)) as [E3 E4].
    { rewrite ?Nat.pow_succ_r' in *. lia. }
    rewrite E3, E4.
    pose proof (Sweep (S P) P 0 (2^(S P) - 1) 0 0 0 1) as H.
    specialize (H ltac:(rewrite ?Nat.pow_succ_r' in *; lia) ltac:(lia) (PF0 0 0)).
    apply PAs_1_inv.
    eapply PAs_eq. 1: apply H. all: rewrite ?Nat.pow_succ_r' in *; lia.
  - destruct (pk_eq P (S N)) as [E3 E4].
    { rewrite ?Nat.pow_succ_r' in *. lia. }
    rewrite E3, E4.
    pose proof (Gap P (N - 2^(S P)) 0 0) as H.
    specialize (H ltac:(rewrite ?(Nat.pow_succ_r' 2 (S P)) in *; lia)).
    eapply PA_eq. 1: apply H. all: lia.
Qed.

Lemma INC_pks j N: 2 <= N -> PAs j (pkE N) (pkO N) (pkE (N+j)) (pkO (N+j)).
Proof.
  gen N. induction j; intros N HN.
  - eapply PAs_eq. 1: apply (PAs0 (pkE N) (pkO N)). all: f_equal; lia.
  - econstructor. 1: apply INC_pk; lia.
    eapply PAs_eq. 1: apply (IHj (S N)); lia. all: f_equal; lia.
Qed.

(** ** Macro rules (proof.md 3.4).  l is bitlen(k)-1, b = 1+i+m. *)

Lemma bounces0 j e o e' o' m:
  PAs j e o e' o' -> K e o j m -->* K e' o' 0 (j+m).
Proof.
  intros H. pose proof (bounces j e o e' o' 0 m H) as H1.
  rewrite Nat.add_0_r in H1. exact H1.
Qed.

Lemma OVB e o a c u m e' o':
  PA e o ((2*a+1)*2^u) (c*2^u) ->
  PAs (1+u+m) c a e' o' ->
  K e o 0 m -->+ K e' o' 0 (1+u+m).
Proof.
  intros H1 H2. eapply progress_evstep_trans. 1: apply OV_even, H1.
  eapply evstep_trans. 1: apply bounces0, H2.
  finish.
Qed.

Lemma std_ov k i: PA ((2*k+1)*2^i-1) 0 ((2*k+1)*2^i) (0*2^i).
Proof.
  pose proof (pow_pos i).
  eapply PA_eq. 1: apply (INC_std ((2*k+1)*2^i-1)). all: nia.
Qed.

Lemma BS_S0 i m: K (2^i-1) 0 0 m -->+ K (1+i+m) 0 0 (1+i+m).
Proof.
  apply OVB with (a:=0%nat) (c:=0%nat).
  - pose proof (std_ov 0 i). eapply PA_eq. 1: apply H. all: lia.
  - eapply PAs_eq. 1: apply (INC_stds (1+i+m) 0). all: lia.
Qed.

Lemma OVoS0 e o u m: PA e o 0 (2^u) -> K e o 0 m -->+ K (u+3+m) 0 0 (u+3+m).
Proof.
  intros H.
  eapply progress_trans. 1: apply (OV_odd e o 0 0 u m).
  - eapply PA_eq. 1: apply H. all: lia.
  - pose proof (BS_S0 0 (u+2+m)) as H1. cbn in H1.
    eapply progress_evstep_trans. 1: apply H1. finish.
Qed.

Lemma BS_S1a l k i m:
  k = 2^l ->
  K ((2*k+1)*2^i-1) 0 0 m -->+ K (pkE (2*k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m).
Proof.
  intros Hk.
  apply OVB with (a:=k) (c:=0%nat).
  1: apply std_ov.
  destruct (pk_eq l (2^(S l))) as [E1 E2].
  { rewrite !Nat.pow_succ_r'. pose proof (pow_pos l). lia. }
  eapply PAs_eq. 1: apply (INC_pks (1+i+m) (2^(S l))).
  - rewrite Nat.pow_succ_r'. pose proof (pow_pos l). lia.
  - reflexivity.
  - rewrite E1. lia.
  - rewrite E2. lia.
  - f_equal. rewrite Nat.pow_succ_r'. lia.
  - f_equal. rewrite Nat.pow_succ_r'. lia.
Qed.

(** sweep of W(0,k), k < 2^(l+1), into pk(2^(l+2)) *)
Lemma O3_merge l k:
  1 <= k < 2^(S l) ->
  PAs (2^(S (S l)) - 2*k) 0 k (pkE (2^(S (S l)))) (pkO (2^(S (S l)))).
Proof.
  intros Hk.
  destruct (lowbit k) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep (S l) P o1 0 0 0 0 1) as H.
  specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF0 0 0)).
  destruct (pk_eq (S l) (2^(S (S l)))) as [E1 E2].
  { rewrite !(Nat.pow_succ_r' 2 (S _)). pose proof (pow_pos (S l)). lia. }
  rewrite E1, E2.
  eapply PAs_eq. 1: apply H. all: rewrite ?Nat.pow_succ_r' in *; lia.
Qed.

Lemma BS_S1b l k i m:
  2^l <= k < 2^(S l) ->
  2^(S (S l)) <= 2*k+(1+i+m) ->
  K ((2*k+1)*2^i-1) 0 0 m -->+ K (pkE (2*k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m).
Proof.
  intros Hk Hb.
  pose proof (pow_pos l).
  apply OVB with (a:=k) (c:=0%nat).
  1: apply std_ov.
  pose proof (O3_merge l k ltac:(lia)) as H1.
  pose proof (INC_pks (2*k+(1+i+m)-2^(S (S l))) (2^(S (S l)))) as H2.
  specialize (H2 ltac:(rewrite !Nat.pow_succ_r'; lia)).
  pose proof (PAs_trans _ _ _ _ _ _ _ _ H1 H2) as H3.
  eapply PAs_eq. 1: apply H3. all: try reflexivity.
  - rewrite !(Nat.pow_succ_r' 2 (S _)) in *. rewrite !Nat.pow_succ_r' in *. lia.
  - f_equal. lia.
  - f_equal. lia.
Qed.

Lemma BS_S2 l k i m:
  2^l <= k < 2^(S l) ->
  2*k+(1+i+m)+1 = 2^(S (S l)) ->
  K ((2*k+1)*2^i-1) 0 0 m -->+ K (l+4+(1+i+m)) 0 0 (l+4+(1+i+m)).
Proof.
  intros Hk Hb.
  pose proof (pow_pos l).
  pose proof (O3_merge l k ltac:(lia)) as H1.
  destruct (pk_eq (S l) (2^(S (S l)))) as [E1 E2].
  { rewrite !(Nat.pow_succ_r' 2 (S _)). pose proof (pow_pos (S l)). lia. }
  rewrite E1, E2 in H1.
  replace (2 ^ S (S l) - 2 * k) with (S (1+i+m)) in H1 by lia.
  destruct (PAs_last _ _ _ _ _ H1) as [e1 [o1 [H2 H3]]].
  eapply progress_trans. 1: apply OV_even with (a:=k) (c:=0%nat) (u:=i), std_ov.
  eapply evstep_progress_trans. 1: apply bounces0, H2.
  eapply progress_evstep_trans. 1: apply (OVoS0 _ _ (S l)).
  - eapply PA_eq. 1: apply H3. all: lia.
  - finish.
Qed.

Lemma pk_ov_full i: 2 <= i ->
  PA (pkE (2^i-1)) (pkO (2^i-1)) 0 (2^(i-1)).
Proof.
  intros Hi.
  pose proof (INC_pk (2^i-1)) as H.
  assert (4 <= 2^i). { pose proof (Nat.pow_le_mono_r 2 2 i ltac:(lia) Hi). cbn in H0. lia. }
  specialize (H ltac:(lia)).
  replace (S (2^i-1)) with (2^i) in H by lia.
  destruct (pk_eq (i-1) (2^i)) as [E1 E2].
  { replace (S (i-1)) with i by lia. split; [lia | apply Nat.pow_lt_mono_r; lia]. }
  rewrite E1, E2 in H.
  eapply PA_eq. 1: apply H. all: try reflexivity.
  replace (S (i-1)) with i by lia. lia.
Qed.

Lemma BS_P0 i m: 2 <= i ->
  K (pkE (2^i-1)) (pkO (2^i-1)) 0 m -->+ K (2+i+m) 0 0 (2+i+m).
Proof.
  intros Hi.
  eapply progress_evstep_trans. 1: apply (OVoS0 _ _ (i-1)), pk_ov_full, Hi.
  finish.
Qed.

(** pk(N) with N+1 = (2k+1) 2^i, 2^l <= k < 2^(l+1), k = 2^l + r: overflow gives W(2^l, r) *)
Lemma pk_ov l r i:
  r < 2^l ->
  PA (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) ((2*r+1)*2^i) (2^l*2^i).
Proof.
  intros Hr.
  pose proof (pow_pos l). pose proof (pow_pos i).
  destruct (pk_eq (l+i) ((2*(2^l+r)+1)*2^i-1)) as [E1 E2].
  { rewrite !Nat.pow_succ_r', Nat.pow_add_r. nia. }
  rewrite E1, E2.
  pose proof (Gap (l+i) ((2*r+1)*2^i-1) 0 0) as HG.
  specialize (HG ltac:(rewrite !Nat.pow_succ_r', Nat.pow_add_r; nia)).
  eapply PA_eq. 1: apply HG.
  all: rewrite ?Nat.pow_succ_r', ?Nat.pow_add_r; nia.
Qed.

Lemma BS_P1 l i m:
  K (pkE ((2*(2^l+0)+1)*2^i-1)) (pkO ((2*(2^l+0)+1)*2^i-1)) 0 m -->+ K (2^l+(1+i+m)) 0 0 (1+i+m).
Proof.
  apply OVB with (a:=0%nat) (c:=2^l).
  1: apply pk_ov; apply pow_pos.
  eapply PAs_eq. 1: apply (INC_stds (1+i+m) (2^l)). all: lia.
Qed.

Lemma BS_P2 l r i m:
  1 <= r < 2^l ->
  2^(S l) <= 2*r+(1+i+m) ->
  K (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) 0 m -->+ K (2*r+(1+i+m)) 0 0 (1+i+m).
Proof.
  intros Hr Hb.
  apply OVB with (a:=r) (c:=2^l).
  1: apply pk_ov; lia.
  destruct (lowbit r) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep l P o1 0 1 0 2 0) as H.
  specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
  specialize (H (PF2 0 0 1 0 (PA0 0 0))).
  rewrite !Nat.mul_0_r in H.
  pose proof (INC_stds (2*r+(1+i+m)-2^(S l)) (2^l*2)) as H2.
  pose proof (PAs_trans _ _ _ _ _ _ _ _ H H2) as H3.
  eapply PAs_eq. 1: apply H3. all: rewrite ?Nat.pow_succ_r' in *; lia.
Qed.

Lemma BS_P3 l r i m:
  1 <= r < 2^l ->
  2*r+(1+i+m)+1 = 2^(S l) ->
  K (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) 0 m -->+ K (l+2+(1+i+m)) 0 0 (l+2+(1+i+m)).
Proof.
  intros Hr Hb.
  destruct (lowbit r) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep l P o1 0 1 0 2 0) as H.
  specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
  specialize (H (PF2 0 0 1 0 (PA0 0 0))).
  replace (2 ^ S l - 2 ^ S P * (2 * o1 + 1) - 0) with (S (1+i+m)) in H by (rewrite ?Nat.pow_succ_r' in *; lia).
  destruct (PAs_last _ _ _ _ _ H) as [e1 [o1' [H2 H3]]].
  eapply progress_trans. 1: apply OV_even with (a:=r) (c:=2^l) (u:=i), pk_ov; lia.
  eapply evstep_progress_trans.
  1: { eapply bounces0. eapply PAs_eq. 1: apply H2. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
  eapply progress_evstep_trans. 1: apply OV_even with (a:=0%nat) (c:=0%nat) (u:=S l).
  - eapply PA_eq. 1: apply H3. all: rewrite ?Nat.pow_succ_r' in *; lia.
  - eapply evstep_trans. 1: apply bounces0, (INC_stds _ 0).
    finish.
Qed.

Lemma PAs_trans_eq j1 j2 e o e1 o1 e1' o1' e2 o2:
  PAs j1 e o e1 o1 -> PAs j2 e1' o1' e2 o2 -> e1 = e1' -> o1 = o1' -> PAs (j1+j2) e o e2 o2.
Proof. intros H1 H2 -> ->. eapply PAs_trans; eauto. Qed.

(** S3 / P4: the gen-1 orbit stops in its final gap at T = 2^(l+1) + v (resp. 2^l + v),
    v = 2^u (2g+1), l = S (h+u); the overflow then leaves the gen-2 word *)
Lemma S3_pre h u r g i m:
  1 <= r < 2^(h+u) -> g < 2^h ->
  2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) ->
  K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (3*2^h) g (1+u+(1+i+m)) 0.
Proof.
  intros Hr Hg Hb.
  pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu.
  assert (E1: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r.
  destruct (lowbit r) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep (h+u) P o1 0 0 2 0 3) as H1.
  specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF_inc0 2)).
  pose proof (Gaps (h+u) (2^u*(2*g+1)) 0 0 1) as H2.
  specialize (H2 ltac:(rewrite Nat.pow_succ_r', E1; nia)).
  pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(lia) ltac:(lia)) as H3.
  assert (Hj: (2 ^ S (h+u) - 2 ^ S P * (2 * o1 + 1) - 0) + 2^u*(2*g+1) = S (1+i+m)).
  { rewrite ?Nat.pow_succ_r' in *. lia. }
  rewrite Hj in H3.
  destruct (PAs_last _ _ _ _ _ H3) as [e1 [o2 [H4 H5]]].
  eapply progress_trans. 1: apply OV_even with (a:=(2^(S (h+u))+r)) (c:=0%nat) (u:=i), std_ov.
  eapply evstep_progress_trans.
  1: { eapply bounces0. eapply PAs_eq. 1: apply H4. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
  eapply progress_evstep_trans. 1: apply OV_even with (a:=g) (c:=3*2^h) (u:=u).
  - eapply PA_eq. 1: apply H5. all: rewrite ?Nat.pow_succ_r' in *; nia.
  - finish.
Qed.

Lemma BS_S3a h u r i m:
  1 <= r < 2^(h+u) ->
  2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u ->
  K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (3*2^h+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)).
Proof.
  intros Hr Hb.
  eapply progress_evstep_trans. 1: apply (S3_pre h u r 0 i m); [lia|apply pow_pos|lia].
  eapply evstep_trans. 1: apply bounces0, (INC_stds _ (3*2^h)).
  finish.
Qed.

Lemma BS_S3b h u r g i m:
  1 <= r < 2^(h+u) -> 1 <= g < 2^h ->
  2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) ->
  2^(S h) <= 2*g + (1+u+(1+i+m)) ->
  K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (2^(S h)+2*g+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)).
Proof.
  intros Hr Hg Hb Hn.
  eapply progress_evstep_trans. 1: apply (S3_pre h u r g i m); lia.
  destruct (lowbit g) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep h P o1 0 3 0 4 0) as H1.
  specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
  specialize (H1 (PF_eq _ _ _ _ _ _ _ _ (PF2 1 0 2 0 (PA_eq _ _ _ _ _ _ _ _ (PA1 0 0 1 0 (PA0 0 0)) eq_refl eq_refl eq_refl eq_refl)) eq_refl eq_refl eq_refl eq_refl)).
  pose proof (INC_stds (2*g+(1+u+(1+i+m)) - 2^(S h)) (2^h*4)) as H2.
  pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 eq_refl ltac:(lia)) as H3.
  eapply evstep_trans.
  1: { eapply bounces0. eapply PAs_eq. 1: apply H3. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
  apply evstep_refl'. f_equal; rewrite ?Nat.pow_succ_r' in *; lia.
Qed.

Lemma P4_pre h u r g i m:
  1 <= r < 2^(h+u) -> g < 2^h ->
  2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) ->
  K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+
  K (2^h) (2^h+g) (1+u+(1+i+m)) 0.
Proof.
  intros Hr Hg Hb.
  pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu.
  assert (E1: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r.
  destruct (lowbit r) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep (h+u) P o1 0 2 0 2 1) as H1.
  specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF0 1 0)).
  pose proof (Gaps (h+u) (2^u*(2*g+1)) 0 1 0) as H2.
  specialize (H2 ltac:(rewrite Nat.pow_succ_r', E1; nia)).
  pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(rewrite ?Nat.pow_succ_r'; lia) ltac:(lia)) as H3.
  assert (Hj: (2 ^ S (h+u) - 2 ^ S P * (2 * o1 + 1) - 0) + 2^u*(2*g+1) = S (1+i+m)).
  { rewrite ?Nat.pow_succ_r' in *. lia. }
  rewrite Hj in H3.
  destruct (PAs_last _ _ _ _ _ H3) as [e1 [o2 [H4 H5]]].
  eapply progress_trans. 1: apply OV_even with (a:=r) (c:=2^(S (h+u))) (u:=i), pk_ov; rewrite ?Nat.pow_succ_r'; lia.
  eapply evstep_progress_trans.
  1: { eapply bounces0. eapply PAs_eq. 1: apply H4. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
  eapply progress_evstep_trans. 1: apply OV_even with (a:=2^h+g) (c:=2^h) (u:=u).
  - eapply PA_eq. 1: apply H5. all: rewrite ?Nat.pow_succ_r' in *; nia.
  - finish.
Qed.

Lemma BS_P4a h u r i m:
  1 <= r < 2^(h+u) ->
  2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u ->
  K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+
  K (pkE (3*2^h+(1+u+(1+i+m)))) (pkO (3*2^h+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)).
Proof.
  intros Hr Hb.
  pose proof (pow_pos h) as Ph.
  eapply progress_evstep_trans. 1: apply (P4_pre h u r 0 i m); [lia|apply pow_pos|lia].
  destruct (pk_eq h (3*2^h)) as [E1 E2]. { rewrite !Nat.pow_succ_r'. lia. }
  pose proof (INC_pks (1+u+(1+i+m)) (3*2^h)) as H1.
  specialize (H1 ltac:(lia)). rewrite E1, E2 in H1.
  eapply evstep_trans.
  1: { eapply bounces0. eapply PAs_eq. 1: apply H1. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
  finish.
Qed.

Lemma BS_P4b h u r g i m:
  1 <= r < 2^(h+u) -> 1 <= g < 2^h ->
  2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) ->
  2^(S h) <= 2*g + (1+u+(1+i+m)) ->
  K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+
  K (pkE (2^(S h)+2*g+(1+u+(1+i+m)))) (pkO (2^(S h)+2*g+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)).
Proof.
  intros Hr Hg Hb Hn.
  pose proof (pow_pos h) as Ph.
  eapply progress_evstep_trans. 1: apply (P4_pre h u r g i m); lia.
  destruct (lowbit g) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep h P o1 0 1 1 0 2) as H1.
  specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
  specialize (H1 (PF_eq _ _ _ _ _ _ _ _ (PF3 0 0 0 1 (PF0 0 0)) eq_refl eq_refl eq_refl eq_refl)).
  destruct (pk_eq (S h) (2^(S (S h)))) as [E1 E2].
  { rewrite !Nat.pow_succ_r'. lia. }
  pose proof (INC_pks (2*g+(1+u+(1+i+m)) - 2^(S h)) (2^(S (S h)))) as H2.
  specialize (H2 ltac:(rewrite !Nat.pow_succ_r'; lia)).
  rewrite E1, E2 in H2.
  pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(rewrite !Nat.pow_succ_r'; lia) ltac:(rewrite !Nat.pow_succ_r'; lia)) as H3.
  eapply evstep_trans.
  1: { eapply bounces0. eapply PAs_eq. 1: apply H3. 4,5: try reflexivity.
       all: try (f_equal; rewrite ?Nat.pow_succ_r' in *; lia).
       all: rewrite ?Nat.pow_succ_r' in *; lia. }
  apply evstep_refl'. rewrite Nat.add_0_r. f_equal; f_equal; rewrite ?Nat.pow_succ_r' in *; lia.
Qed.

(** ** Invariant (proof.md 4.1) and the main induction *)

Definition St (s : bool * nat * nat) : Q * tape :=
  let '(t, N, m) := s in if t then K (pkE N) (pkO N) 0 m else K N 0 0 m.

Definition I (s : bool * nat * nat) : Prop :=
  let '(t, N, m) := s in
  1 <= m <= N /\ (t = true -> 2 <= N) /\
  (if Nat.even (N + m) then
     (if t then (if Nat.even N then N <= 2*m+3 else 2*N <= 5*m+6)
           else (if Nat.even N then 2*N <= 3*m+6 else N <= 2*m+3))
   else N <= m+3).

Ltac solve_initF :=
  change (F, tape0) with (cconfig_to_config (nil,nil,0,F));
  repeat rewrite Str_cons_def;
  repeat rewrite <-Str_app_assoc;
  repeat rewrite simpl_directed_head_l;
  repeat rewrite simpl_directed_head_r;
  repeat rewrite l_const0_app_nil;
  repeat rewrite r_const0_app_nil;
  repeat rewrite config_to_cconfig;
  apply cconfig_evstep_dec_spec with (n:=1000000);
  vm_compute;
  reflexivity.

Lemma initF: F;; tape0 -->* K 2 0 0 2.
Proof.
  unfold K. replace (WS 2 0) with ([0;0;1] *> const 0).
  2: { unfold WS. cbn. rewrite <-const_unfold. reflexivity. }
  unfold R. cbn [lpow Str_app app]. solve_initF.
Qed.

(** ** Coverage and closure (proof.md 4.2 Lemma S, 4.3 Lemma C) *)

Local Open Scope nat_scope.

Lemma St_std N m: St (false, N, m) = K N 0 0 m.
Proof. reflexivity. Qed.

Lemma St_pk N m: St (true, N, m) = K (pkE N) (pkO N) 0 m.
Proof. reflexivity. Qed.

Lemma even_mod x: Nat.even x = true -> x mod 2 = 0.
Proof. intros H. apply Nat.even_spec in H as [q ->]. lia. Qed.

Lemma odd_mod x: Nat.even x = false -> x mod 2 = 1.
Proof.
  intros H. destruct (Nat.Even_or_Odd x) as [He|[q ->]].
  - apply Nat.even_spec in He. congruence.
  - lia.
Qed.

Ltac par x := let E := fresh "E" in
  destruct (Nat.even x) eqn:E; [apply even_mod in E | apply odd_mod in E].

(** I in linear-arithmetic form (parities as [mod 2]) *)
Lemma I_std N m: I (false, N, m) <->
  1 <= m <= N /\
  ((N+m) mod 2 = 0 -> N mod 2 = 0 -> 2*N <= 3*m+6) /\
  ((N+m) mod 2 = 0 -> N mod 2 = 1 -> N <= 2*m+3) /\
  ((N+m) mod 2 = 1 -> N <= m+3).
Proof.
  unfold I. cbv beta iota zeta. par (N+m); par N; cbv beta iota.
  all: split; [intros [H1 [_ H3]]; lia | intros H; split; [lia | split; [intros Hf; discriminate | lia]]].
Qed.

Lemma I_pk N m: I (true, N, m) <->
  1 <= m <= N /\ 2 <= N /\
  ((N+m) mod 2 = 0 -> N mod 2 = 0 -> N <= 2*m+3) /\
  ((N+m) mod 2 = 0 -> N mod 2 = 1 -> 2*N <= 5*m+6) /\
  ((N+m) mod 2 = 1 -> N <= m+3).
Proof.
  unfold I. cbv beta iota zeta. par (N+m); par N; cbv beta iota.
  all: split; [intros [H1 [H2 H3]]; specialize (H2 eq_refl); lia | intros H; split; [lia | split; [intros _; lia | lia]]].
Qed.

(** results N' = D + n, m' = n *)
Lemma close_diag t n: 1 <= n -> (t = true -> 2 <= n) -> I (t, n, n).
Proof.
  intros H1 H2. destruct t; [apply I_pk; specialize (H2 eq_refl) | apply I_std]; lia.
Qed.

Lemma close_std D n: 1 <= n ->
  (D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 1 -> D <= n+3) /\ (n mod 2 = 0 -> 2*D <= n+6)) ->
  I (false, D+n, n).
Proof. intros. apply I_std. lia. Qed.

Lemma close_pk D n: 1 <= n -> 2 <= D+n ->
  (D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 0 -> D <= n+3) /\ (n mod 2 = 1 -> 2*D <= 3*n+6)) ->
  I (true, D+n, n).
Proof. intros. apply I_pk. lia. Qed.

(** N+1 = 2^i (2k+1): the three shapes of N *)
Lemma Nfacts N k i: S N = 2^i*(2*k+1) ->
  (i = 0 /\ N = 2*k) \/ (i = 1 /\ N = 4*k+1) \/ (2 <= i /\ (S N) mod 4 = 0 /\ 8*k+4 <= S N).
Proof.
  intros H. destruct i as [|[|i']].
  - left. rewrite Nat.pow_0_r in H. lia.
  - right; left. rewrite Nat.pow_1_r in H. lia.
  - right; right. rewrite !Nat.pow_succ_r' in H. pose proof (pow_pos i').
    assert (H1: S N = 4 * (2^i'*(2*k+1))) by lia.
    assert (H2: 2*k+1 <= 2^i'*(2*k+1)) by nia.
    remember (2^i'*(2*k+1)) as Y. clear HeqY H. lia.
Qed.

Ltac nfacts N k i Hk :=
  destruct (Nfacts N k i Hk) as [[-> ->]|[[-> ->]|[?Hi [?H4 ?H8]]]]; clear Hk.

Lemma log2_facts k: 1 <= k -> exists l r, k = 2^l + r /\ r < 2^l.
Proof.
  intros Hk. exists (Nat.log2 k), (k - 2^(Nat.log2 k)).
  pose proof (Nat.log2_spec k ltac:(lia)) as [H1 H2].
  rewrite Nat.pow_succ_r' in H2. lia.
Qed.

Lemma pow_ge2 u: 1 <= u -> 2 <= 2^u.
Proof. intros Hu. destruct u as [|u]; [lia|]. rewrite Nat.pow_succ_r'. pose proof (pow_pos u). lia. Qed.

Lemma pow_ge4 u: 2 <= u -> 4 <= 2^u.
Proof.
  intros Hu. replace u with (S (S (u-2))) by lia. rewrite !Nat.pow_succ_r'.
  pose proof (pow_pos (u-2)). lia.
Qed.

Lemma pow_par h: (h = 0 /\ 2^h = 1) \/ 2^h mod 2 = 0.
Proof. destruct h as [|h]; [left; split; reflexivity | right; rewrite Nat.pow_succ_r'; lia]. Qed.

(** the gen-2 exponents of S3/P4: v = 2^u (2g+1) with 1 <= v < 2^l and v even *)
Lemma split_v l v: 1 <= v -> v < 2^l -> v mod 2 = 0 ->
  exists h u g, l = S (h+u) /\ v = 2^u*(2*g+1) /\ 1 <= u /\ g < 2^h.
Proof.
  intros Hv1 Hv2 Hv3.
  destruct (lowbit v) as [u [g Hv]]; [lia|].
  pose proof (pow_odd_pos u g) as Pug.
  assert (Hul: u < l). { apply (Nat.pow_lt_mono_r_iff 2); lia. }
  exists (l - S u), u, g.
  assert (El: l = S (l - S u + u)) by lia.
  split; [exact El|]. split; [exact Hv|].
  pose proof (pow_pos u) as Pu.
  split.
  - destruct u as [|u']; [|lia]. rewrite Nat.pow_0_r in Hv. lia.
  - set (h := l - S u) in *. clearbody h. subst l.
    rewrite Nat.pow_succ_r', Nat.pow_add_r in Hv2.
    assert (H1: 2^u*(2*g+1) < 2^u*(2*2^h)) by lia.
    apply Nat.mul_lt_mono_pos_l in H1; lia.
Qed.

(** closure of S1, P1, P2 (proof.md 4.3) *)
Lemma C_S1 N m i k: I (false, N, m) -> S N = 2^i*(2*k+1) -> 1 <= k ->
  I (true, 2*k+(1+i+m), 1+i+m).
Proof.
  intros HI Hk Hk1. apply I_std in HI. apply I_pk.
  nfacts N k i Hk; lia.
Qed.

Lemma C_P1 N m i l: I (true, N, m) -> S N = 2^i*(2*(2^l+0)+1) ->
  I (false, 2^l+(1+i+m), 1+i+m).
Proof.
  intros HI Hk. apply I_pk in HI. apply I_std.
  pose proof (pow_pos l). pose proof (pow_par l) as Hl.
  rewrite Nat.add_0_r in Hk. set (Z := 2^l) in *. clearbody Z.
  nfacts N Z i Hk; lia.
Qed.

Lemma C_P2 N m i l r: I (true, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> r < 2^l ->
  I (false, 2*r+(1+i+m), 1+i+m).
Proof.
  intros HI Hk Hr. apply I_pk in HI. apply I_std.
  set (Z := 2^l) in *. clearbody Z.
  nfacts N (Z+r) i Hk; lia.
Qed.

(** coverage of S3 and P4 (proof.md 4.2): the dirty cases are i = 0 (S3), i <= 1 (P4), class P,
    in the final gap, with T even *)
Lemma Cov_S3 N m i l r: I (false, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> 1 <= r -> r < 2^l ->
  2*(2^l+r)+(1+i+m)+1 < 4*2^l ->
  i = 0 /\ m mod 2 = 0 /\ 2*r < 2^l /\ 3*2^l < 2*(2^l+r)+(1+i+m)+1 /\ 4*(2^l+r) <= 3*m+6.
Proof.
  intros HI Hk Hr1 Hr Hlt. apply I_std in HI.
  set (Z := 2^l) in *. clearbody Z.
  nfacts N (Z+r) i Hk; lia.
Qed.

Lemma Cov_P4 N m i l r: I (true, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> 1 <= r -> r < 2^l ->
  2*r+(1+i+m)+1 < 2*2^l ->
  i <= 1 /\ (2*r+(1+i+m)+1) mod 2 = 0 /\ 2*r < 2^l /\ 2^l < 2*r+(1+i+m)+1 /\ 2^l < 1+i+m.
Proof.
  intros HI Hk Hr1 Hr Hlt. apply I_pk in HI.
  set (Z := 2^l) in *. clearbody Z.
  nfacts N (Z+r) i Hk; lia.
Qed.

Lemma step_std N m: I (false, N, m) -> exists s', St (false, N, m) -->+ St s' /\ I s'.
Proof.
  intros HI. rewrite St_std.
  assert (Hm: 1 <= m <= N) by (apply I_std in HI; tauto).
  destruct (lowbit (S N)) as [i [k Hk]]; [lia|].
  destruct (Nat.eq_dec k 0) as [->|Hk0].
  { (* S0 *)
    exists (false, 1+i+m, 1+i+m). rewrite St_std. split.
    - replace N with (2^i-1) by lia. apply BS_S0.
    - apply close_diag; [lia | intros Hf; discriminate Hf]. }
  destruct (log2_facts k ltac:(lia)) as [l [r [-> Hr]]].
  replace N with ((2*(2^l+r)+1)*2^i-1) by lia.
  pose proof (pow_pos l) as Pl.
  assert (E2: 2^(S l) = 2*2^l) by apply Nat.pow_succ_r'.
  assert (E4: 2^(S (S l)) = 4*2^l) by (rewrite !Nat.pow_succ_r'; lia).
  destruct (Nat.eq_dec r 0) as [->|Hr0].
  { (* S1, k = 2^l *)
    exists (true, 2*(2^l+0)+(1+i+m), 1+i+m). rewrite St_pk. split.
    - apply BS_S1a with (l := l). lia.
    - apply (C_S1 N); [exact HI | exact Hk | lia]. }
  destruct (lt_eq_lt_dec (2*(2^l+r)+(1+i+m)+1) (2^(S (S l)))) as [[Hlt|Heq]|Hgt].
  3: { (* S1, T > 2^(l+2) *)
    exists (true, 2*(2^l+r)+(1+i+m), 1+i+m). rewrite St_pk. split.
    - clear Hk. apply BS_S1b with (l := l); lia.
    - apply (C_S1 N); [exact HI | exact Hk | lia]. }
  2: { (* S2 *)
    exists (false, l+4+(1+i+m), l+4+(1+i+m)). rewrite St_std. split.
    - clear Hk. apply BS_S2; lia.
    - apply close_diag; [lia | intros Hf; discriminate Hf]. }
  (* S3 *)
  rewrite E4 in Hlt.
  destruct (Cov_S3 N m i l r HI Hk ltac:(lia) Hr Hlt) as [-> [Hm2 [Hr2 [HT3 H43]]]].
  clear HI Hk Hm.
  assert (HZ: 2^l mod 2 = 0).
  { destruct l as [|l']; [rewrite Nat.pow_0_r in *; lia | rewrite Nat.pow_succ_r'; lia]. }
  destruct (split_v l (2*(2^l+r)+(1+0+m)+1 - 3*2^l)) as [h [u [g [-> [Hv [Hu1 Hg]]]]]];
    [lia|lia|lia|].
  assert (E1: 2^(S (h+u)) = 2*(2^h*2^u)) by (rewrite Nat.pow_succ_r', Nat.pow_add_r; reflexivity).
  assert (E3: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r.
  assert (E5: 2^(S h) = 2*2^h) by apply Nat.pow_succ_r'.
  pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu.
  assert (HU: 2*2^h <= 2^h*2^u) by (pose proof (pow_ge2 u Hu1); nia).
  assert (HU2: 2 <= u -> 4*2^h <= 2^h*2^u) by (intros Hu2; pose proof (pow_ge4 u Hu2); nia).
  pose proof (pow_par h) as Hh.
  (* n = 1+u+(1+0+m) > 2^l >= 4*2^h, n odd if u = 1 *)
  assert (Hn: 2^(S (h+u)) < 1+u+(1+0+m)) by lia.
  assert (Hv': 2*r+(1+0+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1)) by lia.
  clear Hv HZ E4 E2 Pl HT3 H43 Hlt.
  destruct (Nat.eq_dec g 0) as [->|Hg0].
  - exists (false, 3*2^h+(1+u+(1+0+m)), 1+u+(1+0+m)). rewrite St_std. split.
    + apply BS_S3a; lia.
    + apply close_std; [lia|].
      destruct Hh as [[-> Hh1]|Hh]; [left; lia | right; lia].
  - exists (false, 2^(S h)+2*g+(1+u+(1+0+m)), 1+u+(1+0+m)). rewrite St_std. split.
    + apply BS_S3b; lia.
    + apply close_std; [lia|]. right. lia.
Qed.

Lemma step_pk N m: I (true, N, m) -> exists s', St (true, N, m) -->+ St s' /\ I s'.
Proof.
  intros HI. rewrite St_pk.
  assert (Hm: 1 <= m <= N /\ 2 <= N) by (apply I_pk in HI; tauto).
  destruct (lowbit (S N)) as [i [k Hk]]; [lia|].
  destruct (Nat.eq_dec k 0) as [->|Hk0].
  { (* P0 *)
    assert (Hi: 2 <= i).
    { destruct (Nfacts N 0 i Hk) as [[_ HN]|[[_ HN]|[Hi _]]]; lia. }
    exists (false, 2+i+m, 2+i+m). rewrite St_std. split.
    - replace N with (2^i-1) by lia. apply BS_P0, Hi.
    - apply close_diag; [lia | intros Hf; discriminate Hf]. }
  destruct (log2_facts k ltac:(lia)) as [l [r [-> Hr]]].
  replace N with ((2*(2^l+r)+1)*2^i-1) by lia.
  pose proof (pow_pos l) as Pl.
  assert (E2: 2^(S l) = 2*2^l) by apply Nat.pow_succ_r'.
  destruct (Nat.eq_dec r 0) as [->|Hr0].
  { (* P1 *)
    exists (false, 2^l+(1+i+m), 1+i+m). rewrite St_std. split.
    - apply BS_P1.
    - apply (C_P1 N); [exact HI | exact Hk]. }
  destruct (lt_eq_lt_dec (2*r+(1+i+m)+1) (2^(S l))) as [[Hlt|Heq]|Hgt].
  3: { (* P2 *)
    exists (false, 2*r+(1+i+m), 1+i+m). rewrite St_std. split.
    - clear Hk. apply BS_P2; lia.
    - apply (C_P2 N m i l); [exact HI | exact Hk | exact Hr]. }
  2: { (* P3 *)
    exists (false, l+2+(1+i+m), l+2+(1+i+m)). rewrite St_std. split.
    - clear Hk. apply BS_P3; lia.
    - apply close_diag; [lia | intros Hf; discriminate Hf]. }
  (* P4 *)
  rewrite E2 in Hlt.
  destruct (Cov_P4 N m i l r HI Hk ltac:(lia) Hr Hlt) as [Hi1 [HT2 [Hr2 [HT1 Hb]]]].
  clear HI Hk Hm.
  assert (HZ: 2^l mod 2 = 0).
  { destruct l as [|l']; [rewrite Nat.pow_0_r in *; lia | rewrite Nat.pow_succ_r'; lia]. }
  destruct (split_v l (2*r+(1+i+m)+1 - 2^l)) as [h [u [g [-> [Hv [Hu1 Hg]]]]]];
    [lia|lia|lia|].
  assert (E1: 2^(S (h+u)) = 2*(2^h*2^u)) by (rewrite Nat.pow_succ_r', Nat.pow_add_r; reflexivity).
  assert (E3: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r.
  assert (E5: 2^(S h) = 2*2^h) by apply Nat.pow_succ_r'.
  pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu.
  assert (HU: 2*2^h <= 2^h*2^u) by (pose proof (pow_ge2 u Hu1); nia).
  pose proof (pow_par h) as Hh.
  assert (Hv': 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1)) by lia.
  clear Hv HZ E2 Pl HT1 HT2 Hlt.
  destruct (Nat.eq_dec g 0) as [->|Hg0].
  - exists (true, 3*2^h+(1+u+(1+i+m)), 1+u+(1+i+m)). rewrite St_pk. split.
    + apply BS_P4a; lia.
    + apply close_pk; [lia|lia|].
      destruct Hh as [[-> Hh1]|Hh]; [left; lia | right; lia].
  - exists (true, 2^(S h)+2*g+(1+u+(1+i+m)), 1+u+(1+i+m)). rewrite St_pk. split.
    + apply BS_P4b; lia.
    + apply close_pk; [lia|lia|]. right. lia.
Qed.

Lemma step_I s: I s -> exists s', St s -->+ St s' /\ I s'.
Proof.
  destruct s as [[[|] N] m].
  - apply step_pk.
  - apply step_std.
Qed.

Lemma nonhalt_F: ~halts tmP (F;; tape0).
Proof.
  eapply multistep_nonhalt. 1: apply initF.
  change (K 2 0 0 2) with (St (false, 2%nat, 2%nat)).
  apply progress_nonhalt_cond with (P := I).
  - apply step_I.
  - cbn. lia.
Qed.

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

Definition f349 (q : Q) : Q :=
  match q with A => F | B => A | C => B | D => C | E => D | F => E end.

Lemma perm_349 : Perm (flip tm) tmP f349.
Proof.
  split.
  - intros [] [] H; cbn in *; try discriminate; reflexivity.
  - intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
Qed.

Lemma nonhalt: ~halts tm c0.
Proof.
  intros H. apply flip_halts in H.
  change (halts (flip tm) (A;; tape0)) in H.
  exact (nonhalt_F (perm_halts _ _ _ _ _ perm_349 H)).
Qed.

Print Assumptions nonhalt.