Require Import ssim chain count right regroup step.
From BusyCoq Require Import Individual62.
Require Import Lia ZifyNat List Arith NArith ZArith.
Import ListNotations.
Open Scope nat_scope.

Definition wv (c a t : N) : N := (c + a * t)%N.

Lemma evN_tl1 c a t : evN [t] (tl1 c a) = wv c a t.
Proof. unfold evN, tl1, wv. cbn [lc lv dot]. lia. Qed.

Lemma take_step L first4 Re' Rs nu sg X' :
  reach 100000 (Rc B (L, TV 0) (first4, TV 1)) (Rc A (comp_runs sg (blk U0), TV 0) ([], TV 1)) = true ->
  ep_run true Re' = Some Rs ->
  ev_runs nu L X' {{B}}> ev_runs nu first4 (evR nu Re') -->+
    ev_runs (map (evN nu) sg) (blk U0) X' <{{D}} evR nu Rs.
Proof.
  intros H1 H2. eapply progress_evstep_trans.
  - exact (reach_spec _ _ _ H1 nu (sg2 X' (evR nu Re'))).
  - change (ev_runs nu (comp_runs sg (blk U0)) X' {{A}}> evR nu Re' -->*
            ev_runs (map (evN nu) sg) (blk U0) X' <{{D}} evR nu Rs).
    rewrite ev_runs_comp. apply (ep_run_spec _ _ _ H2 nu).
Qed.

Lemma split4 nu r1 r2 r3 b c v rest X :
  ev_runs nu (r1 :: r2 :: r3 :: (b, LF (3 + c) v) :: rest) X =
  ev_runs nu [r1; r2; r3; (b, cn 3)] (ev_runs nu ((sneg b, LF c v) :: rest) X).
Proof.
  destruct r1 as [b1 n1], r2 as [b2 n2], r3 as [b3 n3]. cbn [ev_runs].
  assert (E : alt b (ev nu (LF (3 + c) v)) = alt b 3 ++ alt (sneg b) (ev nu (LF c v))).
  { unfold ev. cbn [lc lv].
    replace (N.to_nat (3 + c + dot v nu)) with (3 + N.to_nat (c + dot v nu)) by lia.
    rewrite alt_add. reflexivity. }
  rewrite E, Str_app_assoc. reflexivity.
Qed.

(* ---------- r0 -> r1 (take in x1, x2, x3) ---------- *)

Definition W0t := wv 6227 49896.
Definition W0s := wv 2069 16632.
Definition W1t := wv 168389 1347192.
Definition W1s := wv 56123 449064.
Definition W1a := wv 18701 149688.
Definition W1I := wv 6227 49896.
Definition W1u := wv 2069 16632.   (* t gap of block K-1 *)

Definition sig01 : list lf := [tl1 168389 1347192; tl1 56123 449064; tl1 18701 149688; tl1 6227 49896]%N.
Definition f4_r0 : list run := [(S0, tl1 74804 598752); (S1, tl1 224496 1796256); (S0, tl1 673560 5388768); (S1, cn 3)]%N.
Definition Rp_r0 : list run := [(S0, tl1 2020748 16166304); (S1, cn 7); (S1, tl1 551120 4408992); (S0, tl1 1564798 12518388); (S1, cn 1)]%N.

Lemma rec_r0a : reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 24910 199584)], TV 0) (f4_r0, TV 1))
  (Rc A (comp_runs sig01 (blk U0), TV 0) ([], TV 1)) = true.
Proof. vm_compute. reflexivity. Qed.
Lemma rec_r0b : ep_run true Rp_r0 = Some Rs_r1.
Proof. vm_compute. reflexivity. Qed.

Lemma split_r0 t : evR [t] Re_r0 = ev_runs [t] f4_r0 (evR [t] Rp_r0).
Proof.
  unfold evR, Re_r0, f4_r0, Rp_r0, tl1.
  change (2020751)%N with (3 + 2020748)%N. rewrite split4. reflexivity.
Qed.

