(** * 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC never halts

    Machine: 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC ("Bell eats counter").
    Adapted from verify/BECv5.v, Module TM1 (architecture only): a binary counter
    BinInc [1;1] on the right (here incremented with RBinInc_spec), a 1010 budget
    word with a one-cell defect on the left, one budget pair per count, an eat of the
    low counter digits, BigStep lemmas and progress_nonhalt_cond with a linear
    invariant (here 1 <= N <= 2p).  Differences: the defect walks away from the
    counter, the eat happens at the far blank edge after a C/F sweep over the whole
    word, it removes 1-3 digits depending on N mod 8, and N = 6 (mod 8) goes through a
    misaligned fixed-width counter Q_k(x,y) and a two-defect transient.
    The informal proof is the accompanying write-up (proof.md); the rules below are
    its 3.1-3.5 (count rules INC1/INC0/INC011/OVF, eat rules EAT/Y1-Y4, walks
    W/W2/W0/B, macro rules M1-M5) and the invariant J of its 4.

    Configurations are taken 6 steps after the write-up's G form (after rule TS):
      HF l r  =  l <E 1 0 1 1 r,   EC p N  =  HF (0^inf (10)^p) (C N)  ( = E(p,N) ).

    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.
From BusyCoq Require Import BinaryCounter_v2.

Open Scope list.

Definition tm := Eval compute in (TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC").

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

(** C(n): n in binary, lowest digit first, 1 = 11, 0 = 00, leading 1 last.
    HF l r: E reads the last cell of l, followed by 1 0 1 1 and the right side r. *)
Definition C n := BinInc [1;1] n.
Definition HF (l r : side) := l <{{E}} [1;0;1;1] *> r.

(** ** Low-level rules *)

(* right part of every count: A over (11)^n, CARRY, TS *)

Lemma RIncG l r n:
  l <* [1;1;0;1] {{A}}> [1;1]^^n *> [0;0] *> r -->+
  l <{{E}} [1;0;1;1] *> [0;0]^^n *> [1;1] *> r.
Proof. es. Qed.

(* the counter increment on C *)
Lemma RInc n l:
  l <* [1;1;0;1] {{A}}> C n -->+ HF l (C (1+n)).
Proof.
  unfold C, HF. apply RBinInc_spec. intros. apply RIncG.
Qed.

(* left parts: INC1 (EB, X1, AS), INC0 (EB, X0, AS), INC011 (F011, A01, AS) *)
Lemma L1 u b r:
  HF (u <* [1] <* [0;1]^^b) r -->+ u <* [0] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma L0 u b r:
  HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ u <* [0;1;0;1] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma L011 u r:
  HF (u <* [0;0;1;1;0;1]) r -->+ u <* [0;1;1;0;1;0] <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

(* EAT: EB, then the C/F sweep EAT0 over the whole word, then CS *)
Lemma LEat b r:
  HF (0inf <* [0;1]^^b) r -->+ 0inf <* [0;1]^^(b+2) <* [0;1;1] {{A}}> r.
Proof. unfold HF. es. Qed.

(* Y rules: the right part after an eat *)
Lemma Y1C v n:
  v <* [0;1;1] {{A}}> C (n*2+1) -->+ HF (v <* [1]) (C (1+n)).
Proof.
  unfold C. rewrite BinInc_mul2add1. fold (C n).
  eapply progress_trans. 2: apply RInc.
  unfold C. es.
Qed.

Lemma Y2C v n:
  v <* [0;1;1] {{A}}> C (n*4) -->+ HF (v <* [1;1;1]) (C n).
Proof.
  unfold C. replace (n*4) with (n*2*2) by lia. rewrite !BinInc_mul2.
  unfold HF. es.
Qed.

Lemma Y3 v s r:
  v <* [0;1;1] {{A}}> [0;0] *> [1;1] *> [1;1]^^s *> [0;0] *> r -->+
  HF (v <* [1;1]) ([0;0]^^s *> [0] *> [1;1] *> r).
Proof. unfold HF. es. Qed.

Lemma Y4 v m:
  v <* [0;1;1] {{A}}> [1;1;0] *> [1;1] *> C m -->+ HF (v <* [1;0;1;1]) (C (1+m)).
Proof.
  eapply progress_trans. 2: apply RInc.
  es.
Qed.

Lemma Y1Q v r:
  v <* [0;1;1] {{A}}> [1;1] *> [0;0] *> r -->+ HF (v <* [1]) ([1;1] *> r).
Proof. unfold HF. es. Qed.

(* right part of OVF: the overflow of Q_j(2^j-1, 2m+1) *)
Lemma ROvf l j m:
  l <* [1;1;0;1] {{A}}> [1;1]^^j *> [0;1;1] *> C m -->+
  HF (l <* [0;1] <* [1;1]^^j <* [1]) (C (1+m)).
Proof.
  eapply progress_trans. 2: apply RInc.
  es.
Qed.

(** ** Generic counting *)

Definition Inc r r' := forall l, l <* [1;1;0;1] {{A}}> r -->+ HF l r'.

Lemma IncC n: Inc (C n) (C (1+n)).
Proof. intros l. apply RInc. Qed.

Lemma Inc00 r: Inc ([0;0] *> r) ([1;1] *> r).
Proof. intros l. apply (RIncG l r 0). Qed.

Lemma pt3 c1 c2 c2' c3: c1 -->+ c2 -> c2 = c2' -> c2' -->+ c3 -> c1 -->+ c3.
Proof. intros H1 -> H2. eapply progress_trans; eauto. Qed.

Lemma pt_pre c1 c1' c2: c1 = c1' -> c1' -->+ c2 -> c1 -->+ c2.
Proof. intros -> H1. exact H1. Qed.

Lemma pt_eq c1 c2 c3: c1 -->+ c2 -> c2 = c3 -> c1 -->+ c3.
Proof. intros H1 ->. exact H1. Qed.

Lemma HF_eq l l' r r': l = l' -> r = r' -> HF l r = HF l' r'.
Proof. intros -> ->. reflexivity. Qed.

Lemma Cnt1 u b r r': Inc r r' ->
  HF (u <* [1] <* [0;1]^^b) r -->+ HF (u <* [0] <* [0;1]^^b) r'.
Proof. intros I. eapply progress_trans. 1: apply L1. apply I. Qed.

Lemma Cnt0 u b r r': Inc r r' ->
  HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ HF (u <* [0;1;0;1] <* [0;1]^^b) r'.
Proof. intros I. eapply progress_trans. 1: apply L0. apply I. Qed.

Lemma Cnt011 u r r': Inc r r' ->
  HF (u <* [0;0;1;1;0;1]) r -->+ HF (u <* [0;1;1;0;1;0]) r'.
Proof. intros I. eapply progress_trans. 1: apply L011. apply I. Qed.

(** ** The misaligned counter Q_k(x,y) = D_k(x) 0 C(y) *)

Fixpoint Dk (k x : nat) : list Sym :=
  match k with
  | O => []
  | S k' => (if Nat.odd x then [1;1] else [0;0]) ++ Dk k' (Nat.div2 x)
  end.

Definition Q k x y := Dk k x *> [0] *> C y.

Lemma Dk_even k a: Dk (S k) (2*a) = [0;0] ++ Dk k a.
Proof.
  cbn [Dk]. rewrite Nat.div2_double.
  replace (Nat.odd (2*a)) with false. 1: reflexivity.
  rewrite <-Nat.negb_even, Nat.even_mul. reflexivity.
Qed.

Lemma Dk_odd k a: Dk (S k) (2*a+1) = [1;1] ++ Dk k a.
Proof.
  replace (2*a+1) with (S (2*a)) by lia.
  cbn [Dk]. rewrite Nat.div2_succ_double.
  replace (Nat.odd (S (2*a))) with true. 1: reflexivity.
  rewrite Nat.odd_succ, Nat.even_mul. reflexivity.
Qed.

Lemma Dk_0 k: Dk k 0 = [0;0]^^k.
Proof. induction k as [|k IH]. 1: reflexivity. cbn. rewrite IH. reflexivity. Qed.

Lemma Dk_1 k: Dk (S k) 1 = [1;1] ++ [0;0]^^k.
Proof. cbn [Dk]. cbn. rewrite Dk_0. reflexivity. Qed.

Lemma Dk_full k: Dk k (2^k-1) = [1;1]^^k.
Proof.
  induction k as [|k IH]. 1: reflexivity.
  replace (2^(S k)-1) with (2*(2^k-1)+1).
  2: { rewrite Nat.pow_succ_r'. pose proof (Nat.pow_nonzero 2 k). lia. }
  rewrite Dk_odd, IH. reflexivity.
Qed.

Lemma Dk_inc k: forall x, S x < 2^k -> exists t rest,
  Dk k x = [1;1]^^t ++ [0;0] ++ rest /\ Dk k (S x) = [0;0]^^t ++ [1;1] ++ rest.
Proof.
  induction k as [|k IH]; intros x Hx.
  1: cbn in Hx; lia.
  rewrite Nat.pow_succ_r' in Hx.
  destruct (Nat.Even_or_Odd x) as [[a ->]|[a ->]].
  - exists O, (Dk k a). rewrite Dk_even.
    replace (S (2*a)) with (2*a+1) by lia. rewrite Dk_odd. split; reflexivity.
  - destruct (IH a) as [t [rest [E1 E2]]]. 1: lia.
    exists (S t), rest. rewrite Dk_odd.
    replace (S (2*a+1)) with (2*(S a)) by lia. rewrite Dk_even.
    rewrite E1, E2. split; reflexivity.
Qed.

Lemma IncQ k x y: S x < 2^k -> Inc (Q k x y) (Q k (S x) y).
Proof.
  intros Hx l. unfold Q.
  destruct (Dk_inc k x Hx) as [t [rest [E1 E2]]].
  rewrite E1, E2, !Str_app_assoc. apply RIncG.
Qed.

(** ** Walks *)

Lemma lp2 (b:nat) (X:side): [0;1]^^b *> [0;1;0;1] *> X = [0;1]^^(S (S b)) *> X.
Proof.
  change ([0;1;0;1] *> X) with ([0;1] *> [0;1] *> X).
  rewrite !lpow_shift'. reflexivity.
Qed.

Lemma lp1 (b:nat) (X:side): [0;1]^^b *> [0;1] *> X = [0;1]^^(S b) *> X.
Proof. rewrite lpow_shift'. reflexivity. Qed.

(* W2: G(u (10)^2 1 (10)^b, r1) -> G(u 1 (10)^(b+2), r3), counts INC1, INC0 *)
Lemma W2 u b r1 r2 r3: Inc r1 r2 -> Inc r2 r3 ->
  HF (u <* [0;1;0;1] <* [1] <* [0;1]^^b) r1 -->+ HF (u <* [1] <* [0;1]^^(S (S b))) r3.
Proof.
  intros I1 I2.
  eapply progress_trans. 1: apply (Cnt1 (u <* [0;1;0;1]) b r1 r2 I1).
  eapply pt_eq. 1: apply (Cnt0 (u <* [1]) b r2 r3 I2).
  apply HF_eq. 2: reflexivity.
  apply lp2.
Qed.

(* W(a,b): G((10)^a 1 (10)^b, C n) -> E(a+b+[a odd], n+a+1), a+1 counts *)
Lemma Wk a: forall b n,
  HF (0inf <* [0;1]^^a <* [1] <* [0;1]^^b) (C n) -->+
  HF (0inf <* [0;1]^^(a+b+a mod 2)) (C (n+a+1)).
Proof.
  induction a as [a IH] using lt_wf_ind. intros b n.
  destruct a as [|[|a]].
  - eapply pt_eq. 1: apply (Cnt1 0inf b (C n) _ (IncC n)).
    apply HF_eq. 2: f_equal; lia.
    cbn [Nat.add Nat.modulo]. rewrite Nat.add_0_r.
    cbn [Str_app]. rewrite <-const_unfold. reflexivity.
  - eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]) b (C n) _ (IncC n)).
    eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
      instantiate (1:= 0inf <* [0;0;1;0] <* [0;1]^^b).
      cbn [Str_app]. rewrite <-const_unfold. reflexivity. }
    eapply pt_eq. 1: apply (Cnt0 0inf b (C (1+n)) _ (IncC (1+n))).
    apply HF_eq. 2: f_equal; lia.
    rewrite lp2. f_equal. f_equal.
    pose proof (Nat.mod_upper_bound (S (S b)) 2).
    cbn. lia.
  - eapply progress_trans.
    1: apply (W2 (0inf <* [0;1]^^a) b (C n) (C (1+n)) (C (1+(1+n))) (IncC n) (IncC (1+n))).
    eapply pt_eq. 1: apply (IH a ltac:(lia) (S (S b)) (1+(1+n))).
    apply HF_eq. 2: f_equal; lia.
    f_equal. f_equal. lia.
