Require Import ssim chain.
From BusyCoq Require Import Individual62.
Require Import Lia ZifyNat List Arith NArith.
Import ListNotations.

Open Scope nat_scope.

(* ===================================================================== *)
(* Lemma T: the visits of one record interval, as a computation on block *)
(* labels.                                                               *)
(* ===================================================================== *)

Lemma runv_add a : forall b st st1 ps1 st2 ps2,
  runv a st = Some (st1, ps1) -> runv b st1 = Some (st2, ps2) -> runv (a + b) st = Some (st2, ps1 ++ ps2).
Proof.
  induction a as [|a IH]; intros b st st1 ps1 st2 ps2 H1 H2.
  - cbn in H1. inversion H1; subst. exact H2.
  - change (S a + b) with (S (a + b)). cbn [runv] in H1 |- *. destruct (vis st) as [[st0 p]|]; [|discriminate].
    destruct (runv a st0) as [[st3 ps3]|] eqn:E; [|discriminate].
    inversion H1; subst. rewrite (IH _ _ _ _ _ _ E H2). reflexivity.
Qed.

Lemma runv_one st st' p : vis st = Some (st', p) -> runv 1 st = Some (st', [p]).
Proof. intros H. cbn. rewrite H. reflexivity. Qed.

Lemma vis3 ls ls' p b i : visit3 ls = Some (ls', p) -> vis (ls, b, i) = Some ((ls', b, i), p).
Proof. intros H. cbn. rewrite H. reflexivity. Qed.

Lemma repeat_add {X} (x : X) n m : repeat x (n + m) = repeat x n ++ repeat x m.
Proof. induction n; cbn in *; congruence. Qed.

Lemma repeat_snoc {X} (x : X) n l : repeat x n ++ x :: l = repeat x (S n) ++ l.
Proof. induction n; cbn in *; congruence. Qed.

Lemma pow3_pos j : 1 <= 3 ^ j.
Proof. induction j; cbn; lia. Qed.

Lemma visit3_U2 j X X' : visit3 X = Some (X', true) -> visit3 (repeat U2 j ++ X) = Some (repeat U0 j ++ X', true).
Proof. intros H. induction j as [|j IH]; cbn; [exact H|]. rewrite IH. reflexivity. Qed.

Lemma cb_U2 j X p X' : cb X p = Some (X', true) -> cb (repeat U2 j ++ X) p = Some (repeat U0 j ++ X', true).
Proof. intros H. induction j as [|j IH]; cbn; [exact H|]. rewrite IH. reflexivity. Qed.

Lemma visit3_full ls : forallb fullb ls = true -> visit3 ls = None.
Proof.
  induction ls as [|s ls IH]; cbn; intros H; [reflexivity|].
  apply andb_prop in H as [H1 H2]. unfold fullb in H1.
  destruct (turn s); [discriminate|]. rewrite IH by exact H2. reflexivity.
Qed.

Lemma fullb_U2 j : forallb fullb (repeat U2 j) = true.
Proof. induction j; cbn; auto. Qed.

Lemma fullb_D0 j : forallb fullb (repeat D0 j) = true.
Proof. induction j; cbn; auto. Qed.

Lemma fullb_app a b : forallb fullb a = true -> forallb fullb b = true -> forallb fullb (a ++ b) = true.
Proof. intros. rewrite forallb_app. apply andb_true_intro. auto. Qed.

Lemma rep_app {X} (x : X) a b : repeat x a ++ repeat x b = repeat x (a + b).
Proof. symmetry. apply repeat_add. Qed.

(* CU: the j blocks nearest the head count from all U0 to all U2 *)
Lemma CU j : forall rest b i,
  runv (3 ^ j - 1) (repeat U0 j ++ rest, b, i) = Some ((repeat U2 j ++ rest, b, i), repeat true (3 ^ j - 1)).
Proof.
  induction j as [|j IH]; intros rest b i; [reflexivity|].
  pose proof (pow3_pos j) as Hp.
  rewrite <-(repeat_snoc U0 j rest), <-(repeat_snoc U2 j rest).
  pose proof (IH (U0 :: rest) b i) as H1.
  assert (H2 : runv 1 (repeat U2 j ++ U0 :: rest, b, i) = Some ((repeat U0 j ++ U1 :: rest, b, i), repeat true 1))
    by (apply runv_one, vis3, visit3_U2; reflexivity).
  pose proof (IH (U1 :: rest) b i) as H3.
  assert (H4 : runv 1 (repeat U2 j ++ U1 :: rest, b, i) = Some ((repeat U0 j ++ U2 :: rest, b, i), repeat true 1))
    by (apply runv_one, vis3, visit3_U2; reflexivity).
  pose proof (IH (U2 :: rest) b i) as H5.
  pose proof (runv_add _ _ _ _ _ _ _ H4 H5) as H45.
  pose proof (runv_add _ _ _ _ _ _ _ H3 H45) as H35.
  pose proof (runv_add _ _ _ _ _ _ _ H2 H35) as H25.
  pose proof (runv_add _ _ _ _ _ _ _ H1 H25) as H.
  rewrite !rep_app in H.
  replace (3 ^ S j - 1) with ((3 ^ j - 1) + (1 + ((3 ^ j - 1) + (1 + (3 ^ j - 1))))) by (cbn; lia).
  exact H.
Qed.

(* CW: a suffix W0 U0^j counts to D0 U2^j *)
Lemma CW j : forall rest b i,
  runv (3 ^ S j - 1) (repeat U0 j ++ W0 :: rest, b, i) =
    Some ((repeat U2 j ++ D0 :: rest, b, i), repeat true (3 ^ S j - 1)).
Proof.
  intros rest b i. pose proof (pow3_pos j) as Hp.
  pose proof (CU j (W0 :: rest) b i) as H1.
  assert (H2 : runv 1 (repeat U2 j ++ W0 :: rest, b, i) = Some ((repeat U0 j ++ W1 :: rest, b, i), repeat true 1))
    by (apply runv_one, vis3, visit3_U2; reflexivity).
  pose proof (CU j (W1 :: rest) b i) as H3.
  assert (H4 : runv 1 (repeat U2 j ++ W1 :: rest, b, i) = Some ((repeat U0 j ++ D0 :: rest, b, i), repeat true 1))
    by (apply runv_one, vis3, visit3_U2; reflexivity).
  pose proof (CU j (D0 :: rest) b i) as H5.
  pose proof (runv_add _ _ _ _ _ _ _ H4 H5) as H45.
  pose proof (runv_add _ _ _ _ _ _ _ H3 H45) as H35.
  pose proof (runv_add _ _ _ _ _ _ _ H2 H35) as H25.
  pose proof (runv_add _ _ _ _ _ _ _ H1 H25) as H.
  rewrite !rep_app in H.
  replace (3 ^ S j - 1) with ((3 ^ j - 1) + (1 + ((3 ^ j - 1) + (1 + (3 ^ j - 1))))) by (cbn; lia).
  exact H.
Qed.

Fixpoint tc (j : nat) : nat :=
  match j with
  | O => 0
  | S O => 2
  | S j' => 3 ^ j + tc j'
  end.

Lemma tc_closed j : 2 * tc (S j) + 5 = 3 ^ S (S j).
Proof.
  induction j as [|j IH]; [reflexivity|].
  change (tc (S (S j))) with (3 ^ S (S j) + tc (S j)). cbn [Nat.pow] in *. lia.
Qed.

(* S3: from U0^j W0 d (d a D block that is not full) to all D *)
Lemma S3 j : forall d d' rest b i, turn d = Some (d', false) ->
  runv (tc (S j) + 1) (repeat U0 j ++ W0 :: d :: rest, b, i) =
    Some ((D2 :: repeat D1 j ++ d' :: rest, b, i), repeat true (tc (S j)) ++ [false]).
Proof.
  induction j as [|j IH]; intros d d' rest b i Hd.
  - pose proof (CW 0 (d :: rest) b i) as H1.
    assert (H2 : runv 1 (repeat U2 0 ++ D0 :: d :: rest, b, i) = Some ((D2 :: d' :: rest, b, i), [false]))
      by (apply runv_one, vis3; cbn; rewrite Hd; reflexivity).
    exact (runv_add _ _ _ _ _ _ _ H1 H2).
  - pose proof (pow3_pos (S (S j))) as Hp.
    pose proof (CW (S j) (d :: rest) b i) as H1.
    assert (H2 : runv 1 (repeat U2 (S j) ++ D0 :: d :: rest, b, i) =
                 Some ((repeat U0 j ++ W0 :: D2 :: d' :: rest, b, i), repeat true 1)).
    { apply runv_one, vis3. rewrite <-repeat_snoc. apply visit3_U2. cbn. rewrite Hd. reflexivity. }
    pose proof (IH D2 D1 (d' :: rest) b i eq_refl) as H3.
    pose proof (runv_add _ _ _ _ _ _ _ H2 H3) as H23.
    pose proof (runv_add _ _ _ _ _ _ _ H1 H23) as H.
    rewrite repeat_snoc, app_assoc, rep_app, app_assoc, rep_app in H.
    change (tc (S (S j))) with (3 ^ S (S j) + tc (S j)).
    replace (3 ^ S (S j) + tc (S j) + 1) with ((3 ^ S (S j) - 1) + (1 + (tc (S j) + 1))) by lia.
    replace (3 ^ S (S j) + tc (S j)) with (3 ^ S (S j) - 1 + 1 + tc (S j)) by lia.
    exact H.
Qed.

(* ---- all-D words count like a plain ternary counter, every exit at phase c ---- *)

Definition isD (s : lab) : bool := match s with D0 | D1 | D2 => true | _ => false end.
Definition dv (s : lab) : nat := match s with D1 => 1 | D0 => 2 | _ => 0 end.
Fixpoint dval (ls : list lab) : nat := match ls with [] => 0 | s :: ls' => dv s + 3 * dval ls' end.
Definition dv1 (b : lab1) : nat := match b with PD1 => 1 | PD0 => 2 | _ => 0 end.
Definition isD1 (b : lab1) : bool := match b with PD0 | PD1 | PD2 => true | _ => false end.

Lemma dval_lt ls : forallb isD ls = true -> dval ls < 3 ^ length ls.
Proof.
  induction ls as [|s ls IH]; cbn; intros H; [lia|].
  apply andb_prop in H as [H1 H2]. specialize (IH H2). destruct s; cbn in *; try discriminate; lia.
Qed.

Lemma dval_max ls : forallb isD ls = true -> dval ls + 1 = 3 ^ length ls -> ls = repeat D0 (length ls).
Proof.
  induction ls as [|s ls IH]; cbn; intros H E; [reflexivity|].
  apply andb_prop in H as [H1 H2]. pose proof (dval_lt ls H2).
  destruct s; cbn in *; try discriminate; try lia. f_equal. apply IH; [exact H2 | lia].
Qed.

Lemma visit3_D ls : forallb isD ls = true -> dval ls + 1 < 3 ^ length ls ->
  exists ls', visit3 ls = Some (ls', false) /\ forallb isD ls' = true /\ dval ls' = dval ls + 1 /\
    length ls' = length ls.
Proof.
  induction ls as [|s ls IH]; cbn; intros H E; [lia|].
  apply andb_prop in H as [H1 H2]. pose proof (dval_lt ls H2).
  destruct s; cbn in H1; try discriminate.
  - assert (E' : dval ls + 1 < 3 ^ length ls) by (cbn in E; lia).
    destruct (IH H2 E') as [ls' [E1 [E2 [E3 E4]]]]. cbn. rewrite E1. cbn.
    exists (D2 :: ls'). cbn. rewrite E2, E3, E4. repeat split; lia.
  - exists (D0 :: ls). cbn. rewrite H2. repeat split; lia.
  - exists (D1 :: ls). cbn. rewrite H2. repeat split; lia.
Qed.

Lemma cb_D0 j : cb (repeat D0 j) false = Some (repeat D2 j, false).
Proof. induction j as [|j IH]; cbn; [reflexivity|]. rewrite IH. reflexivity. Qed.

Lemma isD_D2 j : forallb isD (repeat D2 j) = true.
Proof. induction j; cbn; auto. Qed.

Lemma dval_D2 j : dval (repeat D2 j) = 0.
Proof. induction j; cbn; lia. Qed.

Lemma dval_D1 j : 2 * dval (repeat D1 j) + 1 = 3 ^ j.
Proof. induction j; cbn in *; lia. Qed.

Lemma isD_D1 j : forallb isD (repeat D1 j) = true.
Proof. induction j; cbn; auto. Qed.

Lemma vis_b1 ls b b' p1 ls' p i : forallb fullb ls = true -> turn1 b = Some (b', p1) -> cb ls p1 = Some (ls', p) ->
  vis (ls, b, i) = Some ((ls', b', i), p).
Proof. intros H1 H2 H3. cbn. rewrite (visit3_full _ H1), H1, H2, H3. reflexivity. Qed.

Lemma vis_co ls ls' p i : forallb fullb ls = true -> i < 80 -> cb ls false = Some (ls', p) ->
  vis (ls, PD0, i) = Some ((ls', PD2, S i), p).
Proof.
  intros H1 H2 H3. cbv beta iota zeta delta [vis]. rewrite (visit3_full _ H1), H1. apply Nat.ltb_lt in H2.
  cbv beta iota delta [turn1 lab1_eqb andb]. rewrite H2, H3. reflexivity.
Qed.

Lemma allD n : forall ls b i, forallb isD ls = true -> isD1 b = true ->
  dval ls + 3 ^ length ls * dv1 b + n + 1 = 3 ^ S (length ls) ->
  runv n (ls, b, i) = Some ((repeat D0 (length ls), PD0, i), repeat false n).
Proof.
  induction n as [|n IH]; intros ls b i H1 H2 E; pose proof (dval_lt ls H1) as Hl; cbn [Nat.pow] in E.
  - assert (Eb : b = PD0) by (destruct b; cbn in *; try discriminate; try reflexivity; lia).
    subst b. cbn [dv1] in E. rewrite <-(dval_max ls H1) by lia. reflexivity.
  - destruct (Nat.lt_ge_cases (dval ls + 1) (3 ^ length ls)) as [Hlt|Hge].
    + destruct (visit3_D ls H1 Hlt) as [ls' [E1 [E2 [E3 E4]]]].
      cbn [runv]. rewrite (vis3 _ _ _ b i E1).
      rewrite (IH ls' b i E2 H2) by (rewrite E3, E4; cbn [Nat.pow]; lia). rewrite E4. reflexivity.
    + assert (Hd : dval ls + 1 = 3 ^ length ls) by lia.
      pose proof (dval_max ls H1 Hd) as Hr. remember (length ls) as m eqn:Em. subst ls.
      destruct b; cbn in H2; try discriminate; cbn [dv1] in E; [lia| |].
      * cbn [runv]. rewrite (vis_b1 _ PD1 PD0 false _ _ i (fullb_D0 m) eq_refl (cb_D0 m)).
        rewrite (IH (repeat D2 m) PD0 i (isD_D2 m) eq_refl) by (rewrite dval_D2, repeat_length; cbn; lia).
        rewrite repeat_length. reflexivity.
      * cbn [runv]. rewrite (vis_b1 _ PD2 PD1 false _ _ i (fullb_D0 m) eq_refl (cb_D0 m)).
        rewrite (IH (repeat D2 m) PD1 i (isD_D2 m) eq_refl) by (rewrite dval_D2, repeat_length; cbn; lia).
        rewrite repeat_length. reflexivity.
Qed.

Lemma cyc m i : i < 80 ->
  runv (3 ^ S m) (repeat D0 m, PD0, i) = Some ((repeat D0 m, PD0, S i), repeat false (3 ^ S m)).
Proof.
  intros Hi. pose proof (pow3_pos (S m)) as Hp.
  replace (3 ^ S m) with (1 + (3 ^ S m - 1)) by lia. rewrite repeat_add.
  eapply runv_add; [apply runv_one, (vis_co _ _ _ _ (fullb_D0 m) Hi (cb_D0 m))|].
  pose proof (allD (3 ^ S m - 1) (repeat D2 m) PD2 (S i) (isD_D2 m) eq_refl) as A.
  rewrite dval_D2, repeat_length in A. apply A. cbn [dv1]. lia.
Qed.

Lemma cycs c : forall m i, i + c <= 80 ->
  runv (c * 3 ^ S m) (repeat D0 m, PD0, i) = Some ((repeat D0 m, PD0, i + c), repeat false (c * 3 ^ S m)).
Proof.
  induction c as [|c IH]; intros m i Hi; [rewrite Nat.add_0_r; reflexivity|].
  change (S c * 3 ^ S m) with (3 ^ S m + c * 3 ^ S m).
  rewrite repeat_add. eapply runv_add; [apply cyc; lia|].
  replace (i + S c) with (S i + c) by lia. apply IH. lia.
Qed.

Lemma rep_app_cons {X} (x : X) a b l : repeat x a ++ (repeat x b ++ l) = repeat x (a + b) ++ l.
Proof. rewrite app_assoc, rep_app. reflexivity. Qed.

Lemma odd_pow3 j : exists k, 3 ^ j = 2 * k + 1.
Proof. induction j as [|j [k Hk]]; [exists 0; reflexivity|]. exists (3 * k + 1). cbn [Nat.pow]. lia. Qed.

Lemma half9 j : 2 * ((9 * 3 ^ j + 1) / 2) = 9 * 3 ^ j + 1.
Proof.
  destruct (odd_pow3 j) as [k Hk]. rewrite Hk.
  replace (9 * (2 * k + 1) + 1) with ((9 * k + 5) * 2) by lia. rewrite Nat.div_mul by lia. lia.
Qed.

(* Lemma T: one whole interval of visits, m = K - 1 blocks with m = 3 *)
Lemma interval m : 2 <= m ->
  exists T, 2 * T + 5 = 3 ^ S (S m) /\
  runv (81 * 3 ^ S m - 1) (repeat U0 m, P0, 0) =
    Some ((repeat D0 m, PD0, 80), repeat true T ++ repeat false (81 * 3 ^ S m - 1 - T)).
Proof.
  intros Hm. destruct m as [|[|m]]; [lia|lia|].
  pose proof (half9 (S m)) as Hh.
  set (y := 3 ^ S m) in *.
  assert (Hy : 1 <= y) by apply pow3_pos.
  assert (E3 : 3 ^ S (S m) = 3 * y) by reflexivity.
  assert (E9 : 3 ^ S (S (S m)) = 9 * y) by (cbn [Nat.pow]; unfold y; cbn [Nat.pow]; lia).
  pose proof (tc_closed m) as Etc. rewrite E3 in Etc.
  (* phase 1: block 1 plays the role of W *)
  assert (H1 : runv (3 ^ S (S (S m)) - 1) (repeat U0 (S (S m)), P0, 0) =
               Some ((repeat U2 (S (S m)), PD0, 0), repeat true (3 ^ S (S (S m)) - 1))).
  { pose proof (CU (S (S m)) [] P0 0) as A1. rewrite !app_nil_r in A1.
    assert (A2 : runv 1 (repeat U2 (S (S m)), P0, 0) = Some ((repeat U0 (S (S m)), P1, 0), repeat true 1)).
    { apply runv_one, (vis_b1 _ _ _ true); [apply fullb_U2 | reflexivity |].
      pose proof (cb_U2 (S (S m)) [] true [] eq_refl) as C. rewrite !app_nil_r in C. exact C. }
    pose proof (CU (S (S m)) [] P1 0) as A3. rewrite !app_nil_r in A3.
    assert (A4 : runv 1 (repeat U2 (S (S m)), P1, 0) = Some ((repeat U0 (S (S m)), PD0, 0), repeat true 1)).
    { apply runv_one, (vis_b1 _ _ _ true); [apply fullb_U2 | reflexivity |].
      pose proof (cb_U2 (S (S m)) [] true [] eq_refl) as C. rewrite !app_nil_r in C. exact C. }
    pose proof (CU (S (S m)) [] PD0 0) as A5. rewrite !app_nil_r in A5.
    pose proof (runv_add _ _ _ _ _ _ _ A4 A5) as A45.
    pose proof (runv_add _ _ _ _ _ _ _ A3 A45) as A35.
    pose proof (runv_add _ _ _ _ _ _ _ A2 A35) as A25.
    pose proof (runv_add _ _ _ _ _ _ _ A1 A25) as A.
    rewrite !rep_app in A. rewrite E3 in A. rewrite E9.
    replace (9 * y - 1) with (3 * y - 1 + (1 + (3 * y - 1 + (1 + (3 * y - 1))))) by lia. exact A. }
  (* carry-out 1 *)
  assert (H2 : runv 1 (repeat U2 (S (S m)), PD0, 0) = Some ((repeat U0 (S m) ++ [W0], PD2, 1), repeat true 1)).
  { apply runv_one, vis_co; [apply fullb_U2 | lia |].
    rewrite <-(app_nil_r (repeat U2 (S (S m)))), <-(repeat_snoc U2 (S m) []). apply cb_U2. reflexivity. }
  (* W-suffix of length S (S m) then the turn of block 1 *)
  pose proof (CW (S m) [] PD2 1) as H3.
  assert (H4 : runv 1 (repeat U2 (S m) ++ [D0], PD2, 1) = Some ((repeat U0 m ++ [W0; D2], PD1, 1), repeat true 1)).
  { apply runv_one, (vis_b1 _ _ _ false).
    - apply fullb_app; [apply fullb_U2 | reflexivity].
    - reflexivity.
    - rewrite <-(repeat_snoc U2 m [D0]). apply cb_U2. reflexivity. }
  pose proof (S3 m D2 D1 [] PD1 1 eq_refl) as H5.
  rewrite repeat_snoc, app_nil_r in H5.
  (* all-D counting up to the second carry-out *)
  assert (H6 : runv ((9 * y + 1) / 2) (D2 :: repeat D1 (S m), PD1, 1) =
               Some ((repeat D0 (S (S m)), PD0, 1), repeat false ((9 * y + 1) / 2))).
  { pose proof (dval_D1 (S m)) as Ed. fold y in Ed.
    pose proof (allD ((9 * y + 1) / 2) (D2 :: repeat D1 (S m)) PD1 1 ltac:(cbn; apply isD_D1) eq_refl) as A.
    cbn [length dval dv dv1] in A. rewrite repeat_length in A. apply A.
    rewrite E3, E9. lia. }
  (* 79 more carry-outs in the all-D regime *)
  pose proof (cycs 79 (S (S m)) 1 ltac:(lia)) as H7. rewrite E9 in H7.
  pose proof (runv_add _ _ _ _ _ _ _ H6 H7) as H67.
  pose proof (runv_add _ _ _ _ _ _ _ H5 H67) as H57.
  pose proof (runv_add _ _ _ _ _ _ _ H4 H57) as H47.
  pose proof (runv_add _ _ _ _ _ _ _ H3 H47) as H37.
  pose proof (runv_add _ _ _ _ _ _ _ H2 H37) as H27.
  pose proof (runv_add _ _ _ _ _ _ _ H1 H27) as H.
  rewrite rep_app, <-app_assoc in H. change [false] with (repeat false 1) in H.
  rewrite rep_app, !rep_app_cons in H. rewrite E3, E9 in H.
  assert (E27 : 3 ^ S (S (S (S m))) = 27 * y) by (unfold y; cbn [Nat.pow]; lia).
  exists (9 * y - 1 + 1 + (3 * y - 1) + 1 + tc (S m)). split; [rewrite E27; lia|].
  rewrite E9.
  replace (81 * (9 * y) - 1)
    with (9 * y - 1 + (1 + (3 * y - 1 + (1 + (tc (S m) + 1 + ((9 * y + 1) / 2 + 79 * (9 * y)))))))
    by lia.
  rewrite H.
  replace (9 * y - 1 + (1 + (3 * y - 1 + (1 + (tc (S m) + 1 + ((9 * y + 1) / 2 + 79 * (9 * y))))))
           - (9 * y - 1 + 1 + (3 * y - 1) + 1 + tc (S m)))
    with (1 + ((9 * y + 1) / 2 + 79 * (9 * y))) by lia.
  reflexivity.
Qed.

(* the chain side of one interval, on the machine *)
Lemma interval_tm m nus R R' : 2 <= m -> length nus = m ->
  (forall T, 2 * T + 5 = 3 ^ S (S m) -> EpSeq (repeat true T ++ repeat false (81 * 3 ^ S m - 1 - T)) R R') ->
  Gc (repeat U0 m, P0, 0) nus R -->* Gc (repeat D0 m, PD0, 80) nus R'.
Proof.
  intros Hm Hl HE. destruct (interval m Hm) as [T [ET Hr]].
  apply (runv_spec _ _ _ _ _ _ _ Hr); [cbn; rewrite repeat_length; auto | apply HE, ET].
Qed.

(* the record visit: carry-out at all D0, left episode 80 (the left record), carry back to all D2 *)
Lemma record_visit m nus R : length nus = m ->
  Gc (repeat D0 m, PD0, 80) nus R -->+ chs (repeat D2 m) nus (b1s PD2 (LWs 81)) {{B}}> R.
Proof.
  intros Hl. cbn [Gc].
  eapply evstep_progress_trans; [apply pass_spec; [apply fullb_D0 | rewrite repeat_length; auto]|].
  unfold b1s. eapply progress_trans; [apply blk1_pass|].
  eapply progress_trans; [apply lw_ep; lia|].
  eapply progress_evstep_trans; [apply blk1_back|].
  apply (cb_spec _ false _ false); [apply cb_D0 | rewrite repeat_length; auto].
Qed.