Lemma step_r0 t f1 f2 deep :
  chs (repeat D2 (S (length deep))) ([W0t t; W0s t; f1; f2] :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r0 -->+
  Gc (repeat U0 (S (S (length deep))), P0, 0)
     ([W1t t; W1s t; W1a t; W1I t] :: [W0s t; f1; f2; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r1).
Proof.
  pose proof (regroup ([W0t t; W0s t; f1; f2] :: deep) 0%N _ (b1s P0 (LWs 0)) regroup_b1) as E.
  cbn [length] in E. rewrite E. clear E. cbn [rtop rshift nth Gc].
  set (X' := chs (repeat U0 (S (length deep))) ([W0s t; f1; f2; rtop deep 0%N] :: rshift deep 0%N) (b1s P0 (LWs 0))).
  replace (2 + 4 * N.to_nat (W0t t)) with (ev [t] (tl1 24910 199584)) by (unfold ev, W0t, wv, tl1; cbn [lc lv dot]; lia).
  change (alt S0 1 *> (alt S0 (ev [t] (tl1 24910 199584)) *> X')) with (ev_runs [t] [(S0, cn 1); (S0, tl1 24910 199584)] X').
  rewrite split_r0.
  replace [W1t t; W1s t; W1a t; W1I t] with (map (evN [t]) sig01)
    by (unfold sig01; cbn [map]; rewrite !evN_tl1; reflexivity).
  change (chs (repeat U0 (S (S (length deep)))) (map (evN [t]) sig01 :: [W0s t; f1; f2; rtop deep 0%N] :: rshift deep 0%N)
            (b1s P0 (LWs 0))) with (ev_runs (map (evN [t]) sig01) (blk U0) X').
  apply take_step; [exact rec_r0a | exact rec_r0b].
Qed.

(* ---------- r3 -> r4 (drop 1) ---------- *)

Definition W3t := wv 18701 149688.

Lemma rec_r3_ok : reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 74806 598752)], TV 0) (Re_r3, T0)) (Lc D ([], TV 0) (Rs_r4, T0)) = true.
Proof. vm_compute. reflexivity. Qed.

Lemma step_r3 t f1 f2 f3 deep :
  chs (repeat D2 (S (length deep))) ([W3t t; f1; f2; f3] :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r3 -->+
  Gc (repeat U0 (S (length deep)), P0, 0) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r4).
Proof.
  pose proof (regroup ([W3t t; f1; f2; f3] :: deep) 0%N _ (b1s P0 (LWs 0)) regroup_b1) as E.
  cbn [length] in E. rewrite E. clear E. cbn [rtop rshift nth Gc].
  set (X' := chs (repeat U0 (S (length deep))) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (b1s P0 (LWs 0))).
  replace (2 + 4 * N.to_nat (W3t t)) with (ev [t] (tl1 74806 598752)) by (unfold ev, W3t, wv, tl1; cbn [lc lv dot]; lia).
  change (alt S0 1 *> (alt S0 (ev [t] (tl1 74806 598752)) *> X')) with (ev_runs [t] [(S0, cn 1); (S0, tl1 74806 598752)] X').
  apply drop_step, rec_r3_ok.
Qed.

(* ---------- r1 -> r2 (drop 5) ---------- *)

Definition sig12 : list lf := [tl1 56123 449064; tl1 18701 149688; tl1 6227 49896; tl1 2069 16632]%N.

Lemma rec_r1_ok : reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 673558 5388768)] ++ comp_runs sig12 (blk U0), TV 0) (Re_r1, T0))
  (Lc D ([], TV 0) (Rs_r2, T0)) = true.
Proof. vm_compute. reflexivity. Qed.

Lemma step_r1 t f1 f2 f3 deep :
  chs (repeat D2 (S (S (length deep)))) ([W1t t; W1s t; W1a t; W1I t] :: [W1u t; f1; f2; f3] :: deep) (b1s PD2 (LWs 81))
    {{B}}> evR [t] Re_r1 -->+
  Gc (repeat U0 (S (length deep)), P0, 0) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r2).