Qed.

(* W2 iterated on Q: phase (d) of M5 *)
Lemma W2Q t y i: forall u b x, x + 2*i < 2^t ->
  HF (u <* [0;1;0;1]^^i <* [1] <* [0;1]^^b) (Q t x y) -->*
  HF (u <* [1] <* [0;1]^^(b+2*i)) (Q t (x+2*i) y).
Proof.
  induction i as [|i IH]; intros u b x Hx.
  - apply evstep_refl'. apply HF_eq. 2: f_equal; lia.
    rewrite Nat.add_0_r. reflexivity.
  - apply progress_evstep.
    eapply progress_evstep_trans.
    1: apply (W2 (u <* [0;1;0;1]^^i) b _ _ _ (IncQ t x y ltac:(lia)) (IncQ t (S x) y ltac:(lia))).
    eapply evstep_trans. 1: apply (IH u (S (S b)) (S (S x)) ltac:(lia)).
    apply evstep_refl'. apply HF_eq; lia_refl.
Qed.

(* B(s): G(u 1^(2s+1) (10)^j, C n) -> G(u 0 (10)^(s+j), C(n+s+1)), s+1 counts INC1 *)
Lemma Bk s: forall j u n,
  HF (u <* [1;1]^^s <* [1] <* [0;1]^^j) (C n) -->+
  HF (u <* [0] <* [0;1]^^(s+j)) (C (n+s+1)).
