Lemma lowbit x: x <> 0 -> 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, 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.

(** 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 (2*(2^h*E)+1) (2*(2^h - 1 + 2^h*O)+1) (2*(2^h*E')) (2*(2^h*O')).
          + 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 E O E' O') as IH.
          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)) (2*(2^h*E)+1) (2*(o1 + 2^h*O)+1) (2*(2^h*E')) (2*(2^h*O')).
          + 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) as [->|Hc1].
      * exact H1.
      * assert (c = 0) as -> by lia.
        apply PAs_eq with (1 + (2^(S (S h)) - 2*(2*o1+1) - 1)) (0 + 2^(S h)*E) (2*o1+1+2^(S h)*O) (2^(S h)*E') (2^(S h)*O').
        -- 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.
        -- lia.
        -- lia.
        -- lia.
        -- 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.
        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.
        rewrite !Nat.pow_succ_r' in IH.
        specialize (IH ltac:(lia) ltac:(lia) HF).
        pose proof (pow_odd_pos P' o1).
        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.

(** ** 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) as [E|E].
  - assert (a = 0) as -> by lia. assert (c = 0) 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, Nat.add_comm, Nat.mul_comm, 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.
  rewrite !Str_app_assoc.
  apply OVo.
Qed.