Proof.
  pose proof (regroup ([W1t t; W1s t; W1a t; W1I t] :: [W1u t; f1; f2; f3] :: deep) 0%N _ (b1s P0 (LWs 0)) regroup_b1) as E.
  cbn [length] in E. rewrite E. clear E. cbn [rtop rshift nth Gc].
  set (X' := chs (repeat U0 (S (length deep))) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (b1s P0 (LWs 0))).
  change (chs (repeat U0 (S (S (length deep)))) ([W1s t; W1a t; W1I t; W1u t] :: [f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N)
            (b1s P0 (LWs 0))) with (ev_runs [W1s t; W1a t; W1I t; W1u t] (blk U0) X').
  replace [W1s t; W1a t; W1I t; W1u t] with (map (evN [t]) sig12) by (unfold sig12; cbn [map]; rewrite !evN_tl1; reflexivity).
  rewrite <-ev_runs_comp.
  replace (2 + 4 * N.to_nat (W1t t)) with (ev [t] (tl1 673558 5388768)) by (unfold ev, W1t, wv, tl1; cbn [lc lv dot]; lia).
  change (alt S0 1 *> (alt S0 (ev [t] (tl1 673558 5388768)) *> ev_runs [t] (comp_runs sig12 (blk U0)) X'))
    with (ev_runs [t] ([(S0, cn 1); (S0, tl1 673558 5388768)] ++ comp_runs sig12 (blk U0)) X').
  apply drop_step, rec_r1_ok.
Qed.

(* ---------- r2 -> r3 (take in x1, x2, x3; the last t gap of the chain is free) ---------- *)

Definition xv : lf := LF 2 [0; 4]%N.
Definition sig23 : list lf := [tl1 18701 149688; tl1 6227 49896; tl1 2069 16632; LF 0 [0; 1]]%N.
Definition f4_r2 : list run := [(S0, tl1 8276 66528); (S1, tl1 24912 199584); (S0, tl1 74808 598752); (S1, cn 3)]%N.
Definition Rp_r2 : list run := [(S0, tl1 224492 1796256); (S1, tl1 673559 5388768); (S1, tl1 2020752 16166304);
  (S0, tl1 6062328 48498912); (S1, cn 3); (S1, tl1 1564801 12518388); (S1, cn 1)]%N.

Lemma rec_r2a : reach 100000 (Rc B ([(S0, cn 1); (S0, xv)], TV 0) (f4_r2, TV 1))
  (Rc A (comp_runs sig23 (blk U0), TV 0) ([], TV 1)) = true.
Proof. vm_compute. reflexivity. Qed.
Lemma rec_r2b : ep_run true Rp_r2 = Some Rs_r3.
Proof. vm_compute. reflexivity. Qed.

Lemma split_r2 nu : evR nu Re_r2 = ev_runs nu f4_r2 (evR nu Rp_r2).
Proof.
  unfold evR, Re_r2, f4_r2, Rp_r2, tl1.
  change (224495)%N with (3 + 224492)%N. rewrite split4. reflexivity.
Qed.

Lemma step_r2 t q deep :
  chs (repeat D2 (S (length deep))) (q :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r2 -->+
  Gc (repeat U0 (S (S (length deep))), P0, 0)
     ([W3t t; wv 6227 49896 t; wv 2069 16632 t; nth 0 q 0%N] :: rshift (q :: deep) 0%N) (evR [t] Rs_r3).
Proof.
  pose proof (regroup (q :: deep) 0%N _ (b1s P0 (LWs 0)) regroup_b1) as E.
  cbn [length] in E. rewrite E. clear E. cbn [rtop Gc].
  set (xK := nth 0 q 0%N).
  set (X' := chs (repeat U0 (S (length deep))) (rshift (q :: deep) 0%N) (b1s P0 (LWs 0))).
  replace (evR [t] Re_r2) with (evR [t; xK] Re_r2) by reflexivity.
  replace (evR [t] Rs_r3) with (evR [t; xK] Rs_r3) by reflexivity.
  replace (2 + 4 * N.to_nat xK) with (ev [t; xK] xv) by (unfold ev, xv; cbn [lc lv dot]; lia).
  change (alt S0 1 *> (alt S0 (ev [t; xK] xv) *> X')) with (ev_runs [t; xK] [(S0, cn 1); (S0, xv)] X').
  replace [W3t t; wv 6227 49896 t; wv 2069 16632 t; xK] with (map (evN [t; xK]) sig23)
    by (unfold sig23, W3t, wv, tl1, evN; cbn [map lc lv dot]; f_equal; [lia|f_equal; [lia|f_equal; [lia|f_equal; lia]]]).
  change (chs (repeat U0 (S (S (length deep)))) (map (evN [t; xK]) sig23 :: rshift (q :: deep) 0%N) (b1s P0 (LWs 0)))
    with (ev_runs (map (evN [t; xK]) sig23) (blk U0) X').
  rewrite split_r2.
  apply take_step; [exact rec_r2a | exact rec_r2b].
Qed.

(* ---------- r4 -> r5 (take in x1, x2, x3; next epoch, u -> 9 u, t -> 1 + 9 t) ---------- *)

Definition sub9_lf (l : lf) : lf := match lv l with [a] => LF (lc l + a) [9 * a] | _ => l end%N.
Definition sub9 (rs : list run) : list run := map (fun r => (fst r, sub9_lf (snd r))) rs.

Lemma ev_runs_sub9 t rs X : forallb (fun r => Nat.leb (length (lv (snd r))) 1) rs = true ->
  ev_runs [t] (sub9 rs) X = ev_runs [(1 + 9 * t)%N] rs X.
Proof.
  unfold sub9. induction rs as [|[b l] rs IH]; intros H; [reflexivity|].
  cbn [forallb] in H. apply andb_prop in H as [H1 H2]. cbn [map ev_runs fst snd]. rewrite IH by exact H2.
  f_equal. f_equal. unfold sub9_lf, ev. destruct l as [c [|a [|a' v]]]; cbn [lc lv dot length Nat.leb] in *; [reflexivity | f_equal; ring | discriminate].
Qed.

Lemma evR_sub9_r5 t : evR [t] (sub9 Rs_r5) = evR [(1 + 9 * t)%N] Rs_r5.
Proof. unfold evR. apply ev_runs_sub9. reflexivity. Qed.

Definition sig45 : list lf := [tl1 168389 1347192; tl1 56123 449064; tl1 18701 149688; LF 0 [0; 1]]%N.
Definition f4_r4 : list run := [(S0, tl1 74804 598752); (S1, tl1 224496 1796256); (S0, tl1 673560 5388768); (S1, cn 3)]%N.
Definition Rp_r4 : list run := [(S0, tl1 2020748 16166304); (S1, tl1 6062327 48498912); (S1, cn 7);
  (S1, tl1 88573 708588); (S1, tl1 17478488 139828032); (S0, cn 2)]%N.

Lemma rec_r4a : reach 100000 (Rc B ([(S0, cn 1); (S0, xv)], TV 0) (f4_r4, TV 1))
  (Rc A (comp_runs sig45 (blk U0), TV 0) ([], TV 1)) = true.
Proof. vm_compute. reflexivity. Qed.
Lemma rec_r4b : ep_run true Rp_r4 = Some (sub9 Rs_r5).
Proof. vm_compute. reflexivity. Qed.

Lemma split_r4 nu : evR nu Re_r4 = ev_runs nu f4_r4 (evR nu Rp_r4).
Proof.
  unfold evR, Re_r4, f4_r4, Rp_r4, tl1.
  change (2020751)%N with (3 + 2020748)%N. rewrite split4. reflexivity.
Qed.

Lemma step_r4 t q deep :
  chs (repeat D2 (S (length deep))) (q :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r4 -->+
  Gc (repeat U0 (S (S (length deep))), P0, 0)
     ([W5t (1 + 9 * t); W5s (1 + 9 * t); W5a (1 + 9 * t); nth 0 q 0%N] :: rshift (q :: deep) 0%N)
     (evR [(1 + 9 * t)%N] Rs_r5).
Proof.
  pose proof (regroup (q :: deep) 0%N _ (b1s P0 (LWs 0)) regroup_b1) as E.
  cbn [length] in E. rewrite E. clear E. cbn [rtop Gc].
  set (xK := nth 0 q 0%N).
  set (X' := chs (repeat U0 (S (length deep))) (rshift (q :: deep) 0%N) (b1s P0 (LWs 0))).
  replace (evR [t] Re_r4) with (evR [t; xK] Re_r4) by reflexivity.
  rewrite <-evR_sub9_r5.
  replace (evR [t] (sub9 Rs_r5)) with (evR [t; xK] (sub9 Rs_r5)) by reflexivity.
  replace (2 + 4 * N.to_nat xK) with (ev [t; xK] xv) by (unfold ev, xv; cbn [lc lv dot]; lia).
  change (alt S0 1 *> (alt S0 (ev [t; xK] xv) *> X')) with (ev_runs [t; xK] [(S0, cn 1); (S0, xv)] X').
  replace [W5t (1 + 9 * t); W5s (1 + 9 * t); W5a (1 + 9 * t); xK] with (map (evN [t; xK]) sig45)
    by (unfold sig45, W5t, W5s, W5a, tl1, evN; cbn [map lc lv dot]; f_equal; [lia|f_equal; [lia|f_equal; [lia|f_equal; lia]]]).
  change (chs (repeat U0 (S (S (length deep)))) (map (evN [t; xK]) sig45 :: rshift (q :: deep) 0%N) (b1s P0 (LWs 0)))
    with (ev_runs (map (evN [t; xK]) sig45) (blk U0) X').
  rewrite split_r4.
  apply take_step; [exact rec_r4a | exact rec_r4b].
Qed.

Lemma S_r0 e t f1 f2 deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 1 + 2 * e ->
  Gc (repeat U0 (S (length deep)), P0, 0) ([W0t t; W0s t; f1; f2] :: deep) (evR [t] Rs_r0) -->+
  Gc (repeat U0 (S (S (length deep))), P0, 0) ([W1t t; W1s t; W1a t; W1I t] :: [W0s t; f1; f2; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r1).
Proof.
  intros He Ht Hl.
  eapply evstep_progress_trans; [apply interval_tm; [lia | reflexivity |]|].
  - intros T ET. pose proof (prog_check_spec _ _ _ _ _ int_r0 [t]) as HP.
    assert (E3 : 3 ^ S (S (S (length deep))) = 81 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (S (1 + 2 * e)))) with (4 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    assert (E2 : 3 ^ S (S (length deep)) = 27 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (1 + 2 * e))) with (3 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    rewrite E3 in ET. rewrite E2.
    replace T with (ev [t] (tl1 3278 26244)) by (unfold ev, tl1; cbn [lc lv dot]; lia).
    replace (81 * (27 * 81 * (1 + 8 * N.to_nat t)) - 1 - ev [t] (tl1 3278 26244)) with (ev [t] (tl1 173868 1390932))
      by (unfold ev, tl1; cbn [lc lv dot]; lia).
    exact HP.
  - eapply progress_trans; [apply record_visit; reflexivity|].
    apply step_r0.
Qed.

Lemma S_r1 e t f1 f2 f3 deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 1 + 2 * e ->
  Gc (repeat U0 (S (S (length deep))), P0, 0) ([W1t t; W1s t; W1a t; W1I t] :: [W1u t; f1; f2; f3] :: deep) (evR [t] Rs_r1) -->+
  Gc (repeat U0 (S (length deep)), P0, 0) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r2).
Proof.
  intros He Ht Hl.
  eapply evstep_progress_trans; [apply interval_tm; [lia | reflexivity |]|].
  - intros T ET. pose proof (prog_check_spec _ _ _ _ _ int_r1 [t]) as HP.
    assert (E3 : 3 ^ S (S (S (S (length deep)))) = 243 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (S (S (1 + 2 * e))))) with (5 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    assert (E2 : 3 ^ S (S (S (length deep))) = 81 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (S (1 + 2 * e)))) with (4 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    rewrite E3 in ET. rewrite E2.
    replace T with (ev [t] (tl1 9839 78732)) by (unfold ev, tl1; cbn [lc lv dot]; lia).
    replace (81 * (81 * 81 * (1 + 8 * N.to_nat t)) - 1 - ev [t] (tl1 9839 78732)) with (ev [t] (tl1 521601 4172796))
      by (unfold ev, tl1; cbn [lc lv dot]; lia).
    exact HP.
  - eapply progress_trans; [apply record_visit; reflexivity|].
    apply step_r1.
Qed.

Lemma S_r2 e t q deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 1 + 2 * e ->
  Gc (repeat U0 (S (length deep)), P0, 0) (q :: deep) (evR [t] Rs_r2) -->+
  Gc (repeat U0 (S (S (length deep))), P0, 0) ([W3t t; wv 6227 49896 t; wv 2069 16632 t; nth 0 q 0%N] :: rshift (q :: deep) 0%N) (evR [t] Rs_r3).
Proof.
  intros He Ht Hl.
  eapply evstep_progress_trans; [apply interval_tm; [lia | reflexivity |]|].
  - intros T ET. pose proof (prog_check_spec _ _ _ _ _ int_r2 [t]) as HP.
    assert (E3 : 3 ^ S (S (S (length deep))) = 81 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (S (1 + 2 * e)))) with (4 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    assert (E2 : 3 ^ S (S (length deep)) = 27 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (1 + 2 * e))) with (3 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    rewrite E3 in ET. rewrite E2.
    replace T with (ev [t] (tl1 3278 26244)) by (unfold ev, tl1; cbn [lc lv dot]; lia).
    replace (81 * (27 * 81 * (1 + 8 * N.to_nat t)) - 1 - ev [t] (tl1 3278 26244)) with (ev [t] (tl1 173868 1390932))
      by (unfold ev, tl1; cbn [lc lv dot]; lia).
    exact HP.
  - eapply progress_trans; [apply record_visit; reflexivity|].
    apply step_r2.
Qed.

Lemma S_r3 e t f1 f2 f3 deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 2 + 2 * e ->
  Gc (repeat U0 (S (length deep)), P0, 0) ([W3t t; f1; f2; f3] :: deep) (evR [t] Rs_r3) -->+
  Gc (repeat U0 (S (length deep)), P0, 0) ([f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r4).
Proof.
  intros He Ht Hl.
  eapply evstep_progress_trans; [apply interval_tm; [lia | reflexivity |]|].
  - intros T ET. pose proof (prog_check_spec _ _ _ _ _ int_r3 [t]) as HP.
    assert (E3 : 3 ^ S (S (S (length deep))) = 243 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (S (2 + 2 * e)))) with (5 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    assert (E2 : 3 ^ S (S (length deep)) = 81 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (2 + 2 * e))) with (4 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    rewrite E3 in ET. rewrite E2.
    replace T with (ev [t] (tl1 9839 78732)) by (unfold ev, tl1; cbn [lc lv dot]; lia).
    replace (81 * (81 * 81 * (1 + 8 * N.to_nat t)) - 1 - ev [t] (tl1 9839 78732)) with (ev [t] (tl1 521601 4172796))
      by (unfold ev, tl1; cbn [lc lv dot]; lia).
    exact HP.
  - eapply progress_trans; [apply record_visit; reflexivity|].
    apply step_r3.
Qed.

Lemma S_r4 e t q deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 2 + 2 * e ->
  Gc (repeat U0 (S (length deep)), P0, 0) (q :: deep) (evR [t] Rs_r4) -->+
  Gc (repeat U0 (S (S (length deep))), P0, 0) ([W5t (1 + 9 * t); W5s (1 + 9 * t); W5a (1 + 9 * t); nth 0 q 0%N] :: rshift (q :: deep) 0%N) (evR [(1 + 9 * t)%N] Rs_r5).
Proof.
  intros He Ht Hl.
  eapply evstep_progress_trans; [apply interval_tm; [lia | reflexivity |]|].
  - intros T ET. pose proof (prog_check_spec _ _ _ _ _ int_r4 [t]) as HP.
    assert (E3 : 3 ^ S (S (S (length deep))) = 243 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (S (2 + 2 * e)))) with (5 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    assert (E2 : 3 ^ S (S (length deep)) = 81 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (2 + 2 * e))) with (4 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    rewrite E3 in ET. rewrite E2.
    replace T with (ev [t] (tl1 9839 78732)) by (unfold ev, tl1; cbn [lc lv dot]; lia).
    replace (81 * (81 * 81 * (1 + 8 * N.to_nat t)) - 1 - ev [t] (tl1 9839 78732)) with (ev [t] (tl1 521601 4172796))
      by (unfold ev, tl1; cbn [lc lv dot]; lia).
    exact HP.
  - eapply progress_trans; [apply record_visit; reflexivity|].
    apply step_r4.
Qed.