Proof.
  induction s as [|s IH]; intros j u n.
  - eapply pt_eq. 1: apply (Cnt1 u j (C n) _ (IncC n)).
    apply HF_eq. 1: reflexivity. f_equal; lia.
  - eapply progress_trans. 1: apply (Cnt1 (u <* [1;1]^^s <* [1;1]) j (C n) _ (IncC n)).
    eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
      instantiate (1:= u <* [1;1]^^s <* [1] <* [0;1]^^(S j)).
      apply lp1. }
    eapply pt_eq. 1: apply (IH (S j) u (1+n)).
    apply HF_eq; lia_refl.
Qed.

(* W0(c,d): G(u 0 (10)^(2c+1) 0 (10)^d, C n) -> G(u (10)^(2c+2+d), C(n+2c+1)) *)
Lemma W0k c: forall d u n,
  HF (u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [0] <* [0;1]^^d) (C n) -->+
  HF (u <* [0;1]^^(2*c+2+d)) (C (n+2*c+1)).
Proof.
  induction c as [|c IH]; intros d u n.
  - eapply pt_eq. 1: apply (Cnt0 u d (C n) _ (IncC n)).
    apply HF_eq. 2: f_equal; lia.
    rewrite lp2. reflexivity.
  - eapply progress_trans.
    1: apply (Cnt0 (u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [1]) d (C n) _ (IncC n)).
    eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
      instantiate (1:= u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [1] <* [0;1]^^(S (S d))).
      apply lp2. }
    eapply progress_trans.
    1: apply (Cnt1 (u <* [0] <* [0;1] <* [0;1;0;1]^^c) (S (S d)) _ _ (IncC (1+n))).
    eapply pt_eq. 1: apply (IH (S (S d)) u (1+(1+n))).
    apply HF_eq; lia_refl.
