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. }
  finish.
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. }
  finish.
Qed.