(** * 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: (work in progress, not yet closed)
*)

From BusyCoq Require Import Individual62.
Require Import ZifyNat Lia.
Require Import ZArith.
Require Import String.

Open Scope list.

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

Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
Notation "c -->+ c'" := (c -[ tm ]->+ 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}} r -->+ l <{{A}} [1;1] *> r.
Proof. es. Qed.
Lemma TF3 l r: [1;1] *> l <{{F}} r -->+ l <{{F}} [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}} r -->+ WS e' o' {{B}}> 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|]; 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|]; apply TB).
  all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TF2|]; eapply progress_trans; [apply H|]; apply TB).
  all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TF3|]; eapply progress_trans; [apply H|]; apply TB).
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).

Lemma init0: c0 -->* K 1 0 0 1.
Proof.
  unfold K. replace (WS 1 0) with ([1] *> const 0).
  2: { unfold WS. cbn. rewrite <-const_unfold. reflexivity. }
  unfold R. esx.
Qed.

(* TODO (round 2+): Lemma S (coverage) and Lemma C (closure) of proof.md 4.2/4.3, one
   sub-lemma per macro rule (work in progress). *)
Lemma step_I s: I s -> exists s', St s -->+ St s' /\ I s'.
Proof.
Admitted.

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

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

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

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

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

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

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