Qed.


(** ** Eat configurations and the macro rules M1-M5 *)

Definition EC p N := HF (0inf <* [0;1]^^p) (C N).

Lemma C_split m i: C (((m*2+1)*2^i-1)*2) = [0;0] *> [1;1]^^i *> [0;0] *> C m.
Proof. unfold C. rewrite BinInc_mul2, BinInc_mulpow2sub1. reflexivity. Qed.

Lemma C_odd n: C (n*2+1) = [1;1] *> C n.
Proof. unfold C. rewrite BinInc_mul2add1. reflexivity. Qed.

Lemma lp4 i (X:side): [0;1;0;1]^^i *> X = [0;1]^^(2*i) *> X.
Proof.
  induction i as [|i IH]. 1: reflexivity.
  replace (2*S i) with (S (S (2*i))) by lia.
  cbn [lpow]. rewrite Str_app_assoc, IH. reflexivity.
Qed.

(* M1: N odd *)
Lemma BS1 p n: EC p (n*2+1) -->+ EC (p+2+p mod 2) (n+p+4).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  eapply progress_trans. 1: apply Y1C.
  eapply pt_eq. 1: apply (Wk (p+2) 0 (1+n)).
  apply HF_eq. 2: f_equal; lia.
  f_equal. f_equal.
  pose proof (Nat.mod_upper_bound p 2). pose proof (Nat.mod_upper_bound (p+2) 2).
  pose proof (Nat.div_mod p 2). pose proof (Nat.div_mod (p+2) 2). lia.
