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.

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.