Qed.

(* M2: N = 0 mod 4 *)
Lemma BS2 p n: EC p (n*4) -->+ EC (p+3+p mod 2) (n+p+4).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  eapply progress_trans. 1: apply Y2C.
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1;1]) 0 (C n) _ (IncC n)).
  eapply pt_eq. 1: apply (Wk (p+2) 1 (1+n)).
  apply HF_eq. 2: f_equal; lia.
  f_equal. f_equal. lia.
Qed.

(* M3: N = 2 mod 8 *)
Lemma BS3 p m: EC p (((m*2+1)*2^1-1)*2) -->+ EC (p+4+p mod 2) (m+p+6).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  rewrite C_split.
  eapply progress_trans. 1: apply (Y3 _ 0 (C m)).
  eapply progress_trans. 1: apply (L1 (0inf <* [0;1]^^(p+2) <* [1]) 0).
  eapply progress_trans. 1: apply (ROvf _ 0 m).
  eapply pt_eq. 1: apply (Wk (S (S (p+2))) 0 (1+m)).
  apply HF_eq. 2: f_equal; lia.
  f_equal. f_equal. lia.
Qed.

(* M4: N = 6 mod 16 *)
Lemma BS4 p m: EC p (((m*2+1)*2^2-1)*2) -->+ EC (p+7) (m+5).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  rewrite C_split.
  eapply progress_trans. 1: apply (Y3 _ 1 (C m)).
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1]) 0 _ _ (Inc00 ([0;1;1] *> C m))).
  eapply progress_trans. 1: apply (LEat (S (p+2))).
  eapply progress_trans. 1: apply Y4.
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(S (p+2)+2) <* [0;1;1]) 0 _ _ (IncC _)).
  eapply progress_trans. 1: apply (Cnt011 (0inf <* [0;1]^^(p+2+2)) _ _ (IncC _)).
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2+2) <* [0;1;0]) 1 _ _ (IncC _)).
  eapply pt_eq. 1: apply (Cnt0 (0inf <* [0;1]^^(p+2+2)) 1 _ _ (IncC _)).
  apply HF_eq. 2: f_equal; lia.
  replace (p+7) with (S (S (S (p+2+2)))) by lia. reflexivity.
Qed.

(* M5: N = (2m+1) 2^(t+4) - 2 with t' = t+1 >= 1, precondition 2^t' <= p+7 *)
Lemma BS5 p m t: 2^(S t) <= p+7 ->
  EC p (((m*2+1)*2^(S (S (S t)))-1)*2) -->+ EC (p+8+t) (m+2^(S t)+t+2).
Proof.
  intros Hp.
  pose proof (Nat.pow_nonzero 2 t ltac:(lia)) as HT.
  rewrite Nat.pow_succ_r' in Hp.
  unfold EC.
  (* (a) *)
  eapply progress_trans. 1: apply LEat.
  rewrite C_split.
  eapply progress_trans. 1: apply (Y3 _ (S (S t)) (C m)).
  (* (b) *)
  eapply progress_trans.
  1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1]) 0 _ _ (Inc00 ([0;0]^^(S t) *> [0] *> [1;1] *> C m))).
  (* (c) *)
  eapply progress_trans. 1: apply (LEat (S (p+2))).
  eapply pt3. 1: apply (Y1Q _ ([0;0]^^t *> [0] *> [1;1] *> C m)).
  1: { instantiate (1 := HF (0inf <* [0;1]^^(S (p+2)+2) <* [1]) (Q (S t) 1 (m*2+1))).
    apply HF_eq. 1: reflexivity. unfold Q. rewrite Dk_1, C_odd, !Str_app_assoc. reflexivity. }
  (* (d) *)
  set (i := 2^t-1).
  eapply evstep_progress_trans.
  1: { eapply evstep_trans. 2: apply (W2Q (S t) (m*2+1) i (0inf <* [0;1]^^(p+7-2*2^t)) 0 1).
    2: { rewrite Nat.pow_succ_r'. unfold i. lia. }
    apply evstep_refl'. apply HF_eq. 2: reflexivity.
    rewrite lp4, lpow_add'. cbn [Str_app lpow]. unfold i. lia_refl. }
  (* (e) *)
  eapply progress_trans. 1: apply L1.
  replace (Q (S t) (1+2*i) (m*2+1)) with ([1;1]^^(S t) *> [0;1;1] *> C m).
  2: { unfold Q. replace (1+2*i) with (2^(S t)-1).
    2: { rewrite Nat.pow_succ_r'. unfold i. lia. }
    rewrite Dk_full, C_odd. reflexivity. }
  eapply progress_trans. 1: apply ROvf.
  (* (f) *)
  eapply progress_trans. 1: apply (Bk (S t) 0 _ (1+m)).
  (* (g) *)
  eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
    instantiate (1 := 0inf <* [0;1]^^(p+7-2*2^t) <* [0] <* [0;1] <* [0;1;0;1]^^i <* [0] <* [0;1]^^(S t+0)).
    rewrite lp4. f_equal. f_equal. cbn [Nat.add]. rewrite lpow_shift'. reflexivity. }
  eapply pt_eq. 1: apply W0k.
  apply HF_eq.
  - rewrite lpow_add'. f_equal. f_equal. unfold i. lia.
  - f_equal. unfold i. rewrite Nat.pow_succ_r'. lia.
Qed.

(** ** Start: 171 steps from the blank tape to E(2,4) (after TS) *)

Lemma init: c0 -->* EC 2 4.
Proof.
  unfold EC, HF.
  replace (C 4) with ([0;0;0;0;1;1] *> 0inf) by reflexivity.
  change ([0;1]^^2) with [0;1;0;1].
  solve_init.
Qed.

(** ** Invariant J(p,N): 1 <= N <= 2p *)

Local Open Scope nat_scope.

Lemma step_J p N: 1 <= N <= 2*p ->
  exists p' N', EC p N -->+ EC p' N' /\ 1 <= N' <= 2*p'.
Proof.
  intros HJ.
  destruct (Nat.Even_or_Odd N) as [[K ->]|[n ->]].
  - destruct (Nat.Even_or_Odd K) as [[n ->]|[K' ->]].
    + exists (p+3+p mod 2), (n+p+4). split.
      * replace (2*(2*n)) with (n*4) by lia. apply BS2.
      * lia.
    + lowbitS_cases K'.
      pose proof (Nat.pow_nonzero 2 i ltac:(lia)) as HT.
      destruct i as [|[|i]].
      * exists (p+4+p mod 2), (x+p+6). split.
        -- replace (2*(2*((x*2+1)*2^0-1)+1)) with (((x*2+1)*2^1-1)*2) by (cbn; lia).
           apply BS3.
        -- cbn in HJ. lia.
      * exists (p+7), (x+5). split.
        -- replace (2*(2*((x*2+1)*2^1-1)+1)) with (((x*2+1)*2^2-1)*2) by (cbn; lia).
           apply BS4.
        -- cbn in HJ. lia.
      * rewrite !Nat.pow_succ_r' in HJ.
        set (T := 2^i) in *.
        assert (x <= x*T) by nia.
        exists (p+8+i), (x+2^(S i)+i+2). split.
        -- replace (2*(2*((x*2+1)*2^(S (S i))-1)+1)) with (((x*2+1)*2^(S (S (S i)))-1)*2).
           2: { rewrite !Nat.pow_succ_r'. fold T. lia. }
           apply BS5. rewrite Nat.pow_succ_r'. fold T. lia.
        -- rewrite Nat.pow_succ_r'. fold T. lia.
  - exists (p+2+p mod 2), (n+p+4). split.
    + replace (2*n+1) with (n*2+1) by lia. apply BS1.
    + lia.
Qed.

Lemma nonhalt: ~halts tm c0.
Proof.
  eapply multistep_nonhalt. 1: apply init.
  change (EC 2 4) with ((fun x : nat*nat => let (p,N) := x in EC p N) (2,4)).
  apply progress_nonhalt_cond with (P := fun x : nat*nat => let (p,N) := x in 1 <= N <= 2*p).
  - intros [p N] HJ. destruct (step_J p N HJ) as [p' [N' [H1 H2]]].
    exists (p',N'). split; assumption.
  - lia.
Qed.

(*
1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC          (only F0 is undefined; only C0 enters F)

counter    C(0) = 0^inf,  C(2n) = 0 0 C(n),  C(2n+1) = 1 1 C(n)        (= BinInc [1;1] n)
           D_k(x) = the k digits of x < 2^k, lowest first;   Q_k(x, y) = D_k(x) 0 C(y)
configs    G(w, R) = 0^inf w 0 1 1 B> 0 R          (count configuration: w a word, R a right half-tape)
           E(p, N) = G((10)^p, C(N))                (eat configuration; EC p N is E(p,N) after TS)
           Y(v, R) = 0^inf v 1 1 0 A> R
           R = (11)^k 0 0 R'  has  R+ = (00)^k 1 1 R'

count rules, for every word u and every R = (11)^k 0 0 R'
INC1    G(u 1 (10)^b, R)              -> G(u 0 (10)^b, R+)
INC0    G(u 0 1 0 0 (10)^b, R)        -> G(u 1 0 1 0 (10)^b, R+)
INC011  G(u 1 0 1 1 0 0 (10)^b, R)    -> G(u 0 1 0 1 1 0 (10)^b, R+)
OVF     G(u 1 (10)^b, Q_j(2^j-1, 2m+1)) -> G(u 0 (10)^(b+1) 1^(2j+1), C(m+1))

eat rules
EAT     G(0^inf (10)^b, R)            -> Y((10)^(b+2), R)
Y1      Y(v, (11)^s 0 0 R')           -> G(v 1, (00)^(s-1) 1 1 R')     s >= 1
Y2      Y(v, 0 0 0 0 R')              -> G(v 1 1 1, R')
Y3      Y(v, 0 0 1 1 (11)^s 0 0 R')   -> G(v 1 1, 0^(2s+1) 1 1 R')     s >= 0
Y4      Y(v, 1 1 0 1 1 (11)^i 0 0 R') -> G(v 1 1 0 1, (00)^i 1 1 R')

walks
W(a,b)  G((10)^a 1 (10)^b, C(n))      -> E(a+b+[a odd], n+a+1)          a+1 counts INC1, INC0, INC1, ...
W2      G(u (10)^2 1 (10)^b, R)       -> G(u 1 (10)^(b+2), R++)          INC1, INC0
W0      G(u 0 (10)^(2c+1) 0 (10)^d, R) -> G(u (10)^(2c+2+d), R+^(2c+1))  INC0, INC1, ..., INC0
B(t)    G(u 1^(2t+1), R)              -> G(u 0 (10)^t, R+^(t+1))         t+1 times INC1

eat to eat                                                                  E(p, N) -> E(p', N')
M1  N odd                EAT,Y1; W(p+2,0)                                   p+2+[p odd],  (N+1)/2 + p + 3
M2  N = 0 (mod 4)        EAT,Y2; INC1; W(p+2,1)                             p+3+[p odd],  N/4 + p + 4
M3  N = 8m+2             EAT,Y3(0); OVF(0,0); W(p+4,0)                      p+4+[p odd],  m + p + 6
M4  N = 16m+6            EAT,Y3(1); INC1; EAT,Y4; INC1; INC011; INC1; INC0  p+7,          m + 5
M5  N = (2m+1)2^(t+3)-2, t >= 1, p+7 >= 2^t
                         EAT,Y3(t+1); INC1; EAT,Y1(1); W2^(2^(t-1)-1);
                         OVF(2^t-2, t); B(t); W0(2^(t-1)-1, t)              p+7+t,        m + 2^t + t + 1

invariant J(p, N):  1 <= N <= 2p.   J(p, N) -> exactly one of M1..M5 applies, and J(p', N')
start      c0 -->(165) E(2, 4), so c0 -->(171) EC 2 4;  J(2, 4) holds
*)