CoreAdministrativeCommutation.v

From Stdlib Require Import FunctionalExtensionality Lia PeanoNat
  Relations.Relation_Operators.
Require Import AdministrativeReduction.
Require Import AdministrativeAlgebra.
Require Import AdministrativeResiduals.
Require Import FrameCompatibility.
Require Import SharedPrompts.CoreParallel.
Require Import SharedPrompts.CoreParallelCompatibility.
Require Import SharedPrompts.ScopedAlgebra.
Require Import SharedPrompts.SubstitutionMaps.
Require Import SharedPrompts.CoreAlgebra.
Require Import SharedPrompts.ScopedFusion.
Require Import SharedPrompts.MapComposition.

Import SharedPrompts.
Import SharedPrompts.ContinuationMaps.

(** TODO after commutation: eliminate functional extensionality, add the
    sequential/parallel core bridges, define the final union [estep], and
    finish cosmetic API consolidation. *)

Lemma admin_ksubst_star_sequence e e' :
  star admin_step e e' -> forall cut k,
  star admin_step
    (ksubst_e cut (ICont k CHole) e)
    (ksubst_e cut (ICont k CHole) e').
Proof.
  intro H. induction H as [x|x y z Hxy Hyz IH]; intros cut k.
  - apply star_refl.
  - eapply star_trans.
    + exact (proj2 admin_ksubst_star x y Hxy cut k).
    + exact (IH cut k).
Qed.

Lemma admin_olift_value_star v v' :
  star admin_vstep v v' -> forall cut,
  star admin_vstep (olift_v cut 1 v) (olift_v cut 1 v').
Proof.
  intro H. induction H as [x | x y z Hxy Hyz IH]; intro cut.
  - apply star_refl.
  - eapply star_step.
    + exact (proj1 admin_olift_step x y Hxy cut).
    + exact (IH cut).
Qed.

Lemma admin_klift_value_star v v' :
  star admin_vstep v v' -> forall cut,
  star admin_vstep (klift_v cut 1 v) (klift_v cut 1 v').
Proof.
  intro H. induction H as [x | x y z Hxy Hyz IH]; intro cut.
  - apply star_refl.
  - eapply star_step.
    + exact (proj1 admin_klift_step x y Hxy cut).
    + exact (IH cut).
Qed.

(** Changing the value installed for one ordinary variable transports an
    administrative sequence.  Multiple occurrences account for the star. *)
Lemma admin_substitution_value_star :
  (forall x cut v v', star admin_vstep v v' ->
    star admin_vstep
      (osubst_v cut v x) (osubst_v cut v' x)) /\
  (forall e cut v v', star admin_vstep v v' ->
    star admin_step
      (osubst_e cut v e) (osubst_e cut v' e)).
Proof.
  apply (syntax_ind
    (fun x => forall cut v v', star admin_vstep v v' ->
      star admin_vstep (osubst_v cut v x) (osubst_v cut v' x))
    (fun e => forall cut v v', star admin_vstep v v' ->
      star admin_step (osubst_e cut v e) (osubst_e cut v' e))).
  - intros n cut v v' Hv. simpl. destruct (remove_index cut n).
    + apply star_refl.
    + exact Hv.
  - intros e IH cut v v' Hv. simpl.
    apply (admin_star_map admin_step admin_vstep VLam).
    + intros x y Hxy. apply AVS_Lam. exact Hxy.
    + apply IH. exact (admin_olift_value_star v v' Hv 0).
  - intros v0 IH cut v v' Hv. simpl.
    apply (admin_star_map admin_vstep admin_step EVal).
    + intros x y Hxy. apply AS_Val. exact Hxy.
    + apply IH. exact Hv.
  - intros v0 IHv u IHu cut v v' Hv. simpl.
    eapply star_trans.
    + apply (admin_star_map admin_vstep admin_step
        (fun x => EApp x (osubst_v cut v u))).
      * intros x y Hxy. apply AS_AppL. exact Hxy.
      * apply IHv. exact Hv.
    + apply (admin_star_map admin_vstep admin_step
        (fun x => EApp (osubst_v cut v' v0) x)).
      * intros x y Hxy. apply AS_AppR. exact Hxy.
      * apply IHu. exact Hv.
  - intros a IHa t IHt cut v v' Hv. simpl.
    eapply star_trans.
    + apply (admin_star_map admin_step admin_step
        (fun x => ELet x (osubst_e (S cut) (olift_v 0 1 v) t))).
      * intros x y Hxy. apply AS_LetBinding. exact Hxy.
      * apply IHa. exact Hv.
    + apply (admin_star_map admin_step admin_step
        (fun x => ELet (osubst_e cut v' a) x)).
      * intros x y Hxy. apply AS_LetBody. exact Hxy.
      * apply IHt. exact (admin_olift_value_star v v' Hv 0).
  - intros e IH cut v v' Hv. simpl.
    apply (admin_star_map admin_step admin_step EShift).
    + intros x y Hxy. apply AS_ShiftBody. exact Hxy.
    + apply IH. exact (admin_klift_value_star v v' Hv 0).
  - intros k e IH cut v v' Hv. simpl.
    apply (admin_star_map admin_step admin_step (ECont k)).
    + intros x y Hxy. apply AS_ContBody. exact Hxy.
    + apply IH. exact Hv.
  - intros k cut v v' Hv. apply star_refl.
Qed.

Corollary admin_subst0_value_star v v' e :
  star admin_vstep v v' ->
  star admin_step
    (subst_e (subst0 v) e) (subst_e (subst0 v') e).
Proof.
  intro H. unfold subst0. rewrite !subst_single_e.
  exact (proj2 admin_substitution_value_star e 0 v v' H).
Qed.

Lemma cocc_osubst_preserved :
  (forall x k cut v, cocc_v k x = true ->
    cocc_v k (osubst_v cut v x) = true) /\
  (forall e k cut v, cocc_e k e = true ->
    cocc_e k (osubst_e cut v e) = true).
Proof.
  apply (syntax_ind
    (fun x => forall k cut v, cocc_v k x = true ->
      cocc_v k (osubst_v cut v x) = true)
    (fun e => forall k cut v, cocc_e k e = true ->
      cocc_e k (osubst_e cut v e) = true)).
  - intros n k cut v H. discriminate.
  - intros e IH k cut v H. simpl in *. apply IH. exact H.
  - intros x IH k cut v H. simpl in *. apply IH. exact H.
  - intros x IHx y IHy k cut v H. simpl in *.
    apply Bool.orb_true_iff in H. apply Bool.orb_true_iff.
    destruct H as [H | H]; [left; apply IHx | right; apply IHy]; exact H.
  - intros a IHa t IHt k cut v H. simpl in *.
    apply Bool.orb_true_iff in H. apply Bool.orb_true_iff.
    destruct H as [H | H].
    + left. apply IHa. exact H.
    + right. apply IHt. exact H.
  - intros e IH k cut v H. simpl in *. apply IH. exact H.
  - intros j e IH k cut v H. simpl in *.
    apply Bool.orb_true_iff in H. apply Bool.orb_true_iff.
    destruct H as [H | H]; [left | right; apply IH]; exact H.
  - intros j k cut v H. exact H.
Qed.

Lemma osubst_abort cut v e :
  osubst_e cut v (abort e) = abort (osubst_e cut v e).
Proof.
  unfold abort. simpl. f_equal.
  symmetry. apply klift_osubst_e.
Qed.

Lemma tail_step_osubst k e e' :
  tail_step k e e' -> forall cut v,
  tail_step k (osubst_e cut v e) (osubst_e cut v e').
Proof.
  intro H. induction H as [k a t t' Htail IH | k e Hocc | k e];
    intros cut v.
  - simpl. apply TS_LetBody. apply IH.
  - rewrite osubst_abort, fs_osubst_ksubst_hole_e_upk.
    simpl.
    apply TS_Shift. apply (proj2 cocc_osubst_preserved).
    exact Hocc.
  - rewrite osubst_abort. simpl. apply TS_Abort.
Qed.

Lemma admin_osubst_step_from_roots
    (Hlet_shift : forall e t cut v,
      admin_step
        (osubst_e cut v (ELet (EShift e) t))
        (osubst_e cut v (EShift (krepl_e 0 (frame t) e))))
    (Hlet_assoc : forall a u t cut v,
      admin_step
        (osubst_e cut v (ELet (ELet a u) t))
        (osubst_e cut v
          (ELet a (ELet u (olift_e 1 1 t))))) :
  (forall x x', admin_vstep x x' -> forall cut v,
    admin_vstep (osubst_v cut v x) (osubst_v cut v x')) /\
  (forall e e', admin_step e e' -> forall cut v,
    admin_step (osubst_e cut v e) (osubst_e cut v e')).
Proof.
  apply admin_mutind.
  - intros e e' H IH cut v. simpl. apply AVS_Lam. apply IH.
  - intros x x' H IH cut v. simpl. apply AS_Val. apply IH.
  - intros x x' y H IH cut v. simpl. apply AS_AppL. apply IH.
  - intros x y y' H IH cut v. simpl. apply AS_AppR. apply IH.
  - intros a a' t H IH cut v. simpl. apply AS_LetBinding. apply IH.
  - intros a t t' H IH cut v. simpl. apply AS_LetBody. apply IH.
  - intros e e' H IH cut v. simpl. apply AS_ShiftBody. apply IH.
  - intros k e e' H IH cut v. simpl. apply AS_ContBody. apply IH.
  - intros k e e' Htail cut v. simpl. apply AS_ContTail.
    apply tail_step_osubst. exact Htail.
  - exact Hlet_shift.
  - exact Hlet_assoc.
Qed.

Lemma admin_osubst_star_from_roots
    (Hlet_shift : forall e t cut v,
      admin_step
        (osubst_e cut v (ELet (EShift e) t))
        (osubst_e cut v (EShift (krepl_e 0 (frame t) e))))
    (Hlet_assoc : forall a u t cut v,
      admin_step
        (osubst_e cut v (ELet (ELet a u) t))
        (osubst_e cut v
          (ELet a (ELet u (olift_e 1 1 t)))))
    e e' :
  star admin_step e e' -> forall cut v,
  star admin_step (osubst_e cut v e) (osubst_e cut v e').
Proof.
  intro H. induction H as [x | x y z Hxy Hyz IH]; intros cut v.
  - apply star_refl.
  - eapply star_step.
    + exact (proj2
        (admin_osubst_step_from_roots Hlet_shift Hlet_assoc)
        x y Hxy cut v).
    + exact (IH cut v).
Qed.

Lemma osubst_olift_one_below cut v e :
  osubst_e (S (S cut)) (olift_v 0 1 (olift_v 0 1 v))
    (olift_e 1 1 e) =
  olift_e 1 1 (osubst_e (S cut) (olift_v 0 1 v) e).
Proof.
  pose proof (omap_olift_depth_e 1 (osub_map cut v) e) as H.
  cbn [omap_up_n] in H.
  rewrite (osub_map_lam_eq cut v) in H.
  rewrite (osub_map_lam_eq (S cut) (olift_v 0 1 v)) in H.
  rewrite !omap_single_e in H. exact H.
Qed.

Fixpoint osubst_ectx (cut : nat) (v : value) (c : ectx) : ectx :=
  match c with
  | CHole => CHole
  | CLet c t =>
      CLet (osubst_ectx cut v c)
        (osubst_e (S cut) (olift_v 0 1 v) t)
  end.

Definition osubst_installed (cut : nat) (v : value)
    (d : installed) : installed :=
  match d with
  | ICont k c => ICont k (osubst_ectx cut v c)
  end.

Lemma osubst_plug_ectx cut v c q :
  osubst_e cut v (plug c q) =
  plug (osubst_ectx cut v c) (osubst_e cut v q).
Proof.
  induction c as [|c IH t]; simpl; [reflexivity |].
  rewrite IH. reflexivity.
Qed.

Lemma osubst_plug_installed cut v d q :
  osubst_e cut v (plug_d d q) =
  plug_d (osubst_installed cut v d) (osubst_e cut v q).
Proof.
  destruct d as [k c]. simpl. f_equal. apply osubst_plug_ectx.
Qed.

Lemma osubst_ectx_olift cut v c :
  osubst_ectx (S cut) (olift_v 0 1 v) (olift_c 0 1 c) =
  olift_c 0 1 (osubst_ectx cut v c).
Proof.
  induction c as [|c IH t]; simpl.
  - reflexivity.
  - f_equal.
    + exact IH.
    + apply osubst_olift_one_below.
Qed.

Lemma osubst_installed_olift cut v d :
  osubst_installed (S cut) (olift_v 0 1 v) (olift_d 0 1 d) =
  olift_d 0 1 (osubst_installed cut v d).
Proof.
  destruct d as [k c]. simpl. f_equal. apply osubst_ectx_olift.
Qed.

Lemma osubst_ectx_klift cut v c :
  osubst_ectx cut (klift_v 0 1 v) (klift_c 0 1 c) =
  klift_c 0 1 (osubst_ectx cut v c).
Proof.
  induction c as [|c IH t]; simpl.
  - reflexivity.
  - f_equal; [exact IH |].
    rewrite <- klift_olift_v_comm.
    symmetry. apply klift_osubst_e.
Qed.

Lemma osubst_installed_klift cut v d :
  osubst_installed cut (klift_v 0 1 v) (klift_d 0 1 d) =
  klift_d 0 1 (osubst_installed cut v d).
Proof.
  destruct d as [k c]. simpl. f_equal. apply osubst_ectx_klift.
Qed.

Lemma osubst_krepl :
  (forall x kc d cut v,
    cocc_v kc v = false ->
    osubst_v cut v (krepl_v kc d x) =
    krepl_v kc (osubst_installed cut v d) (osubst_v cut v x)) /\
  (forall e kc d cut v,
    cocc_v kc v = false ->
    osubst_e cut v (krepl_e kc d e) =
    krepl_e kc (osubst_installed cut v d) (osubst_e cut v e)).
Proof.
  apply (syntax_ind
    (fun x => forall kc d cut v,
      cocc_v kc v = false ->
      osubst_v cut v (krepl_v kc d x) =
      krepl_v kc (osubst_installed cut v d) (osubst_v cut v x))
    (fun e => forall kc d cut v,
      cocc_v kc v = false ->
      osubst_e cut v (krepl_e kc d e) =
      krepl_e kc (osubst_installed cut v d) (osubst_e cut v e))).
  - intros n kc d cut v Hfresh. simpl.
    destruct (remove_index cut n) as [n' |] eqn:Hremove; simpl.
    + reflexivity.
    + symmetry. apply (proj1 admin_krepl_no_cocc). exact Hfresh.
  - intros e IH kc d cut v Hfresh. simpl. f_equal.
    rewrite IH, osubst_installed_olift; [reflexivity |].
    rewrite (proj1 admin_cocc_olift). exact Hfresh.
  - intros x IH kc d cut v Hfresh. simpl. f_equal. apply IH. exact Hfresh.
  - intros x IHx y IHy kc d cut v Hfresh. simpl. f_equal.
    + apply IHx. exact Hfresh.
    + apply IHy. exact Hfresh.
  - intros a IHa t IHt kc d cut v Hfresh. simpl. f_equal.
    + apply IHa. exact Hfresh.
    + rewrite IHt, osubst_installed_olift; [reflexivity |].
      rewrite (proj1 admin_cocc_olift). exact Hfresh.
  - intros e IH kc d cut v Hfresh. simpl. f_equal.
    rewrite IH, osubst_installed_klift; [reflexivity |].
    rewrite cocc_klift_zero_succ_v. exact Hfresh.
  - intros k e IH kc d cut v Hfresh. simpl.
    destruct (Nat.eqb k kc); simpl.
    + rewrite osubst_plug_installed, IH; [reflexivity | exact Hfresh].
    + f_equal. apply IH. exact Hfresh.
  - intros k kc d cut v Hfresh. simpl. destruct (Nat.eqb k kc).
    + destruct d. reflexivity.
    + reflexivity.
Qed.

Lemma osubst_installed_frame cut v t :
  osubst_installed cut (klift_v 0 1 v) (frame t) =
  frame (osubst_e (S cut) (olift_v 0 1 v) t).
Proof.
  unfold frame, osubst_installed. simpl. f_equal. f_equal.
  symmetry. rewrite <- klift_olift_v_comm. apply klift_osubst_e.
Qed.

Lemma admin_osubst_let_assoc_root a u t cut v :
  admin_step
    (osubst_e cut v (ELet (ELet a u) t))
    (osubst_e cut v (ELet a (ELet u (olift_e 1 1 t)))).
Proof.
  simpl.
  rewrite osubst_olift_one_below.
  apply AS_LetAssoc.
Qed.

Lemma admin_osubst_let_shift_root e t cut v :
  admin_step
    (osubst_e cut v (ELet (EShift e) t))
    (osubst_e cut v (EShift (krepl_e 0 (frame t) e))).
Proof.
  simpl.
  rewrite (proj2 osubst_krepl e 0 (frame t) cut
    (klift_v 0 1 v) (cocc_klift_fresh_v 0 v)).
  rewrite osubst_installed_frame.
  apply AS_LetShift.
Qed.

Corollary admin_osubst_star e e' :
  star admin_step e e' -> forall cut v,
  star admin_step (osubst_e cut v e) (osubst_e cut v e').
Proof.
  apply admin_osubst_star_from_roots.
  - exact admin_osubst_let_shift_root.
  - exact admin_osubst_let_assoc_root.
Qed.

Corollary admin_subst0_expr_star v e e' :
  star admin_step e e' ->
  star admin_step
    (subst_e (subst0 v) e) (subst_e (subst0 v) e').
Proof.
  intro H. unfold subst0. rewrite !subst_single_e.
  exact (admin_osubst_star e e' H 0 v).
Qed.

Lemma subst0_let_lift_cancel (v : value) (u t : expr) :
  subst_e (subst0 v) (ELet u (olift_e 1 1 t)) =
  ELet (subst_e (subst0 v) u) t.
Proof.
  unfold subst0.
  rewrite !subst_single_e.
  simpl. rewrite osubst_olift_cancel_e. reflexivity.
Qed.

Lemma core_parallel_let_assoc_residual
    (delta : payload_env) (a u b t t' : expr) :
  core_parallel delta (ELet a u) b ->
  core_parallel (payload_env_olift delta) t t' ->
  exists z,
    star admin_step (ELet b t') z /\
    core_parallel delta
      (ELet a (ELet u (olift_e 1 1 t))) z.
Proof.
  intros Hbinding Htail. inversion Hbinding; subst.
  - exists (ELet a' (ELet t'0 (olift_e 1 1 t'))); split.
    + apply star_one. apply AS_LetAssoc.
    + apply CP_Let; [assumption |].
      apply CP_Let; [assumption |].
      pose proof (core_parallel_olift_expr_at Htail 1) as Hlift.
      change (core_parallel
        (payload_env_olift_at (S 0) (payload_env_olift delta))
        (olift_e 1 1 t) (olift_e 1 1 t')) in Hlift.
      rewrite (payload_env_olift_at_payload_env_olift 0 delta) in Hlift.
      exact Hlift.
  - exists (ELet (subst_e (subst0 v') t'0) t'); split.
    + apply star_refl.
    + replace (ELet (subst_e (subst0 v') t'0) t') with
        (subst_e (subst0 v') (ELet t'0 (olift_e 1 1 t'))).
      * apply CP_LetValue; [assumption |].
        apply CP_Let; [assumption |].
        pose proof (core_parallel_olift_expr_at Htail 1) as Hlift.
        change (core_parallel
          (payload_env_olift_at (S 0) (payload_env_olift delta))
          (olift_e 1 1 t) (olift_e 1 1 t')) in Hlift.
        rewrite (payload_env_olift_at_payload_env_olift 0 delta) in Hlift.
        exact Hlift.
      * apply subst0_let_lift_cancel.
Qed.

(** The outer-constructor induction.  This deliberately exposes only the
    substitution and root/tail residuals; no datatype of reduction positions
    is introduced. *)
Lemma core_admin_commute_from_residuals
    (Hsubst_expr : forall v e e',
      star admin_step e e' ->
      star admin_step
        (subst_e (subst0 v) e) (subst_e (subst0 v) e'))
    (Hsubst_value : forall v v' e,
      star admin_vstep v v' ->
      star admin_step
        (subst_e (subst0 v) e) (subst_e (subst0 v') e))
    (Hlet_shift : forall delta e e' t t',
      core_parallel delta (EShift e) (EShift e') ->
      core_parallel (payload_env_olift delta) t t' ->
      exists u,
        star admin_step (ELet (EShift e') t') u /\
        core_parallel delta
          (EShift (krepl_e 0 (frame t) e)) u)
    (Hlet_assoc : forall delta a u b t t',
      core_parallel delta (ELet a u) b ->
      core_parallel (payload_env_olift delta) t t' ->
      exists z,
        star admin_step (ELet b t') z /\
        core_parallel delta
          (ELet a (ELet u (olift_e 1 1 t))) z)
    (Hcont_tail : forall delta k e e' a,
      core_parallel delta e e' ->
      tail_step k e a ->
      exists u,
        star admin_step (ECont k e') u /\
        core_parallel delta (ECont k a) u)
    (Hcont_shift_tail : forall delta k e e' a,
      core_parallel (payload_env_klift delta) e e' ->
      tail_step k (EShift e) a ->
      exists u,
        star admin_step (ksubst_e 0 (ICont k CHole) e') u /\
        core_parallel delta (ECont k a) u) :
  forall delta,
  (forall v c,
      core_value_parallel delta v c ->
      forall a, admin_vstep v a ->
      exists u, star admin_vstep c u /\ core_value_parallel delta a u) /\
  (forall e c,
      core_parallel delta e c ->
      forall a, admin_step e a ->
      exists u, star admin_step c u /\ core_parallel delta a u).
Proof.
  apply (core_parallel_mutind
    (fun delta v c _ => forall a, admin_vstep v a ->
      exists u, star admin_vstep c u /\ core_value_parallel delta a u)
    (fun delta e c _ => forall a, admin_step e a ->
      exists u, star admin_step c u /\ core_parallel delta a u)).
  - intros delta n a Ha. inversion Ha.
  - intros delta e e' Hp IH a Ha. inversion Ha; subst.
    match goal with
    | H : admin_step e _ |- _ =>
        destruct (IH _ H) as [u [Heu Hcore]]
    end.
    exists (VLam u); split.
    + apply (admin_star_map admin_step admin_vstep VLam); [|exact Heu].
      intros x y Hxy. apply AVS_Lam. exact Hxy.
    + apply CP_VLam. exact Hcore.
  - intros delta v v' Hp IH a Ha. inversion Ha; subst.
    match goal with
    | H : admin_vstep v _ |- _ =>
        destruct (IH _ H) as [u [Hvu Hcore]]
    end.
    exists (EVal u); split.
    + apply (admin_star_map admin_vstep admin_step EVal); [|exact Hvu].
      intros x y Hxy. apply AS_Val. exact Hxy.
    + apply CP_Val. exact Hcore.
  - intros delta v v' u u' Hv IHv Hu IHu a Ha.
    inversion Ha; subst.
    + match goal with
      | H : admin_vstep v _ |- _ =>
          destruct (IHv _ H) as [w [Hvw Hcore]]
      end.
      exists (EApp w u'); split.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp x u')); [|exact Hvw].
        intros x y Hxy. apply AS_AppL. exact Hxy.
      * apply CP_App; [exact Hcore | exact Hu].
    + match goal with
      | H : admin_vstep u _ |- _ =>
          destruct (IHu _ H) as [w [Huw Hcore]]
      end.
      exists (EApp v' w); split.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp v' x)); [|exact Huw].
        intros x y Hxy. apply AS_AppR. exact Hxy.
      * apply CP_App; [exact Hv | exact Hcore].
  - intros delta a a' t t' Ha IHa Ht IHt z Hz.
    inversion Hz; subst.
    + match goal with
      | H : admin_step a _ |- _ =>
          destruct (IHa _ H) as [b [Hab Hcore]]
      end.
      exists (ELet b t'); split.
      * apply (admin_star_map admin_step admin_step
          (fun x => ELet x t')); [|exact Hab].
        intros x y Hxy. apply AS_LetBinding. exact Hxy.
      * apply CP_Let; [exact Hcore | exact Ht].
    + match goal with
      | H : admin_step t _ |- _ =>
          destruct (IHt _ H) as [q [Htq Hcore]]
      end.
      exists (ELet a' q); split.
      * apply (admin_star_map admin_step admin_step
          (fun x => ELet a' x)); [|exact Htq].
        intros x y Hxy. apply AS_LetBody. exact Hxy.
      * apply CP_Let; [exact Ha | exact Hcore].
    + inversion Ha; subst. eapply Hlet_shift; eassumption.
    + eapply Hlet_assoc; eassumption.
  - intros delta e e' Hp IH a Ha. inversion Ha; subst.
    match goal with
    | H : admin_step e _ |- _ =>
        destruct (IH _ H) as [u [Heu Hcore]]
    end.
    exists (EShift u); split.
    + apply (admin_star_map admin_step admin_step EShift); [|exact Heu].
      intros x y Hxy. apply AS_ShiftBody. exact Hxy.
    + apply CP_Shift. exact Hcore.
  - intros delta k e e' Hp IH a Ha. inversion Ha; subst.
    + match goal with
      | H : admin_step e _ |- _ =>
          destruct (IH _ H) as [u [Heu Hcore]]
      end.
      exists (ECont k u); split.
      * apply (admin_star_map admin_step admin_step (ECont k)); [|exact Heu].
        intros x y Hxy. apply AS_ContBody. exact Hxy.
      * apply CP_Cont. exact Hcore.
    + eapply Hcont_tail; eassumption.
  - intros delta k a Ha. inversion Ha.
  - intros delta k v Hlookup a Ha. inversion Ha.
  - intros delta e e' v v' He IHe Hv IHv a Ha.
    inversion Ha; subst.
    + match goal with
      | Hlam : admin_vstep (VLam e) _ |- _ => inversion Hlam; subst
      end.
      match goal with
      | H : admin_step e _ |- _ =>
          destruct (IHe _ H) as [b [Heb Hcore]]
      end.
      exists (subst_e (subst0 v') b); split.
      * apply Hsubst_expr. exact Heb.
      * apply CP_Beta; [exact Hcore | exact Hv].
    + match goal with
      | H : admin_vstep v _ |- _ =>
          destruct (IHv _ H) as [w [Hvw Hcore]]
      end.
      exists (subst_e (subst0 w) e'); split.
      * apply Hsubst_value. exact Hvw.
      * apply CP_Beta; [exact He | exact Hcore].
  - intros delta v v' t t' Hv IHv Ht IHt a Ha.
    inversion Ha; subst.
    + match goal with
      | Hval : admin_step (EVal v) _ |- _ => inversion Hval; subst
      end.
      match goal with
      | H : admin_vstep v _ |- _ =>
          destruct (IHv _ H) as [w [Hvw Hcore]]
      end.
      exists (subst_e (subst0 w) t'); split.
      * apply Hsubst_value. exact Hvw.
      * apply CP_LetValue; [exact Hcore | exact Ht].
    + match goal with
      | H : admin_step t _ |- _ =>
          destruct (IHt _ H) as [q [Htq Hcore]]
      end.
      exists (subst_e (subst0 v') q); split.
      * apply Hsubst_expr. exact Htq.
      * apply CP_LetValue; [exact Hv | exact Hcore].
  - intros delta k e e' Hp IH a Ha.
    inversion Ha; subst.
    + match goal with
      | Hshift : admin_step (EShift e) _ |- _ =>
          inversion Hshift; subst
      end.
      match goal with
      | H : admin_step e _ |- _ =>
          destruct (IH _ H) as [u [Heu Hcore]]
      end.
      exists (ksubst_e 0 (ICont k CHole) u); split.
      * exact (admin_ksubst_star_sequence e' u Heu 0 k).
      * apply CP_ContShift. exact Hcore.
    + eapply Hcont_shift_tail; eassumption.
Qed.

(** --------------------------------------------------------------------
    Decreasing mixed pentagons, with [let.S] kept out of core parallelism.

    Compared with strong commutation, the administrative reduct is allowed
    to perform an administrative prefix before the residual parallel step:

                         x
                      P / \ A
                       p   a
                       |   |
                      A*   A*
                       |   |
                       b <-P- r

    This is the mixed diagram required by the source-labelled decreasing-
    diagrams argument. *)

Lemma core_admin_decreasing_from_residuals
    (Hlet_shift : forall delta e p t t',
      core_parallel delta (EShift e) p ->
      core_parallel (payload_env_olift delta) t t' ->
      exists r b,
        star admin_step (ELet p t') b /\
        star admin_step
          (EShift (krepl_e 0 (frame t) e)) r /\
        core_parallel delta r b)
    (Hlet_assoc : forall delta a u p t t',
      core_parallel delta (ELet a u) p ->
      core_parallel (payload_env_olift delta) t t' ->
      exists r b,
        star admin_step (ELet p t') b /\
        star admin_step
          (ELet a (ELet u (olift_e 1 1 t))) r /\
        core_parallel delta r b)
    (Hcont_tail : forall delta k e p a,
      core_parallel delta e p ->
      tail_step k e a ->
      exists r b,
        star admin_step (ECont k p) b /\
        star admin_step (ECont k a) r /\
        core_parallel delta r b)
    (Hcont_shift_tail : forall delta k e p a,
      core_parallel (payload_env_klift delta) e p ->
      tail_step k (EShift e) a ->
      exists r b,
        star admin_step
          (ksubst_e 0 (ICont k CHole) p) b /\
        star admin_step (ECont k a) r /\
        core_parallel delta r b) :
  forall delta,
  (forall v p,
      core_value_parallel delta v p ->
      forall a, admin_vstep v a ->
      exists r b,
        star admin_vstep p b /\
        star admin_vstep a r /\
        core_value_parallel delta r b) /\
  (forall e p,
      core_parallel delta e p ->
      forall a, admin_step e a ->
      exists r b,
        star admin_step p b /\
        star admin_step a r /\
        core_parallel delta r b).
Proof.
  apply (core_parallel_mutind
    (fun delta v p _ => forall a, admin_vstep v a ->
      exists r b,
        star admin_vstep p b /\
        star admin_vstep a r /\
        core_value_parallel delta r b)
    (fun delta e p _ => forall a, admin_step e a ->
      exists r b,
        star admin_step p b /\
        star admin_step a r /\
        core_parallel delta r b)).
  - intros delta n a Ha. inversion Ha.
  - intros delta e e' Hp IH a Ha. inversion Ha; subst.
    match goal with
    | H : admin_step e _ |- _ =>
        destruct (IH _ H) as [r [b [Heb [Har Hcore]]]]
    end.
    exists (VLam r), (VLam b); split; [|split].
    + apply (admin_star_map admin_step admin_vstep VLam); [|exact Heb].
      intros x y Hxy. apply AVS_Lam. exact Hxy.
    + apply (admin_star_map admin_step admin_vstep VLam); [|exact Har].
      intros x y Hxy. apply AVS_Lam. exact Hxy.
    + apply CP_VLam. exact Hcore.
  - intros delta v v' Hp IH a Ha. inversion Ha; subst.
    match goal with
    | H : admin_vstep v _ |- _ =>
        destruct (IH _ H) as [r [b [Hvb [Har Hcore]]]]
    end.
    exists (EVal r), (EVal b); split; [|split].
    + apply (admin_star_map admin_vstep admin_step EVal); [|exact Hvb].
      intros x y Hxy. apply AS_Val. exact Hxy.
    + apply (admin_star_map admin_vstep admin_step EVal); [|exact Har].
      intros x y Hxy. apply AS_Val. exact Hxy.
    + apply CP_Val. exact Hcore.
  - intros delta v v' u u' Hv IHv Hu IHu a Ha.
    inversion Ha; subst.
    + match goal with
      | H : admin_vstep v _ |- _ =>
          destruct (IHv _ H) as [r [b [Hvb [Har Hcore]]]]
      end.
      exists (EApp r u), (EApp b u'); split; [|split].
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp x u')); [|exact Hvb].
        intros x y Hxy. apply AS_AppL. exact Hxy.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp x u)); [|exact Har].
        intros x y Hxy. apply AS_AppL. exact Hxy.
      * apply CP_App; [exact Hcore | exact Hu].
    + match goal with
      | H : admin_vstep u _ |- _ =>
          destruct (IHu _ H) as [r [b [Hub [Har Hcore]]]]
      end.
      exists (EApp v r), (EApp v' b); split; [|split].
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp v' x)); [|exact Hub].
        intros x y Hxy. apply AS_AppR. exact Hxy.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp v x)); [|exact Har].
        intros x y Hxy. apply AS_AppR. exact Hxy.
      * apply CP_App; [exact Hv | exact Hcore].
  - intros delta e e' t t' He IHe Ht IHt z Hz.
    inversion Hz; subst.
    + match goal with
      | H : admin_step e _ |- _ =>
          destruct (IHe _ H) as [r [b [Heb [Har Hcore]]]]
      end.
      exists (ELet r t), (ELet b t'); split; [|split].
      * apply (admin_star_map admin_step admin_step
          (fun x => ELet x t')); [|exact Heb].
        intros x y Hxy. apply AS_LetBinding. exact Hxy.
      * apply (admin_star_map admin_step admin_step
          (fun x => ELet x t)); [|exact Har].
        intros x y Hxy. apply AS_LetBinding. exact Hxy.
      * apply CP_Let; [exact Hcore | exact Ht].
    + match goal with
      | H : admin_step t _ |- _ =>
          destruct (IHt _ H) as [r [b [Htb [Har Hcore]]]]
      end.
      exists (ELet e r), (ELet e' b); split; [|split].
      * apply (admin_star_map admin_step admin_step
          (fun x => ELet e' x)); [|exact Htb].
        intros x y Hxy. apply AS_LetBody. exact Hxy.
      * apply (admin_star_map admin_step admin_step
          (fun x => ELet e x)); [|exact Har].
        intros x y Hxy. apply AS_LetBody. exact Hxy.
      * apply CP_Let; [exact He | exact Hcore].
    + eapply Hlet_shift; eassumption.
    + eapply Hlet_assoc; eassumption.
  - intros delta e e' Hp IH a Ha. inversion Ha; subst.
    match goal with
    | H : admin_step e _ |- _ =>
        destruct (IH _ H) as [r [b [Heb [Har Hcore]]]]
    end.
    exists (EShift r), (EShift b); split; [|split].
    + apply (admin_star_map admin_step admin_step EShift); [|exact Heb].
      intros x y Hxy. apply AS_ShiftBody. exact Hxy.
    + apply (admin_star_map admin_step admin_step EShift); [|exact Har].
      intros x y Hxy. apply AS_ShiftBody. exact Hxy.
    + apply CP_Shift. exact Hcore.
  - intros delta k e e' Hp IH a Ha. inversion Ha; subst.
    + match goal with
      | H : admin_step e _ |- _ =>
          destruct (IH _ H) as [r [b [Heb [Har Hcore]]]]
      end.
      exists (ECont k r), (ECont k b); split; [|split].
      * apply (admin_star_map admin_step admin_step (ECont k)); [|exact Heb].
        intros x y Hxy. apply AS_ContBody. exact Hxy.
      * apply (admin_star_map admin_step admin_step (ECont k)); [|exact Har].
        intros x y Hxy. apply AS_ContBody. exact Hxy.
      * apply CP_Cont. exact Hcore.
    + eapply Hcont_tail; eassumption.
  - intros delta k a Ha. inversion Ha.
  - intros delta k v Hlookup a Ha. inversion Ha.
  - intros delta e e' v v' He IHe Hv IHv a Ha.
    inversion Ha; subst.
    + match goal with
      | Hlam : admin_vstep (VLam e) _ |- _ => inversion Hlam; subst
      end.
      match goal with
      | H : admin_step e _ |- _ =>
          destruct (IHe _ H) as [r [b [Heb [Har Hcore]]]]
      end.
      exists (EApp (VLam r) v), (subst_e (subst0 v') b); split; [|split].
      * apply admin_subst0_expr_star. exact Heb.
      * apply (admin_star_map admin_step admin_step
          (fun x => EApp (VLam x) v)); [|exact Har].
        intros x y Hxy. apply AS_AppL. apply AVS_Lam. exact Hxy.
      * apply CP_Beta; [exact Hcore | exact Hv].
    + match goal with
      | H : admin_vstep v _ |- _ =>
          destruct (IHv _ H) as [r [b [Hvb [Har Hcore]]]]
      end.
      exists (EApp (VLam e) r), (subst_e (subst0 b) e'); split; [|split].
      * apply admin_subst0_value_star. exact Hvb.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp (VLam e) x)); [|exact Har].
        intros x y Hxy. apply AS_AppR. exact Hxy.
      * apply CP_Beta; [exact He | exact Hcore].
  - intros delta v v' t t' Hv IHv Ht IHt a Ha.
    inversion Ha; subst.
    + match goal with
      | Hval : admin_step (EVal v) _ |- _ => inversion Hval; subst
      end.
      match goal with
      | H : admin_vstep v _ |- _ =>
          destruct (IHv _ H) as [r [b [Hvb [Har Hcore]]]]
      end.
      exists (ELet (EVal r) t), (subst_e (subst0 b) t'); split; [|split].
      * apply admin_subst0_value_star. exact Hvb.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => ELet (EVal x) t)); [|exact Har].
        intros x y Hxy. apply AS_LetBinding. apply AS_Val. exact Hxy.
      * apply CP_LetValue; [exact Hcore | exact Ht].
    + match goal with
      | H : admin_step t _ |- _ =>
          destruct (IHt _ H) as [r [b [Htb [Har Hcore]]]]
      end.
      exists (ELet (EVal v) r), (subst_e (subst0 v') b); split; [|split].
      * apply admin_subst0_expr_star. exact Htb.
      * apply (admin_star_map admin_step admin_step
          (fun x => ELet (EVal v) x)); [|exact Har].
        intros x y Hxy. apply AS_LetBody. exact Hxy.
      * apply CP_LetValue; [exact Hv | exact Hcore].
  - intros delta k e e' Hp IH a Ha.
    inversion Ha; subst.
    + match goal with
      | Hshift : admin_step (EShift e) _ |- _ =>
          inversion Hshift; subst
      end.
      match goal with
      | H : admin_step e _ |- _ =>
          destruct (IH _ H) as [r [b [Heb [Har Hcore]]]]
      end.
      exists (ECont k (EShift r)),
        (ksubst_e 0 (ICont k CHole) b); split; [|split].
      * exact (admin_ksubst_star_sequence e' b Heb 0 k).
      * apply (admin_star_map admin_step admin_step
          (fun x => ECont k (EShift x))); [|exact Har].
        intros x y Hxy. apply AS_ContBody. apply AS_ShiftBody. exact Hxy.
      * apply CP_ContShift. exact Hcore.
    + eapply Hcont_shift_tail; eassumption.
Qed.

(** Let-association already satisfies the stronger square proved above, so
    its decreasing residual needs no new algebra. *)
Lemma core_parallel_let_assoc_decreasing_residual
    (delta : payload_env) (a u p t t' : expr) :
  core_parallel delta (ELet a u) p ->
  core_parallel (payload_env_olift delta) t t' ->
  exists r b,
    star admin_step (ELet p t') b /\
    star admin_step
      (ELet a (ELet u (olift_e 1 1 t))) r /\
    core_parallel delta r b.
Proof.
  intros Hp Ht.
  destruct (core_parallel_let_assoc_residual delta a u p t t' Hp Ht)
    as [b [Hpb Hcore]].
  exists (ELet a (ELet u (olift_e 1 1 t))), b.
  repeat split; try assumption. apply star_refl.
Qed.

(** Frame postponement is the one genuinely new algebraic lemma exposed by
    the decreasing presentation.  Administrative preprocessing may bubble
    core [k.S] redexes back out of installed let frames; the final parallel
    step also updates every duplicated copy of the frame payload. *)
Lemma osubst_olift_cancel_ectx (cut : nat) (v : value) (c : ectx) :
  osubst_ectx cut v (olift_c cut 1 c) = c.
Proof.
  induction c as [|c IH t]; simpl.
  - reflexivity.
  - rewrite IH, osubst_olift_cancel_e. reflexivity.
Qed.

Lemma osubst_olift_cancel_installed (cut : nat) (v : value)
    (d : installed) :
  osubst_installed cut v (olift_d cut 1 d) = d.
Proof.
  destruct d as [k c]. simpl. f_equal.
  apply osubst_olift_cancel_ectx.
Qed.

Lemma krepl_osubst_fusion :
  (forall x kc d cut v,
    krepl_v kc d (osubst_v cut v x) =
    osubst_v cut (krepl_v kc d v)
      (krepl_v kc (olift_d cut 1 d) x)) /\
  (forall e kc d cut v,
    krepl_e kc d (osubst_e cut v e) =
    osubst_e cut (krepl_v kc d v)
      (krepl_e kc (olift_d cut 1 d) e)).
Proof.
  apply (syntax_ind
    (fun x => forall kc d cut v,
      krepl_v kc d (osubst_v cut v x) =
      osubst_v cut (krepl_v kc d v)
        (krepl_v kc (olift_d cut 1 d) x))
    (fun e => forall kc d cut v,
      krepl_e kc d (osubst_e cut v e) =
      osubst_e cut (krepl_v kc d v)
        (krepl_e kc (olift_d cut 1 d) e))).
  - intros n kc d cut v. simpl.
    destruct (remove_index cut n); reflexivity.
  - intros e IH kc d cut v. simpl. f_equal.
    rewrite (IH kc (olift_d 0 1 d) (S cut) (olift_v 0 1 v)).
    rewrite (proj1 admin_olift_krepl v 0 1 kc d).
    rewrite admin_olift_d_comp. reflexivity.
  - intros v0 IH kc d cut v. simpl. f_equal. apply IH.
  - intros v0 IHv u IHu kc d cut v. simpl. f_equal;
      [apply IHv | apply IHu].
  - intros a IHa t IHt kc d cut v. simpl. f_equal.
    + apply IHa.
    + rewrite (IHt kc (olift_d 0 1 d) (S cut) (olift_v 0 1 v)).
      rewrite (proj1 admin_olift_krepl v 0 1 kc d).
      rewrite admin_olift_d_comp. reflexivity.
  - intros e IH kc d cut v. simpl. f_equal.
    rewrite (IH (S kc) (klift_d 0 1 d) cut (klift_v 0 1 v)).
    rewrite (admin_klift_krepl_v 0 kc d v).
    rewrite admin_klift_olift_d_general. reflexivity.
  - intros k e IH kc d cut v. simpl.
    destruct (Nat.eqb k kc); simpl.
    + rewrite osubst_plug_installed, IH.
      rewrite osubst_olift_cancel_installed. reflexivity.
    + rewrite IH. reflexivity.
  - intros k kc d cut v. simpl.
    destruct (Nat.eqb k kc); [destruct d |]; reflexivity.
Qed.

(** Pointwise ordinary lifting of every installed continuation in a map.
    Unlike continuation lifting, ordinary lifting does not reindex the map's
    domain, so its naturality law is genuinely pointwise. *)
Definition cmap_olift_at_action (cut amount : nat) (rho : cmap) : cmap :=
  fun k => olift_d cut amount (rho k).

Lemma cmap_olift_at_action_binder cut amount rho :
  cmap_olift_at_action (S cut) amount (cmap_olift rho) =
  cmap_olift (cmap_olift_at_action cut amount rho).
Proof.
  apply functional_extensionality. intro k.
  unfold cmap_olift_at_action, cmap_olift.
  apply admin_olift_d_comp.
Qed.

Lemma cmap_olift_at_action_shift cut amount rho :
  cmap_olift_at_action cut amount (cmap_up rho) =
  cmap_up (cmap_olift_at_action cut amount rho).
Proof.
  apply functional_extensionality. intros [|k].
  - reflexivity.
  - unfold cmap_olift_at_action, cmap_up.
    symmetry. apply admin_klift_olift_d_general.
Qed.

Lemma cmap_action_olift_v :
  (forall v rho cut amount,
    olift_v cut amount (cmap_v rho v) =
    cmap_v (cmap_olift_at_action cut amount rho)
      (olift_v cut amount v)) /\
  (forall e rho cut amount,
    olift_e cut amount (cmap_e rho e) =
    cmap_e (cmap_olift_at_action cut amount rho)
      (olift_e cut amount e)).
Proof.
  apply (syntax_ind
    (fun v => forall rho cut amount,
      olift_v cut amount (cmap_v rho v) =
      cmap_v (cmap_olift_at_action cut amount rho)
        (olift_v cut amount v))
    (fun e => forall rho cut amount,
      olift_e cut amount (cmap_e rho e) =
      cmap_e (cmap_olift_at_action cut amount rho)
        (olift_e cut amount e))).
  - reflexivity.
  - intros e IH rho cut amount. simpl. f_equal.
    rewrite <- cmap_olift_at_action_binder. apply IH.
  - intros v IH rho cut amount. simpl. f_equal. apply IH.
  - intros v IHv u IHu rho cut amount. simpl. f_equal;
      [apply IHv | apply IHu].
  - intros a IHa t IHt rho cut amount. simpl. f_equal.
    + apply IHa.
    + rewrite <- cmap_olift_at_action_binder. apply IHt.
  - intros e IH rho cut amount. simpl. f_equal.
    rewrite <- cmap_olift_at_action_shift. apply IH.
  - intros k e IH rho cut amount. simpl.
    rewrite admin_olift_plug_d. f_equal. apply IH.
  - intros k rho cut amount. simpl.
    unfold cmap_olift_at_action. destruct (rho k). reflexivity.
Qed.

Lemma cmap_action_olift_e e rho cut amount :
  olift_e cut amount (cmap_e rho e) =
  cmap_e (cmap_olift_at_action cut amount rho)
    (olift_e cut amount e).
Proof. apply (proj2 cmap_action_olift_v). Qed.

Lemma cmap_action_olift_c rho c cut amount :
  olift_c cut amount (cmap_c rho c) =
  cmap_c (cmap_olift_at_action cut amount rho)
    (olift_c cut amount c).
Proof.
  revert rho cut amount.
  induction c as [|c IH t]; intros rho cut amount; simpl.
  - reflexivity.
  - rewrite IH, (proj2 cmap_action_olift_v).
    rewrite cmap_olift_at_action_binder. reflexivity.
Qed.

Lemma olift_ectx_comp cut amount c d :
  olift_c cut amount (ectx_comp c d) =
  ectx_comp (olift_c cut amount c) (olift_c cut amount d).
Proof.
  induction c as [|c IH t]; simpl.
  - reflexivity.
  - rewrite IH. reflexivity.
Qed.

Lemma cmap_action_olift_d rho d cut amount :
  olift_d cut amount (cmap_d rho d) =
  cmap_d (cmap_olift_at_action cut amount rho)
    (olift_d cut amount d).
Proof.
  destruct d as [k c]. unfold cmap_d, cmap_olift_at_action.
  destruct (rho k) as [j d] eqn:Hrho.
  cbn [olift_d cmap_d cmap_olift_at_action].
  rewrite Hrho. cbn [olift_d].
  rewrite olift_ectx_comp, cmap_action_olift_c. reflexivity.
Qed.

Lemma cmap_olift_comp rho sigma :
  cmap_olift (cmap_comp rho sigma) =
  cmap_comp (cmap_olift rho) (cmap_olift sigma).
Proof.
  apply functional_extensionality. intro k.
  unfold cmap_olift, cmap_comp.
  change (olift_d 0 1 (cmap_d rho (sigma k)) =
    cmap_d (cmap_olift rho) (olift_d 0 1 (sigma k))).
  apply cmap_action_olift_d.
Qed.

(** Reindex a continuation map after inserting [amount] fresh continuation
    variables at [cut].  Entries in the inserted interval are bare; every
    old installed continuation is lifted together with its domain index. *)
Definition cmap_kinsert (cut amount : nat) (rho : cmap) : cmap :=
  fun k =>
    if Nat.ltb k cut then klift_d cut amount (rho k)
    else if Nat.ltb k (cut + amount) then ICont k CHole
    else klift_d cut amount (rho (k - amount)).

Lemma cmap_kinsert_image cut amount rho k :
  cmap_kinsert cut amount rho
    (if Nat.leb cut k then k + amount else k) =
  klift_d cut amount (rho k).
Proof.
  unfold cmap_kinsert.
  destruct (Nat.leb cut k) eqn:Hle.
  - apply Nat.leb_le in Hle.
    assert (Hlt0 : Nat.ltb (k + amount) cut = false)
      by (apply Nat.ltb_ge; lia).
    assert (Hlt1 : Nat.ltb (k + amount) (cut + amount) = false)
      by (apply Nat.ltb_ge; lia).
    rewrite Hlt0, Hlt1. replace (k + amount - amount) with k by lia.
    reflexivity.
  - apply Nat.leb_gt in Hle.
    assert (Hlt0 : Nat.ltb k cut = true) by (apply Nat.ltb_lt; lia).
    rewrite Hlt0. reflexivity.
Qed.

Lemma admin_klift_d_cross (cut amount : nat) (d : installed) :
  klift_d (S cut) amount (klift_d 0 1 d) =
  klift_d 0 1 (klift_d cut amount d).
Proof.
  destruct d as [k c]. simpl. f_equal.
  - assert (Htest :
      (match k + 1 with
       | 0 => false
       | S m => Nat.leb cut m
       end) = Nat.leb cut k).
    { rewrite Nat.add_1_r. reflexivity. }
    rewrite Htest.
    destruct (Nat.leb cut k); lia.
  - induction c as [|c IH t]; simpl.
    + reflexivity.
    + rewrite IH. f_equal. apply klift_comp_shift_e. lia.
Qed.

Lemma cmap_kinsert_olift cut amount rho :
  cmap_olift (cmap_kinsert cut amount rho) =
  cmap_kinsert cut amount (cmap_olift rho).
Proof.
  apply functional_extensionality. intro k.
  unfold cmap_olift, cmap_kinsert.
  destruct (Nat.ltb k cut), (Nat.ltb k (cut + amount)); simpl;
    try reflexivity;
    symmetry; apply admin_klift_olift_d_general.
Qed.

Lemma cmap_kinsert_up cut amount rho :
  cmap_up (cmap_kinsert cut amount rho) =
  cmap_kinsert (S cut) amount (cmap_up rho).
Proof.
  apply functional_extensionality. intros [|k].
  - unfold cmap_up, cmap_kinsert. simpl.
    destruct cut; simpl; reflexivity.
  - unfold cmap_up, cmap_kinsert.
    assert (Hcut : Nat.ltb (S k) (S cut) = Nat.ltb k cut).
    { reflexivity. }
    assert (Hsum : Nat.ltb (S k) (S cut + amount) =
        Nat.ltb k (cut + amount)).
    { replace (S cut + amount) with (S (cut + amount)) by lia.
      reflexivity. }
    rewrite Hcut, Hsum.
    destruct (Nat.ltb k cut) eqn:H0;
      destruct (Nat.ltb k (cut + amount)) eqn:H1; simpl.
    + symmetry. apply admin_klift_d_cross.
    + symmetry. apply admin_klift_d_cross.
    + f_equal. lia.
    + destruct amount as [|amount].
      * rewrite !admin_klift_zero_d, Nat.sub_0_r. reflexivity.
      * apply Nat.ltb_ge in H1.
        replace (k - amount) with (S (k - S amount)) by lia.
        simpl. symmetry. apply admin_klift_d_cross.
Qed.

Lemma cmap_action_klift_v :
  (forall v rho cut amount,
    klift_v cut amount (cmap_v rho v) =
    cmap_v (cmap_kinsert cut amount rho)
      (klift_v cut amount v)) /\
  (forall e rho cut amount,
    klift_e cut amount (cmap_e rho e) =
    cmap_e (cmap_kinsert cut amount rho)
      (klift_e cut amount e)).
Proof.
  apply (syntax_ind
    (fun v => forall rho cut amount,
      klift_v cut amount (cmap_v rho v) =
      cmap_v (cmap_kinsert cut amount rho)
        (klift_v cut amount v))
    (fun e => forall rho cut amount,
      klift_e cut amount (cmap_e rho e) =
      cmap_e (cmap_kinsert cut amount rho)
        (klift_e cut amount e))).
  - reflexivity.
  - intros e IH rho cut amount. simpl. f_equal.
    rewrite cmap_kinsert_olift. apply IH.
  - intros v IH rho cut amount. simpl. f_equal. apply IH.
  - intros v IHv u IHu rho cut amount. simpl. f_equal;
      [apply IHv | apply IHu].
  - intros a IHa t IHt rho cut amount. simpl. f_equal.
    + apply IHa.
    + rewrite cmap_kinsert_olift. apply IHt.
  - intros e IH rho cut amount. simpl. f_equal.
    rewrite cmap_kinsert_up. apply IH.
  - intros k e IH rho cut amount. simpl.
    rewrite admin_klift_plug_d.
    rewrite cmap_kinsert_image. f_equal. apply IH.
  - intros k rho cut amount. simpl.
    rewrite cmap_kinsert_image. destruct (rho k). reflexivity.
Qed.

Lemma cmap_action_klift_e e rho cut amount :
  klift_e cut amount (cmap_e rho e) =
  cmap_e (cmap_kinsert cut amount rho)
    (klift_e cut amount e).
Proof. apply (proj2 cmap_action_klift_v). Qed.

Lemma cmap_action_klift_c rho c cut amount :
  klift_c cut amount (cmap_c rho c) =
  cmap_c (cmap_kinsert cut amount rho)
    (klift_c cut amount c).
Proof.
  revert rho cut amount.
  induction c as [|c IH t]; intros rho cut amount; simpl.
  - reflexivity.
  - rewrite IH, (proj2 cmap_action_klift_v).
    rewrite cmap_kinsert_olift. reflexivity.
Qed.

Lemma klift_ectx_comp cut amount c d :
  klift_c cut amount (ectx_comp c d) =
  ectx_comp (klift_c cut amount c) (klift_c cut amount d).
Proof.
  induction c as [|c IH t]; simpl.
  - reflexivity.
  - rewrite IH. reflexivity.
Qed.

Lemma cmap_action_klift_d rho d cut amount :
  klift_d cut amount (cmap_d rho d) =
  cmap_d (cmap_kinsert cut amount rho)
    (klift_d cut amount d).
Proof.
  destruct d as [k c].
  unfold cmap_d. destruct (rho k) as [j d] eqn:Hrho.
  cbn [klift_d cmap_kinsert].
  rewrite cmap_kinsert_image.
  rewrite Hrho.
  cbn [cmap_d]. rewrite klift_ectx_comp, cmap_action_klift_c.
  reflexivity.
Qed.

Lemma cmap_kinsert_zero_one rho :
  cmap_kinsert 0 1 rho = cmap_up rho.
Proof.
  apply functional_extensionality. intros [|k].
  - reflexivity.
  - unfold cmap_kinsert, cmap_up. simpl.
    replace (k - 0) with k by lia. reflexivity.
Qed.

Lemma cmap_up_comp rho sigma :
  cmap_up (cmap_comp rho sigma) =
  cmap_comp (cmap_up rho) (cmap_up sigma).
Proof.
  apply functional_extensionality. intros [|k].
  - reflexivity.
  - change (klift_d 0 1 (cmap_d rho (sigma k)) =
      cmap_d (cmap_up rho) (klift_d 0 1 (sigma k))).
    rewrite <- (cmap_kinsert_zero_one rho).
    apply cmap_action_klift_d.
Qed.

Lemma cmap_action_comp_v :
  (forall v rho sigma,
    cmap_v rho (cmap_v sigma v) =
    cmap_v (cmap_comp rho sigma) v) /\
  (forall e rho sigma,
    cmap_e rho (cmap_e sigma e) =
    cmap_e (cmap_comp rho sigma) e).
Proof.
  apply (syntax_ind
    (fun v => forall rho sigma,
      cmap_v rho (cmap_v sigma v) = cmap_v (cmap_comp rho sigma) v)
    (fun e => forall rho sigma,
      cmap_e rho (cmap_e sigma e) = cmap_e (cmap_comp rho sigma) e)).
  - reflexivity.
  - intros e IH rho sigma. simpl. f_equal.
    rewrite cmap_olift_comp. apply IH.
  - intros v IH rho sigma. simpl. f_equal. apply IH.
  - intros v IHv u IHu rho sigma. simpl. f_equal;
      [apply IHv | apply IHu].
  - intros a IHa t IHt rho sigma. simpl. f_equal.
    + apply IHa.
    + rewrite cmap_olift_comp. apply IHt.
  - intros e IH rho sigma. simpl. f_equal.
    rewrite cmap_up_comp. apply IH.
  - intros k e IH rho sigma. simpl.
    rewrite cmap_plug_d, IH. reflexivity.
  - intros k rho sigma. simpl. apply cmap_ask_of.
Qed.

Lemma cmap_action_comp_e e rho sigma :
  cmap_e rho (cmap_e sigma e) = cmap_e (cmap_comp rho sigma) e.
Proof. apply (proj2 cmap_action_comp_v). Qed.

Lemma cmap_action_comp_c rho sigma c :
  cmap_c rho (cmap_c sigma c) = cmap_c (cmap_comp rho sigma) c.
Proof.
  revert rho sigma.
  induction c as [|c IH t]; intros rho sigma; simpl.
  - reflexivity.
  - rewrite IH, (proj2 cmap_action_comp_v), cmap_olift_comp.
    reflexivity.
Qed.

Lemma cmap_ectx_comp rho c d :
  cmap_c rho (ectx_comp c d) =
  ectx_comp (cmap_c rho c) (cmap_c rho d).
Proof.
  induction c as [|c IH t]; simpl.
  - reflexivity.
  - rewrite IH. reflexivity.
Qed.

Lemma cmap_action_comp_d rho sigma d :
  cmap_d rho (cmap_d sigma d) = cmap_d (cmap_comp rho sigma) d.
Proof.
  destruct d as [k c].
  destruct (sigma k) as [j d] eqn:Hsigma.
  destruct (rho j) as [i f] eqn:Hrho.
  unfold cmap_d, cmap_comp. rewrite Hsigma, Hrho. simpl.
  rewrite cmap_ectx_comp, cmap_action_comp_c, <- ectx_comp_assoc.
  rewrite Hrho. reflexivity.
Qed.

Lemma cmap_comp_assoc rho sigma tau :
  cmap_comp rho (cmap_comp sigma tau) =
  cmap_comp (cmap_comp rho sigma) tau.
Proof.
  apply functional_extensionality. intro k.
  unfold cmap_comp. apply cmap_action_comp_d.
Qed.

(** The continuation map accumulated by repeatedly bubbling a shift through
    an evaluation-context spine.  The order mirrors reduction: first capture
    the inner spine, then install the outer let frame. *)
Fixpoint capture_cmap (c : ectx) : cmap :=
  match c with
  | CHole => cmap_id
  | CLet c t => cmap_comp (repl_cmap 0 (frame t)) (capture_cmap c)
  end.

Lemma cmap_repl_klift_c cut d c :
  cmap_c (repl_cmap cut d) (klift_c cut 1 c) = klift_c cut 1 c.
Proof.
  induction c as [|c IH t]; simpl.
  - reflexivity.
  - rewrite repl_cmap_olift, IH.
    rewrite cmap_repl_e.
    rewrite (proj2 admin_krepl_no_cocc (klift_e cut 1 t) cut
      (olift_d 0 1 d) (cocc_klift_fresh_e cut t)).
    reflexivity.
Qed.

Lemma cmap_repl_klift_d cut d f :
  cmap_d (repl_cmap cut d) (klift_d cut 1 f) = klift_d cut 1 f.
Proof.
  destruct f as [k c].
  unfold cmap_d, repl_cmap. simpl.
  destruct (Nat.leb cut k) eqn:Hle.
  - assert (Hneq : Nat.eqb (k + 1) cut = false).
    { apply Nat.eqb_neq. apply Nat.leb_le in Hle. lia. }
    rewrite Hneq. simpl.
    f_equal. now apply cmap_repl_klift_c.
  - assert (Hneq : Nat.eqb k cut = false).
    { apply Nat.eqb_neq. apply Nat.leb_gt in Hle. lia. }
    rewrite Hneq. simpl.
    f_equal. now apply cmap_repl_klift_c.
Qed.

Lemma capture_cmap_klift : forall c,
  (forall v, cmap_v (capture_cmap c) (klift_v 0 1 v) = klift_v 0 1 v) /\
  (forall e, cmap_e (capture_cmap c) (klift_e 0 1 e) = klift_e 0 1 e) /\
  (forall d, cmap_d (capture_cmap c) (klift_d 0 1 d) = klift_d 0 1 d).
Proof.
  intro c. induction c as [|c IH t].
  - repeat split; intros; [apply cmap_id_v | apply cmap_id_e | apply cmap_d_id].
  - destruct IH as [IHv [IHe IHd]]. repeat split; intros.
    + simpl. rewrite <- (proj1 cmap_action_comp_v), IHv.
      rewrite cmap_repl_v.
      apply (proj1 admin_krepl_no_cocc).
      apply cocc_klift_fresh_v.
    + simpl. rewrite <- cmap_action_comp_e, IHe.
      rewrite cmap_repl_e.
      apply (proj2 admin_krepl_no_cocc).
      apply cocc_klift_fresh_e.
    + simpl. rewrite <- cmap_action_comp_d, IHd.
      apply cmap_repl_klift_d.
Qed.

Lemma capture_cmap_bare c :
  cmap_d (capture_cmap c) (ICont 0 CHole) =
  ICont 0 (klift_c 0 1 c).
Proof.
  induction c as [|c IH t].
  - reflexivity.
  - change (cmap_d
      (cmap_comp (repl_cmap 0 (frame t)) (capture_cmap c))
      (ICont 0 CHole) =
      ICont 0 (CLet (klift_c 0 1 c) (klift_e 0 1 t))).
    rewrite <- cmap_action_comp_d, IH.
    unfold cmap_d.
    assert (Hhead : repl_cmap 0 (frame t) 0 = frame t)
      by reflexivity.
    rewrite Hhead. simpl.
    rewrite cmap_repl_klift_c.
    reflexivity.
Qed.

Lemma cmap_d_bare rho k : cmap_d rho (ICont k CHole) = rho k.
Proof.
  unfold cmap_d. destruct (rho k) as [j c]. simpl.
  rewrite ectx_comp_hole_r. reflexivity.
Qed.

Lemma cmap_sub_klift_cancel_c j c :
  cmap_c (csub_map 0 (ICont j CHole)) (klift_c 0 1 c) = c.
Proof.
  induction c as [|c IH t]; simpl.
  - reflexivity.
  - rewrite cmap_sub_olift, IH, cmap_sub_e.
    rewrite ksubst_klift_cancel_e0. reflexivity.
Qed.

Lemma cmap_sub_klift_cancel_d j d :
  cmap_d (csub_map 0 (ICont j CHole)) (klift_d 0 1 d) = d.
Proof.
  destruct d as [k c]. cbn [klift_d].
  replace (Nat.leb 0 k) with true by
    (symmetry; apply Nat.leb_le; lia).
  unfold cmap_d.
  assert (Hmap : csub_map 0 (ICont j CHole) (k + 1) =
      ICont k CHole).
  { replace (k + 1) with (S k) by lia.
    unfold csub_map. reflexivity. }
  rewrite Hmap. simpl. f_equal. apply cmap_sub_klift_cancel_c.
Qed.

Lemma cmap_sub_bound_context j c :
  cmap_d (csub_map 0 (ICont j CHole))
    (ICont 0 (klift_c 0 1 c)) = ICont j c.
Proof.
  unfold cmap_d.
  assert (Hmap : csub_map 0 (ICont j CHole) 0 = ICont j CHole).
  { unfold csub_map. rewrite remove_index_eq. reflexivity. }
  rewrite Hmap. simpl. f_equal. apply cmap_sub_klift_cancel_c.
Qed.

Lemma capture_cmap_sub sigma k j c :
  sigma k = ICont j c ->
  cmap_comp (csub_map 0 (ICont j CHole))
    (cmap_comp (capture_cmap c) (cmap_up sigma)) =
  cmap_comp sigma (csub_map 0 (ICont k CHole)).
Proof.
  intro Hsigma. apply functional_extensionality. intros [|n].
  - change (cmap_d (csub_map 0 (ICont j CHole))
      (cmap_d (capture_cmap c) (ICont 0 CHole)) =
      cmap_d sigma (ICont k CHole)).
    rewrite capture_cmap_bare, cmap_d_bare, Hsigma.
    apply cmap_sub_bound_context.
  - change (cmap_d (csub_map 0 (ICont j CHole))
      (cmap_d (capture_cmap c) (klift_d 0 1 (sigma n))) =
      cmap_d sigma (ICont n CHole)).
    rewrite cmap_d_bare.
    rewrite (proj2 (proj2 (capture_cmap_klift c))).
    apply cmap_sub_klift_cancel_d.
Qed.

Lemma admin_capture_ectx_star c e :
  star admin_step (plug c (EShift e))
    (EShift (cmap_e (capture_cmap c) e)).
Proof.
  induction c as [|c IH t]; simpl.
  - rewrite cmap_id_e. apply star_refl.
  - eapply star_trans.
    + apply (admin_star_map admin_step admin_step (fun x => ELet x t)).
      * intros x y Hxy. now apply AS_LetBinding.
      * exact IH.
    + eapply star_step.
      * apply AS_LetShift.
      * rewrite <- cmap_repl_e, cmap_action_comp_e. apply star_refl.
Qed.

Lemma admin_capture_installed_star k c e :
  star admin_step (plug_d (ICont k c) (EShift e))
    (ECont k (EShift (cmap_e (capture_cmap c) e))).
Proof.
  simpl.
  apply (admin_star_map admin_step admin_step (ECont k)).
  - intros x y Hxy. now apply AS_ContBody.
  - apply admin_capture_ectx_star.
Qed.

(** Parallel relatedness of installed evaluation contexts.  This is the
    semantic relation carried pointwise by the source and target maps in the
    generalized postponement theorem. *)
Inductive core_ectx_parallel (delta : payload_env) : ectx -> ectx -> Prop :=
| CEP_Hole : core_ectx_parallel delta CHole CHole
| CEP_Let : forall c c' t t',
    core_ectx_parallel delta c c' ->
    core_parallel (payload_env_olift delta) t t' ->
    core_ectx_parallel delta (CLet c t) (CLet c' t').

Inductive core_installed_parallel (delta : payload_env) :
    installed -> installed -> Prop :=
| CIP_Cont : forall k c c',
    core_ectx_parallel delta c c' ->
    core_installed_parallel delta (ICont k c) (ICont k c').

Definition core_cmap_parallel (delta : payload_env)
    (rho sigma : cmap) : Prop :=
  forall k, core_installed_parallel delta (rho k) (sigma k).

Definition cmap_payload_coherent (input output : payload_env)
    (rho : cmap) : Prop :=
  forall k v, input k = Some v ->
    match rho k with
    | ICont j _ => output j = Some (cmap_v rho v)
    end.

Lemma core_ectx_parallel_olift_at delta c c' :
  core_ectx_parallel delta c c' -> forall cut,
  core_ectx_parallel (payload_env_olift_at cut delta)
    (olift_c cut 1 c) (olift_c cut 1 c').
Proof.
  intro H. induction H; intro cut; simpl.
  - apply CEP_Hole.
  - apply CEP_Let.
    + now apply IHcore_ectx_parallel.
    + pose proof (core_parallel_olift_expr_at H0 (S cut)) as Hlift.
      rewrite payload_env_olift_at_payload_env_olift in Hlift.
      exact Hlift.
Qed.

Lemma core_installed_parallel_olift delta d d' :
  core_installed_parallel delta d d' ->
  core_installed_parallel (payload_env_olift delta)
    (olift_d 0 1 d) (olift_d 0 1 d').
Proof.
  intro H. inversion H; subst. simpl. apply CIP_Cont.
  rewrite <- payload_env_olift_at_0.
  now apply core_ectx_parallel_olift_at.
Qed.

Lemma core_cmap_parallel_olift delta rho sigma :
  core_cmap_parallel delta rho sigma ->
  core_cmap_parallel (payload_env_olift delta)
    (cmap_olift rho) (cmap_olift sigma).
Proof.
  intros H k. apply core_installed_parallel_olift. apply H.
Qed.

Lemma core_ectx_parallel_klift_at delta c c' :
  core_ectx_parallel delta c c' -> forall cut,
  core_ectx_parallel (payload_env_klift_at cut delta)
    (klift_c cut 1 c) (klift_c cut 1 c').
Proof.
  intro H. induction H; intro cut; simpl.
  - apply CEP_Hole.
  - apply CEP_Let.
    + now apply IHcore_ectx_parallel.
    + pose proof (core_parallel_klift_expr_at H0 cut) as Hlift.
      rewrite payload_env_klift_at_olift in Hlift. exact Hlift.
Qed.

Lemma core_installed_parallel_klift delta d d' :
  core_installed_parallel delta d d' ->
  core_installed_parallel (payload_env_klift delta)
    (klift_d 0 1 d) (klift_d 0 1 d').
Proof.
  intro H. inversion H; subst. simpl.
  replace (Nat.leb 0 k) with true by
    (symmetry; apply Nat.leb_le; lia).
  apply CIP_Cont.
  rewrite <- payload_env_klift_at_0.
  now apply core_ectx_parallel_klift_at.
Qed.

Lemma core_cmap_parallel_up delta rho sigma :
  core_cmap_parallel delta rho sigma ->
  core_cmap_parallel (payload_env_klift delta)
    (cmap_up rho) (cmap_up sigma).
Proof.
  intros H [|k].
  - simpl. apply CIP_Cont. apply CEP_Hole.
  - simpl. apply core_installed_parallel_klift. apply H.
Qed.

Lemma cmap_payload_coherent_olift input output rho :
  cmap_payload_coherent input output rho ->
  cmap_payload_coherent (payload_env_olift input)
    (payload_env_olift output) (cmap_olift rho).
Proof.
  intros H k v Hlookup.
  unfold payload_env_olift in Hlookup.
  destruct (input k) as [w|] eqn:Hw; simpl in Hlookup; [|discriminate].
  inversion Hlookup; subst v.
  specialize (H k w Hw).
  destruct (rho k) as [j c] eqn:Hrho. simpl in H |- *.
  unfold cmap_olift. rewrite Hrho. simpl.
  change (option_map (olift_v 0 1) (output j) =
    Some (cmap_v (cmap_olift rho) (olift_v 0 1 w))).
  rewrite H. simpl. f_equal.
  change (olift_v 0 1 (cmap_v rho w) =
    cmap_v (cmap_olift rho) (olift_v 0 1 w)).
  apply (proj1 cmap_action_olift_v).
Qed.

Lemma cmap_payload_coherent_up input output rho :
  cmap_payload_coherent input output rho ->
  cmap_payload_coherent (payload_env_klift input)
    (payload_env_klift output) (cmap_up rho).
Proof.
  intros H [|k] v Hlookup; simpl in Hlookup; [discriminate|].
  destruct (input k) as [w|] eqn:Hw; simpl in Hlookup; [|discriminate].
  inversion Hlookup; subst v.
  specialize (H k w Hw).
  destruct (rho k) as [j c] eqn:Hrho. simpl in H |- *.
  unfold cmap_up. rewrite Hrho. simpl.
  replace (j + 1) with (S j) by lia.
  change (option_map (klift_v 0 1) (output j) =
    Some (cmap_v (cmap_up rho) (klift_v 0 1 w))).
  rewrite H. simpl. f_equal.
  change (klift_v 0 1 (cmap_v rho w) =
    cmap_v (cmap_up rho) (klift_v 0 1 w)).
  rewrite <- cmap_kinsert_zero_one. apply (proj1 cmap_action_klift_v).
Qed.

Lemma core_ectx_parallel_plug delta c c' e e' :
  core_ectx_parallel delta c c' ->
  core_parallel delta e e' ->
  core_parallel delta (plug c e) (plug c' e').
Proof.
  intros Hc He. induction Hc as [|c c' t t' Hc IH Ht]; simpl.
  - exact He.
  - apply CP_Let; [now apply IH | exact Ht].
Qed.

Lemma core_installed_parallel_plug delta d d' e e' :
  core_installed_parallel delta d d' ->
  core_parallel delta e e' ->
  core_parallel delta (plug_d d e) (plug_d d' e').
Proof.
  intros Hd He. inversion Hd; subst. simpl.
  apply CP_Cont. now apply core_ectx_parallel_plug.
Qed.

Lemma core_capture_maps_parallel output rho sigma k j c c' :
  core_cmap_parallel output rho sigma ->
  rho k = ICont j c -> sigma k = ICont j c' ->
  core_cmap_parallel (payload_env_klift output)
    (cmap_comp (capture_cmap c) (cmap_up rho))
    (cmap_comp (capture_cmap c') (cmap_up sigma)).
Proof.
  intros Hmaps Hrho Hsigma.
  pose proof (Hmaps k) as Hhead.
  rewrite Hrho, Hsigma in Hhead. inversion Hhead; subst.
  intros [|n].
  - change (core_installed_parallel (payload_env_klift output)
      (cmap_d (capture_cmap c) (ICont 0 CHole))
      (cmap_d (capture_cmap c') (ICont 0 CHole))).
    rewrite !capture_cmap_bare.
    apply CIP_Cont.
    rewrite <- payload_env_klift_at_0.
    now apply core_ectx_parallel_klift_at.
  - change (core_installed_parallel (payload_env_klift output)
      (cmap_d (capture_cmap c) (klift_d 0 1 (rho n)))
      (cmap_d (capture_cmap c') (klift_d 0 1 (sigma n)))).
    rewrite (proj2 (proj2 (capture_cmap_klift c))).
    rewrite (proj2 (proj2 (capture_cmap_klift c'))).
    apply core_installed_parallel_klift. apply Hmaps.
Qed.

Lemma capture_cmap_value_up sigma c v :
  cmap_v (cmap_comp (capture_cmap c) (cmap_up sigma))
    (klift_v 0 1 v) =
  klift_v 0 1 (cmap_v sigma v).
Proof.
  rewrite <- (proj1 cmap_action_comp_v).
  assert (Hup : cmap_v (cmap_up sigma) (klift_v 0 1 v) =
      klift_v 0 1 (cmap_v sigma v)).
  { rewrite <- cmap_kinsert_zero_one.
    symmetry. apply (proj1 cmap_action_klift_v). }
  rewrite Hup. apply (proj1 (capture_cmap_klift c)).
Qed.

Lemma capture_cmap_payload_coherent input output sigma k j c :
  cmap_payload_coherent input output sigma ->
  sigma k = ICont j c ->
  cmap_payload_coherent (payload_env_klift input)
    (payload_env_klift output)
    (cmap_comp (capture_cmap c) (cmap_up sigma)).
Proof.
  intros Hcoherent Hsigma [|n] v Hlookup; simpl in Hlookup;
    [discriminate|].
  destruct (input n) as [w|] eqn:Hw; simpl in Hlookup; [|discriminate].
  inversion Hlookup; subst v.
  specialize (Hcoherent n w Hw).
  destruct (sigma n) as [i d] eqn:Hn.
  simpl in Hcoherent.
  assert (Hmap :
      cmap_comp (capture_cmap c) (cmap_up sigma) (S n) =
      klift_d 0 1 (ICont i d)).
  { unfold cmap_comp, cmap_up. rewrite Hn.
    apply (proj2 (proj2 (capture_cmap_klift c))). }
  rewrite Hmap.
  simpl. replace (i + 1) with (S i) by lia.
  change (option_map (klift_v 0 1) (output i) =
    Some (cmap_v (cmap_comp (capture_cmap c) (cmap_up sigma))
      (klift_v 0 1 w))).
  rewrite Hcoherent. simpl. f_equal.
  symmetry. apply capture_cmap_value_up.
Qed.

Lemma cmap_osubst_fusion :
  (forall x rho cut v,
    cmap_v rho (osubst_v cut v x) =
    osubst_v cut (cmap_v rho v)
      (cmap_v (cmap_olift_at_action cut 1 rho) x)) /\
  (forall e rho cut v,
    cmap_e rho (osubst_e cut v e) =
    osubst_e cut (cmap_v rho v)
      (cmap_e (cmap_olift_at_action cut 1 rho) e)).
Proof.
  apply (syntax_ind
    (fun x => forall rho cut v,
      cmap_v rho (osubst_v cut v x) =
      osubst_v cut (cmap_v rho v)
        (cmap_v (cmap_olift_at_action cut 1 rho) x))
    (fun e => forall rho cut v,
      cmap_e rho (osubst_e cut v e) =
      osubst_e cut (cmap_v rho v)
        (cmap_e (cmap_olift_at_action cut 1 rho) e))).
  - intros n rho cut v. simpl.
    destruct (remove_index cut n); reflexivity.
  - intros e IH rho cut v. simpl. f_equal.
    rewrite (IH (cmap_olift rho) (S cut) (olift_v 0 1 v)).
    rewrite <- cmap_olift_at_action_binder.
    assert (Hv : cmap_v (cmap_olift rho) (olift_v 0 1 v) =
        olift_v 0 1 (cmap_v rho v)).
    { symmetry. apply (proj1 cmap_action_olift_v). }
    rewrite Hv.
    reflexivity.
  - intros x IH rho cut v. simpl. f_equal. apply IH.
  - intros x IHx y IHy rho cut v. simpl. f_equal;
      [apply IHx | apply IHy].
  - intros a IHa t IHt rho cut v. simpl. f_equal.
    + apply IHa.
    + rewrite (IHt (cmap_olift rho) (S cut) (olift_v 0 1 v)).
      rewrite <- cmap_olift_at_action_binder.
      assert (Hv : cmap_v (cmap_olift rho) (olift_v 0 1 v) =
          olift_v 0 1 (cmap_v rho v)).
      { symmetry. apply (proj1 cmap_action_olift_v). }
      rewrite Hv.
      reflexivity.
  - intros e IH rho cut v. simpl. f_equal.
    rewrite (IH (cmap_up rho) cut (klift_v 0 1 v)).
    rewrite cmap_olift_at_action_shift.
    assert (Hv : cmap_v (cmap_up rho) (klift_v 0 1 v) =
        klift_v 0 1 (cmap_v rho v)).
    { rewrite <- cmap_kinsert_zero_one.
      symmetry. apply (proj1 cmap_action_klift_v). }
    rewrite Hv. reflexivity.
  - intros k e IH rho cut v. simpl.
    rewrite osubst_plug_installed, IH.
    unfold cmap_olift_at_action.
    rewrite osubst_olift_cancel_installed. reflexivity.
  - intros k rho cut v. simpl.
    unfold cmap_olift_at_action. destruct (rho k). reflexivity.
Qed.

Lemma cmap_osubst0_fusion_e rho v e :
  cmap_e rho (subst_e (subst0 v) e) =
  subst_e (subst0 (cmap_v rho v)) (cmap_e (cmap_olift rho) e).
Proof.
  replace (subst_e (subst0 v) e) with (osubst_e 0 v e)
    by (symmetry; apply omap_single_e).
  replace (subst_e (subst0 (cmap_v rho v))
      (cmap_e (cmap_olift rho) e)) with
    (osubst_e 0 (cmap_v rho v) (cmap_e (cmap_olift rho) e))
    by (symmetry; apply omap_single_e).
  change (cmap_e rho (osubst_e 0 v e) =
    osubst_e 0 (cmap_v rho v)
      (cmap_e (cmap_olift_at_action 0 1 rho) e)).
  apply (proj2 cmap_osubst_fusion).
Qed.

Lemma admin_star_plug c e e' :
  star admin_step e e' ->
  star admin_step (plug c e) (plug c e').
Proof.
  intro H. induction c as [|c IH t]; simpl.
  - exact H.
  - apply (admin_star_map admin_step admin_step (fun x => ELet x t)).
    + intros x y Hxy. now apply AS_LetBinding.
    + now apply IH.
Qed.

Lemma admin_star_plug_d d e e' :
  star admin_step e e' ->
  star admin_step (plug_d d e) (plug_d d e').
Proof.
  intros H. destruct d as [k c]. simpl.
  apply (admin_star_map admin_step admin_step (ECont k)).
  - intros x y Hxy. now apply AS_ContBody.
  - now apply admin_star_plug.
Qed.

(** Once the root control residual is supplied, postponement through an
    arbitrary pair of related continuation maps is structural. *)
Lemma core_parallel_cmap_postponement_from_contshift
    (Hcapture_parallel : forall output rho sigma k j c c',
      core_cmap_parallel output rho sigma ->
      rho k = ICont j c -> sigma k = ICont j c' ->
      core_cmap_parallel (payload_env_klift output)
        (cmap_comp (capture_cmap c) (cmap_up rho))
        (cmap_comp (capture_cmap c') (cmap_up sigma)))
    (Hcapture_coherent : forall input output sigma k j c,
      cmap_payload_coherent input output sigma ->
      sigma k = ICont j c ->
      cmap_payload_coherent (payload_env_klift input)
        (payload_env_klift output)
        (cmap_comp (capture_cmap c) (cmap_up sigma)))
    (Hcapture_sub : forall sigma k j c,
      sigma k = ICont j c ->
      cmap_comp (csub_map 0 (ICont j CHole))
        (cmap_comp (capture_cmap c) (cmap_up sigma)) =
      cmap_comp sigma (csub_map 0 (ICont k CHole))) :
  forall input,
  (forall v v', core_value_parallel input v v' ->
    forall output rho sigma,
      core_cmap_parallel output rho sigma ->
      cmap_payload_coherent input output sigma ->
      exists r,
        star admin_vstep (cmap_v rho v) r /\
        core_value_parallel output r (cmap_v sigma v')) /\
  (forall e e', core_parallel input e e' ->
    forall output rho sigma,
      core_cmap_parallel output rho sigma ->
      cmap_payload_coherent input output sigma ->
      exists r,
        star admin_step (cmap_e rho e) r /\
        core_parallel output r (cmap_e sigma e')).
Proof.
  intro input.
  apply (core_parallel_mutind
    (fun input v v' _ => forall output rho sigma,
      core_cmap_parallel output rho sigma ->
      cmap_payload_coherent input output sigma ->
      exists r,
        star admin_vstep (cmap_v rho v) r /\
        core_value_parallel output r (cmap_v sigma v'))
    (fun input e e' _ => forall output rho sigma,
      core_cmap_parallel output rho sigma ->
      cmap_payload_coherent input output sigma ->
      exists r,
        star admin_step (cmap_e rho e) r /\
        core_parallel output r (cmap_e sigma e'))).
  - intros d n output rho sigma Hmaps Hpayload.
    exists (VOrd n). split; [apply star_refl | apply CP_VOrd].
  - intros d e e' He IH output rho sigma Hmaps Hpayload.
    destruct (IH (payload_env_olift output)
      (cmap_olift rho) (cmap_olift sigma)
      (core_cmap_parallel_olift output rho sigma Hmaps)
      (cmap_payload_coherent_olift d output sigma Hpayload))
      as [r [Har Hcore]].
    exists (VLam r). split.
    + apply (admin_star_map admin_step admin_vstep VLam); [|exact Har].
      intros x y Hxy. now apply AVS_Lam.
    + now apply CP_VLam.
  - intros d v v' Hv IH output rho sigma Hmaps Hpayload.
    destruct (IH output rho sigma Hmaps Hpayload) as [r [Har Hcore]].
    exists (EVal r). split.
    + apply (admin_star_map admin_vstep admin_step EVal); [|exact Har].
      intros x y Hxy. now apply AS_Val.
    + now apply CP_Val.
  - intros d v v' u u' Hv IHv Hu IHu output rho sigma Hmaps Hpayload.
    destruct (IHv output rho sigma Hmaps Hpayload) as [r [Hvr Hvr']].
    destruct (IHu output rho sigma Hmaps Hpayload) as [s [Hus Hus']].
    exists (EApp r s). split.
    + eapply star_trans.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp x (cmap_v rho u))); [|exact Hvr].
        intros x y Hxy. now apply AS_AppL.
      * apply (admin_star_map admin_vstep admin_step (EApp r)); [|exact Hus].
        intros x y Hxy. now apply AS_AppR.
    + now apply CP_App.
  - intros d a a' t t' Ha IHa Ht IHt output rho sigma Hmaps Hpayload.
    destruct (IHa output rho sigma Hmaps Hpayload) as [r [Har Har']].
    destruct (IHt (payload_env_olift output)
      (cmap_olift rho) (cmap_olift sigma)
      (core_cmap_parallel_olift output rho sigma Hmaps)
      (cmap_payload_coherent_olift d output sigma Hpayload))
      as [s [Hts Hts']].
    exists (ELet r s). split.
    + eapply star_trans.
      * apply (admin_star_map admin_step admin_step
          (fun x => ELet x (cmap_e (cmap_olift rho) t)));
          [|exact Har].
        intros x y Hxy. now apply AS_LetBinding.
      * apply (admin_star_map admin_step admin_step (ELet r)); [|exact Hts].
        intros x y Hxy. now apply AS_LetBody.
    + now apply CP_Let.
  - intros d e e' He IH output rho sigma Hmaps Hpayload.
    destruct (IH (payload_env_klift output)
      (cmap_up rho) (cmap_up sigma)
      (core_cmap_parallel_up output rho sigma Hmaps)
      (cmap_payload_coherent_up d output sigma Hpayload))
      as [r [Har Hcore]].
    exists (EShift r). split.
    + apply (admin_star_map admin_step admin_step EShift); [|exact Har].
      intros x y Hxy. now apply AS_ShiftBody.
    + now apply CP_Shift.
  - intros d k e e' He IH output rho sigma Hmaps Hpayload.
    destruct (IH output rho sigma Hmaps Hpayload) as [r [Har Hcore]].
    pose proof (Hmaps k) as Hrel.
    destruct (rho k) as [j c] eqn:Hrho.
    destruct (sigma k) as [j' c'] eqn:Hsigma.
    inversion Hrel; subst j'.
    cbn [cmap_e]. rewrite Hrho, Hsigma. cbn [plug_d].
    exists (plug_d (ICont j c) r). split.
    + change (star admin_step
        (plug_d (ICont j c) (cmap_e rho e))
        (plug_d (ICont j c) r)).
      now apply admin_star_plug_d.
    + change (core_parallel output
        (plug_d (ICont j c) r)
        (plug_d (ICont j c') (cmap_e sigma e'))).
      apply core_installed_parallel_plug.
      * now apply CIP_Cont.
      * exact Hcore.
  - intros d k output rho sigma Hmaps Hpayload.
    pose proof (Hmaps k) as Hrel.
    destruct (rho k) as [j c] eqn:Hrho.
    destruct (sigma k) as [j' c'] eqn:Hsigma.
    inversion Hrel; subst j'.
    cbn [cmap_e]. rewrite Hrho, Hsigma. cbn [ask_of].
    exists (EAsk j). split; [apply star_refl | apply CP_AskId].
  - intros d k v Hlookup output rho sigma Hmaps Hpayload.
    pose proof (Hmaps k) as Hrel.
    destruct (rho k) as [j c] eqn:Hrho.
    destruct (sigma k) as [j' c'] eqn:Hsigma.
    inversion Hrel; subst j'.
    specialize (Hpayload k v Hlookup).
    rewrite Hsigma in Hpayload. simpl in Hpayload.
    cbn [cmap_e]. rewrite Hrho. cbn [ask_of].
    exists (EAsk j). split; [apply star_refl |].
    now apply CP_Ask with (v := cmap_v sigma v).
  - intros d e e' v v' He IHe Hv IHv output rho sigma Hmaps Hpayload.
    destruct (IHe (payload_env_olift output)
      (cmap_olift rho) (cmap_olift sigma)
      (core_cmap_parallel_olift output rho sigma Hmaps)
      (cmap_payload_coherent_olift d output sigma Hpayload))
      as [r [Her Her']].
    destruct (IHv output rho sigma Hmaps Hpayload) as [w [Hvw Hvw']].
    exists (EApp (VLam r) w). split.
    + eapply star_trans.
      * apply (admin_star_map admin_step admin_step
          (fun x => EApp (VLam x) (cmap_v rho v))); [|exact Her].
        intros x y Hxy. apply AS_AppL. now apply AVS_Lam.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp (VLam r) x)); [|exact Hvw].
        intros x y Hxy. now apply AS_AppR.
    + rewrite cmap_osubst0_fusion_e. now apply CP_Beta.
  - intros d v v' t t' Hv IHv Ht IHt output rho sigma Hmaps Hpayload.
    destruct (IHv output rho sigma Hmaps Hpayload) as [w [Hvw Hvw']].
    destruct (IHt (payload_env_olift output)
      (cmap_olift rho) (cmap_olift sigma)
      (core_cmap_parallel_olift output rho sigma Hmaps)
      (cmap_payload_coherent_olift d output sigma Hpayload))
      as [r [Htr Htr']].
    exists (ELet (EVal w) r). split.
    + eapply star_trans.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => ELet (EVal x) (cmap_e (cmap_olift rho) t)));
          [|exact Hvw].
        intros x y Hxy. apply AS_LetBinding. now apply AS_Val.
      * apply (admin_star_map admin_step admin_step (ELet (EVal w)));
          [|exact Htr].
        intros x y Hxy. now apply AS_LetBody.
    + rewrite cmap_osubst0_fusion_e. now apply CP_LetValue.
  - intros d k e e' He IH output rho sigma Hmaps Hpayload.
    pose proof (Hmaps k) as Hrel.
    destruct (rho k) as [j c] eqn:Hrho.
    destruct (sigma k) as [j' c'] eqn:Hsigma.
    inversion Hrel; subst j'.
    set (alpha := cmap_comp (capture_cmap c) (cmap_up rho)).
    set (beta := cmap_comp (capture_cmap c') (cmap_up sigma)).
    destruct (IH (payload_env_klift output) alpha beta
      (Hcapture_parallel output rho sigma k j c c' Hmaps Hrho Hsigma)
      (Hcapture_coherent d output sigma k j c' Hpayload Hsigma))
      as [r [Har Hcore]].
    exists (ECont j (EShift r)). split.
    + cbn [cmap_e]. rewrite Hrho. cbn [plug_d].
      eapply star_trans.
      * apply (admin_star_map admin_step admin_step (ECont j)).
        -- intros x y Hxy. now apply AS_ContBody.
        -- apply admin_capture_ectx_star.
      * unfold alpha in Har. rewrite <- cmap_action_comp_e in Har.
        apply (admin_star_map admin_step admin_step
          (fun x => ECont j (EShift x))).
        -- intros x y Hxy. apply AS_ContBody. now apply AS_ShiftBody.
        -- exact Har.
    + unfold beta in Hcore.
      rewrite <- cmap_action_comp_e in Hcore.
      pose proof (@CP_ContShift output j
        r
        (cmap_e (capture_cmap c') (cmap_e (cmap_up sigma) e'))
        Hcore) as Hroot.
      assert (Htarget :
        ksubst_e 0 (ICont j CHole)
          (cmap_e (capture_cmap c') (cmap_e (cmap_up sigma) e')) =
        cmap_e sigma (ksubst_e 0 (ICont k CHole) e')).
      { rewrite <- !cmap_sub_e.
        rewrite !cmap_action_comp_e.
        rewrite <- cmap_comp_assoc.
        rewrite (Hcapture_sub sigma k j c' Hsigma).
        reflexivity. }
      rewrite Htarget in Hroot. exact Hroot.
Qed.

Theorem core_parallel_cmap_postponement :
  forall input,
  (forall v v', core_value_parallel input v v' ->
    forall output rho sigma,
      core_cmap_parallel output rho sigma ->
      cmap_payload_coherent input output sigma ->
      exists r,
        star admin_vstep (cmap_v rho v) r /\
        core_value_parallel output r (cmap_v sigma v')) /\
  (forall e e', core_parallel input e e' ->
    forall output rho sigma,
      core_cmap_parallel output rho sigma ->
      cmap_payload_coherent input output sigma ->
      exists r,
        star admin_step (cmap_e rho e) r /\
        core_parallel output r (cmap_e sigma e')).
Proof.
  apply core_parallel_cmap_postponement_from_contshift.
  - exact core_capture_maps_parallel.
  - exact capture_cmap_payload_coherent.
  - exact capture_cmap_sub.
Qed.

Definition payload_env_fresh_at (delta : payload_env) (h : nat) : Prop :=
  forall k v, delta k = Some v -> cocc_v h v = false.

Lemma payload_env_fresh_at_olift delta h :
  payload_env_fresh_at delta h ->
  payload_env_fresh_at (payload_env_olift delta) h.
Proof.
  intros Hfresh k v Hlookup.
  unfold payload_env_olift in Hlookup.
  destruct (delta k) as [w|] eqn:Hw; simpl in Hlookup; [|discriminate].
  inversion Hlookup; subst v.
  rewrite (proj1 admin_cocc_olift). now apply (Hfresh k w).
Qed.

Lemma payload_env_fresh_at_klift delta h :
  payload_env_fresh_at delta h ->
  payload_env_fresh_at (payload_env_klift delta) (S h).
Proof.
  intros Hfresh [|k] v Hlookup; simpl in Hlookup; [discriminate|].
  destruct (delta k) as [w|] eqn:Hw; simpl in Hlookup; [|discriminate].
  inversion Hlookup; subst v.
  rewrite cocc_klift_zero_succ_v. now apply (Hfresh k w).
Qed.

Lemma payload_env_klift_fresh_zero delta :
  payload_env_fresh_at (payload_env_klift delta) 0.
Proof.
  intros [|k] v Hlookup; simpl in Hlookup; [discriminate|].
  destruct (delta k) as [w|]; simpl in Hlookup; [|discriminate].
  inversion Hlookup; subst v. apply cocc_klift_fresh_v.
Qed.

(** All structural and ordinary-substitution cases of frame postponement.
    The premise isolates the only constructor which is not homomorphic:
    a root [k.S] contraction whose surrounding [ECont] can be swallowed by
    the installed let frame. *)
Lemma core_parallel_frame_postponement_from_contshift
    (Hcontshift : forall delta h q q' k e e' r,
      payload_env_fresh_at delta h ->
      core_parallel (payload_env_olift delta) q q' ->
      core_parallel (payload_env_klift delta) e e' ->
      star admin_step
        (krepl_e (S h)
          (klift_d 0 1 (installed_let_frame h q)) e) r ->
      core_parallel (payload_env_klift delta) r
        (krepl_e (S h)
          (klift_d 0 1 (installed_let_frame h q')) e') ->
      exists r,
        star admin_step
          (krepl_e h (installed_let_frame h q)
            (ECont k (EShift e))) r /\
        core_parallel delta r
          (krepl_e h (installed_let_frame h q')
            (ksubst_e 0 (ICont k CHole) e'))) :
  forall delta,
  (forall v v', core_value_parallel delta v v' ->
    forall h q q',
      payload_env_fresh_at delta h ->
      core_parallel (payload_env_olift delta) q q' ->
      exists r,
        star admin_vstep
          (krepl_v h (installed_let_frame h q) v) r /\
        core_value_parallel delta r
          (krepl_v h (installed_let_frame h q') v')) /\
  (forall e e', core_parallel delta e e' ->
    forall h q q',
      payload_env_fresh_at delta h ->
      core_parallel (payload_env_olift delta) q q' ->
      exists r,
        star admin_step
          (krepl_e h (installed_let_frame h q) e) r /\
        core_parallel delta r
          (krepl_e h (installed_let_frame h q') e')).
Proof.
  refine (fun delta => core_parallel_mutind
    (fun delta v v' _ => forall h q q',
      payload_env_fresh_at delta h ->
      core_parallel (payload_env_olift delta) q q' ->
      exists r,
        star admin_vstep
          (krepl_v h (installed_let_frame h q) v) r /\
        core_value_parallel delta r
          (krepl_v h (installed_let_frame h q') v'))
    (fun delta e e' _ => forall h q q',
      payload_env_fresh_at delta h ->
      core_parallel (payload_env_olift delta) q q' ->
      exists r,
        star admin_step
          (krepl_e h (installed_let_frame h q) e) r /\
        core_parallel delta r
          (krepl_e h (installed_let_frame h q') e'))
    _ _ _ _ _ _ _ _ _ _ _ _ delta).
  - intros d n h q q' Hfresh Hq.
    exists (VOrd n). split; [apply star_refl | apply CP_VOrd].
  - intros d e e' He IH h q q' Hfresh Hq.
    destruct (IH h (olift_e 1 1 q) (olift_e 1 1 q'))
      as [r [Har Hcore]].
    + apply payload_env_fresh_at_olift. exact Hfresh.
    + pose proof (core_parallel_olift_expr_at Hq 1) as Hql.
      rewrite (payload_env_olift_at_payload_env_olift 0 d) in Hql.
      exact Hql.
    + exists (VLam r). split.
      * cbn [krepl_v]. rewrite !admin_olift_installed_let_frame.
        apply (admin_star_map admin_step admin_vstep VLam); [|exact Har].
        intros x y Hxy. now apply AVS_Lam.
      * cbn [krepl_v]. rewrite !admin_olift_installed_let_frame.
        now apply CP_VLam.
  - intros d v v' Hv IH h q q' Hfresh Hq.
    destruct (IH h q q' Hfresh Hq) as [r [Har Hcore]].
    exists (EVal r). split.
    + apply (admin_star_map admin_vstep admin_step EVal); [|exact Har].
      intros x y Hxy. now apply AS_Val.
    + now apply CP_Val.
  - intros d v v' u u' Hv IHv Hu IHu h q q' Hfresh Hq.
    destruct (IHv h q q' Hfresh Hq) as [r [Hvr Hvr']].
    destruct (IHu h q q' Hfresh Hq) as [s [Hus Hus']].
    exists (EApp r s). split.
    + eapply star_trans.
      * apply (admin_star_map admin_vstep admin_step
          (fun x => EApp x (krepl_v h (installed_let_frame h q) u)));
          [|exact Hvr].
        intros x y Hxy. now apply AS_AppL.
      * apply (admin_star_map admin_vstep admin_step (EApp r)); [|exact Hus].
        intros x y Hxy. now apply AS_AppR.
    + now apply CP_App.
  - intros d a a' t t' Ha IHa Ht IHt h q q' Hfresh Hq.
    destruct (IHa h q q' Hfresh Hq) as [r [Har Har']].
    destruct (IHt h (olift_e 1 1 q) (olift_e 1 1 q'))
      as [s [Hts Hts']].
    + apply payload_env_fresh_at_olift. exact Hfresh.
    + pose proof (core_parallel_olift_expr_at Hq 1) as Hql.
      rewrite (payload_env_olift_at_payload_env_olift 0 d) in Hql.
      exact Hql.
    + exists (ELet r s). split.
      * simpl.
        eapply star_trans.
        -- apply (admin_star_map admin_step admin_step
             (fun x => ELet x
               (krepl_e h (installed_let_frame h (olift_e 1 1 q)) t)));
             [|exact Har].
           intros x y Hxy. now apply AS_LetBinding.
        -- apply (admin_star_map admin_step admin_step (ELet r)); [|exact Hts].
           intros x y Hxy. now apply AS_LetBody.
      * simpl. now apply CP_Let.
  - intros d e e' He IH h q q' Hfresh Hq.
    destruct (IH (S h) (klift_e 0 1 q) (klift_e 0 1 q'))
      as [r [Har Hcore]].
    + now apply payload_env_fresh_at_klift.
    + pose proof (core_parallel_klift_expr Hq) as Hql.
      rewrite payload_env_olift_klift_comm in Hql. exact Hql.
    + exists (EShift r). split.
      * simpl.
        replace (h + 1) with (S h) by lia.
        apply (admin_star_map admin_step admin_step EShift); [|exact Har].
        intros x y Hxy. now apply AS_ShiftBody.
      * simpl.
        replace (h + 1) with (S h) by lia. now apply CP_Shift.
  - intros d k e e' He IH h q q' Hfresh Hq.
    destruct (IH h q q' Hfresh Hq) as [r [Har Hcore]].
    destruct (Nat.eqb k h) eqn:Hkh.
    + apply Nat.eqb_eq in Hkh. subst k.
      exists (ECont h (ELet r q)). split.
      * simpl. rewrite Nat.eqb_refl.
        apply (admin_star_map admin_step admin_step
          (fun x => ECont h (ELet x q))); [|exact Har].
        intros x y Hxy. apply AS_ContBody. now apply AS_LetBinding.
      * simpl. rewrite Nat.eqb_refl. apply CP_Cont. now apply CP_Let.
    + exists (ECont k r). split.
      * simpl. rewrite Hkh.
        apply (admin_star_map admin_step admin_step (ECont k)); [|exact Har].
        intros x y Hxy. now apply AS_ContBody.
      * simpl. rewrite Hkh. now apply CP_Cont.
  - intros d k h q q' Hfresh Hq.
    exists (if Nat.eqb k h then EAsk h else EAsk k).
    destruct (Nat.eqb k h) eqn:Hkh.
    + simpl. rewrite Hkh. split; [apply star_refl | apply CP_AskId].
    + simpl. rewrite Hkh. split; [apply star_refl | apply CP_AskId].
  - intros d k v Hlookup h q q' Hfresh Hq.
    destruct (Nat.eqb k h) eqn:Hkh.
    + apply Nat.eqb_eq in Hkh. subst k. exists (EAsk h). split.
      * simpl. rewrite Nat.eqb_refl. apply star_refl.
      * simpl.
        rewrite (proj1 admin_krepl_no_cocc v h
          (installed_let_frame h q') (Hfresh h v Hlookup)).
        now apply CP_Ask with (v := v).
    + exists (EAsk k). split.
      * simpl. rewrite Hkh. apply star_refl.
      * simpl.
        rewrite (proj1 admin_krepl_no_cocc v h
          (installed_let_frame h q') (Hfresh k v Hlookup)).
        now apply CP_Ask with (v := v).
  - intros d e e' v v' He IHe Hv IHv h q q' Hfresh Hq.
    destruct (IHe h (olift_e 1 1 q) (olift_e 1 1 q'))
      as [r [Her Her']].
    + now apply payload_env_fresh_at_olift.
    + pose proof (core_parallel_olift_expr_at Hq 1) as Hql.
      rewrite (payload_env_olift_at_payload_env_olift 0 d) in Hql.
      exact Hql.
    + destruct (IHv h q q' Hfresh Hq) as [w [Hvw Hvw']].
      exists (EApp (VLam r) w). split.
      * simpl.
        eapply star_trans.
        -- apply (admin_star_map admin_step admin_step
             (fun x => EApp (VLam x)
               (krepl_v h (installed_let_frame h q) v)));
             [|exact Her].
           intros x y Hxy. apply AS_AppL. now apply AVS_Lam.
        -- apply (admin_star_map admin_vstep admin_step
             (fun x => EApp (VLam r) x)); [|exact Hvw].
           intros x y Hxy. now apply AS_AppR.
      * replace (subst_e (subst0 v') e') with (osubst_e 0 v' e')
          by (symmetry; apply omap_single_e).
        rewrite (proj2 krepl_osubst_fusion e' h
          (installed_let_frame h q') 0 v').
        simpl.
        rewrite <- omap_single_e.
        now apply CP_Beta.
  - intros d v v' t t' Hv IHv Ht IHt h q q' Hfresh Hq.
    destruct (IHv h q q' Hfresh Hq) as [w [Hvw Hvw']].
    destruct (IHt h (olift_e 1 1 q) (olift_e 1 1 q'))
      as [r [Htr Htr']].
    + now apply payload_env_fresh_at_olift.
    + pose proof (core_parallel_olift_expr_at Hq 1) as Hql.
      rewrite (payload_env_olift_at_payload_env_olift 0 d) in Hql.
      exact Hql.
    + exists (ELet (EVal w) r). split.
      * simpl.
        eapply star_trans.
        -- apply (admin_star_map admin_vstep admin_step
             (fun x => ELet (EVal x)
               (krepl_e h (installed_let_frame h (olift_e 1 1 q)) t)));
             [|exact Hvw].
           intros x y Hxy. apply AS_LetBinding. now apply AS_Val.
        -- apply (admin_star_map admin_step admin_step
             (ELet (EVal w))); [|exact Htr].
           intros x y Hxy. now apply AS_LetBody.
      * replace (subst_e (subst0 v') t') with (osubst_e 0 v' t')
          by (symmetry; apply omap_single_e).
        rewrite (proj2 krepl_osubst_fusion t' h
          (installed_let_frame h q') 0 v').
        simpl.
        rewrite <- omap_single_e.
        now apply CP_LetValue.
  - intros d k e e' He IH h q q' Hfresh Hq.
    destruct (IH (S h) (klift_e 0 1 q) (klift_e 0 1 q'))
      as [r [Har Hcore]].
    + now apply payload_env_fresh_at_klift.
    + pose proof (core_parallel_klift_expr Hq) as Hql.
      rewrite payload_env_olift_klift_comm in Hql. exact Hql.
    + assert (Hframe :
          klift_d 0 1 (installed_let_frame h q) =
          installed_let_frame (S h) (klift_e 0 1 q)).
      { rewrite admin_klift_installed_let_frame.
        replace (h + 1) with (S h) by lia. reflexivity. }
      assert (Hframe' :
          klift_d 0 1 (installed_let_frame h q') =
          installed_let_frame (S h) (klift_e 0 1 q')).
      { rewrite admin_klift_installed_let_frame.
        replace (h + 1) with (S h) by lia. reflexivity. }
      rewrite <- Hframe in Har. rewrite <- Hframe' in Hcore.
      eapply Hcontshift with (r := r); eassumption.
Qed.

Lemma core_repl_frame_maps_parallel delta h q q' :
  core_parallel (payload_env_olift delta) q q' ->
  core_cmap_parallel delta
    (repl_cmap h (installed_let_frame h q))
    (repl_cmap h (installed_let_frame h q')).
Proof.
  intros Hq k. unfold repl_cmap.
  destruct (Nat.eqb k h) eqn:Hkh.
  - apply Nat.eqb_eq in Hkh. subst k.
    apply CIP_Cont. apply CEP_Let; [apply CEP_Hole | exact Hq].
  - apply CIP_Cont. apply CEP_Hole.
Qed.

Lemma cmap_repl_frame_payload_coherent delta h q :
  payload_env_fresh_at delta h ->
  cmap_payload_coherent delta delta
    (repl_cmap h (installed_let_frame h q)).
Proof.
  intros Hfresh k v Hlookup.
  assert (Haction :
      cmap_v (repl_cmap h (installed_let_frame h q)) v = v).
  { rewrite cmap_repl_v.
    apply (proj1 admin_krepl_no_cocc). exact (Hfresh k v Hlookup). }
  rewrite Haction.
  unfold repl_cmap. destruct (Nat.eqb k h) eqn:Hkh; simpl.
  - apply Nat.eqb_eq in Hkh. subst k.
    exact Hlookup.
  - exact Hlookup.
Qed.

(** The remaining same-head residual.  Its hypotheses already contain the
    recursively postponed shift body; what remains is the
    let.S/dL.S/AbortD critical calculation at the frame head.

    A second application of one-frame postponement is needed here: [let.S]
    installs a frame for the freshly bound continuation [0], while the body
    is already mapped at [S h].  Thus the genuinely induction-closed
    formulation is simultaneous continuation-map postponement, with the
    map updated by composition in the [CP_ContShift] case.  The singleton
    replacement theorem above is then its [repl_cmap] corollary. *)
Lemma core_parallel_frame_contshift_hit
    (delta : payload_env) (h : nat) (q q' e e' r : expr) :
  payload_env_fresh_at delta h ->
  core_parallel (payload_env_olift delta) q q' ->
  core_parallel (payload_env_klift delta) e e' ->
  star admin_step
    (krepl_e (S h)
      (klift_d 0 1 (installed_let_frame h q)) e) r ->
  core_parallel (payload_env_klift delta) r
    (krepl_e (S h)
      (klift_d 0 1 (installed_let_frame h q')) e') ->
  exists z,
    star admin_step
      (krepl_e h (installed_let_frame h q)
        (ECont h (EShift e))) z /\
    core_parallel delta z
      (krepl_e h (installed_let_frame h q')
        (ksubst_e 0 (ICont h CHole) e')).
Proof.
  intros Hfresh Hq He _ _.
  pose proof (@CP_ContShift delta h e e' He) as Hroot.
  destruct ((proj2 (core_parallel_cmap_postponement delta))
      (ECont h (EShift e))
      (ksubst_e 0 (ICont h CHole) e') Hroot delta
      (repl_cmap h (installed_let_frame h q))
      (repl_cmap h (installed_let_frame h q'))
      (core_repl_frame_maps_parallel delta h q q' Hq)
      (cmap_repl_frame_payload_coherent delta h q' Hfresh))
    as [z [Haz Hcore]].
  exists z. rewrite !cmap_repl_e in Haz, Hcore.
  exact (conj Haz Hcore).
Qed.

Lemma core_parallel_frame_contshift_residual
    (delta : payload_env) (h : nat) (q q' : expr)
    (k : nat) (e e' r : expr) :
  payload_env_fresh_at delta h ->
  core_parallel (payload_env_olift delta) q q' ->
  core_parallel (payload_env_klift delta) e e' ->
  star admin_step
    (krepl_e (S h)
      (klift_d 0 1 (installed_let_frame h q)) e) r ->
  core_parallel (payload_env_klift delta) r
    (krepl_e (S h)
      (klift_d 0 1 (installed_let_frame h q')) e') ->
  exists z,
    star admin_step
      (krepl_e h (installed_let_frame h q)
        (ECont k (EShift e))) z /\
    core_parallel delta z
      (krepl_e h (installed_let_frame h q')
        (ksubst_e 0 (ICont k CHole) e')).
Proof.
  intros Hfresh Hq He Har Hcore.
  destruct (Nat.eqb k h) eqn:Hkh.
  - apply Nat.eqb_eq in Hkh. subst k.
    eapply core_parallel_frame_contshift_hit; eassumption.
  - exists (ECont k (EShift r)). split.
    + simpl. rewrite Hkh.
      apply (admin_star_map admin_step admin_step
        (fun x => ECont k (EShift x))).
      * intros x y Hxy. apply AS_ContBody. now apply AS_ShiftBody.
      * exact Har.
    + simpl.
      pose proof (proj2 admin_ksubst_krepl_frame_nonhit
        e' 0 h k q' ltac:(intro Heq; subst k;
          rewrite Nat.eqb_refl in Hkh; discriminate)) as Hfusion.
      replace (k + 0) with k in Hfusion by lia.
      replace (h + 0) with h in Hfusion by lia.
      replace (S (h + 0)) with (S h) in Hfusion by lia.
      rewrite admin_klift_zero_d in Hfusion.
      rewrite <- Hfusion.
      now apply CP_ContShift.
Qed.

Lemma core_parallel_frame_postponement
    (delta : payload_env) (e e' t t' : expr) :
  core_parallel (payload_env_klift delta) e e' ->
  core_parallel (payload_env_olift delta) t t' ->
  exists r,
    star admin_step
      (EShift (krepl_e 0 (frame t) e)) r /\
    core_parallel delta r
      (EShift (krepl_e 0 (frame t') e')).
Proof.
  intros He Ht.
  assert (Hqt : core_parallel
      (payload_env_olift (payload_env_klift delta))
      (klift_e 0 1 t) (klift_e 0 1 t')).
  { pose proof (core_parallel_klift_expr Ht) as Hlift.
    rewrite payload_env_olift_klift_comm in Hlift. exact Hlift. }
  destruct ((proj2
      (core_parallel_frame_postponement_from_contshift
        core_parallel_frame_contshift_residual
        (payload_env_klift delta)))
      e e' He 0 (klift_e 0 1 t) (klift_e 0 1 t')
      (payload_env_klift_fresh_zero delta) Hqt)
    as [r [Har Hcore]].
  exists (EShift r). split.
  - change (star admin_step
      (EShift
        (krepl_e 0
          (installed_let_frame 0 (klift_e 0 1 t)) e))
      (EShift r)).
    apply (admin_star_map admin_step admin_step EShift).
    + intros x y Hxy. now apply AS_ShiftBody.
    + exact Har.
  - change (core_parallel delta (EShift r)
      (EShift
        (krepl_e 0
          (installed_let_frame 0 (klift_e 0 1 t')) e'))).
    now apply CP_Shift.
Qed.

Lemma core_parallel_let_shift_decreasing_residual
    (delta : payload_env) (e p t t' : expr) :
  core_parallel delta (EShift e) p ->
  core_parallel (payload_env_olift delta) t t' ->
  exists r b,
    star admin_step (ELet p t') b /\
    star admin_step
      (EShift (krepl_e 0 (frame t) e)) r /\
    core_parallel delta r b.
Proof.
  intros Hp Ht. inversion Hp; subst.
  match goal with
  | Hbody : core_parallel ?d e ?q |- _ =>
      destruct (@core_parallel_frame_postponement delta e q t t'
        Hbody Ht)
        as [r [Har Hcore]];
      exists r, (EShift (krepl_e 0 (frame t') q));
      split; [|split]
  end.
  - apply star_one. apply AS_LetShift.
  - exact Har.
  - exact Hcore.
Qed.

(** Small closure facts for doing the tail-spine induction before reinstalling
    the surrounding continuation. *)
Lemma delimited_star_let_body k z e e' :
  star (delimited_step k) e e' ->
  star (delimited_step k) (ELet z e) (ELet z e').
Proof.
  apply (admin_star_map (delimited_step k) (delimited_step k) (ELet z)).
  intros x y [Hadmin | Htail].
  - left. apply AS_LetBody. exact Hadmin.
  - right. apply TS_LetBody. exact Htail.
Qed.

Lemma admin_star_is_delimited k e e' :
  star admin_step e e' -> star (delimited_step k) e e'.
Proof.
  apply (admin_star_map admin_step (delimited_step k) (fun x => x)).
  intros x y H. left. exact H.
Qed.

Lemma delimited_star_osubst k e e' :
  star (delimited_step k) e e' -> forall cut v,
  star (delimited_step k)
    (osubst_e cut v e) (osubst_e cut v e').
Proof.
  intro H. induction H as [x | x y z Hxy Hyz IH]; intros cut v.
  - apply star_refl.
  - eapply star_trans.
    + destruct Hxy as [Hadmin | Htail].
      * apply admin_star_is_delimited.
        exact (admin_osubst_star x y (star_one Hadmin) cut v).
      * apply star_one. right. apply tail_step_osubst. exact Htail.
    + exact (IH cut v).
Qed.

Corollary delimited_star_subst0 k v e e' :
  star (delimited_step k) e e' ->
  star (delimited_step k)
    (subst_e (subst0 v) e) (subst_e (subst0 v) e').
Proof.
  intro H. unfold subst0. rewrite !subst_single_e.
  exact (delimited_star_osubst k e e' H 0 v).
Qed.

(** The cut-zero instance used by both empty-spine tail residuals. *)
Lemma core_parallel_ksubst0 delta e e' k :
  core_parallel (payload_env_klift delta) e e' ->
  core_parallel delta
    (ksubst_e 0 (ICont k CHole) e)
    (ksubst_e 0 (ICont k CHole) e').
Proof.
  intro H.
  eapply (@core_parallel_ksubst_factor_expr
    (payload_env_klift delta) e e' H 0 delta k).
  rewrite payload_env_klift_at_0. reflexivity.
Qed.

Lemma core_parallel_shift_abort_cont_cong
    (delta : payload_env) (k : nat) (q q' : expr) :
  core_parallel (payload_env_klift delta) (klift_e 0 1 q) q' ->
  exists r b,
    star (delimited_step k) (EShift (ECont (S k) q')) b /\
    star (delimited_step k) q r /\
    core_parallel delta r b.
Proof.
  intro Hinner.
  pose proof (core_parallel_ksubst0 delta
    (klift_e 0 1 q) q' k Hinner) as Hsub.
  rewrite ksubst_klift_cancel_e0 in Hsub.
  exists q, (ksubst_e 0 (ICont k CHole) q').
  split; [|split].
  - eapply star_trans.
    + destruct (cocc_e 0 (ECont (S k) q')) eqn:Hocc'.
      * apply star_one. right. apply TS_Shift. exact Hocc'.
      * rewrite (admin_abort_ksubst_no_cocc k
          (ECont (S k) q') Hocc').
        apply star_refl.
    + apply star_one. right. apply TS_Abort.
  - apply star_refl.
  - exact Hsub.
Qed.

(** The only nested root overlap in the empty-spine AbortD case: while the
    administrative arm removes the abort, the parallel arm contracts the
    [k.S] occurring inside the lifted abort. *)
Lemma core_parallel_shift_abort_contshift
    (delta : payload_env) (k : nat) (q u u' : expr) :
  klift_e 0 1 q = EShift u ->
  core_parallel (payload_env_klift (payload_env_klift delta)) u u' ->
  exists r b,
    star (delimited_step k)
      (EShift (ksubst_e 0 (ICont (S k) CHole) u')) b /\
    star (delimited_step k) q r /\
    core_parallel delta r b.
Proof.
  intros Heq Hinner.
  destruct q as [v | v w | a t | body | j body | j];
    simpl in Heq; try discriminate.
  inversion Heq; subst u.
  pose proof (core_parallel_ksubst0
    (payload_env_klift delta)
    (klift_e 1 1 body) u' (S k) Hinner) as Hsub.
  assert (Hcross :
      ksubst_e 0 (ICont (S k) CHole) (klift_e 1 1 body) =
      klift_e 0 1 (ksubst_e 0 (ICont k CHole) body)).
  { symmetry.
    pose proof (fs_klift_ksubst_e 0 k body) as H.
    simpl in H. replace (k + 1) with (S k) in H by lia. exact H. }
  rewrite Hcross in Hsub.
  exists (abort (ksubst_e 0 (ICont k CHole) body)),
    (EShift (ksubst_e 0 (ICont (S k) CHole) u')).
  split; [|split].
  - apply star_refl.
  - destruct (cocc_e 0 body) eqn:Hocc.
    + apply star_one. right. apply TS_Shift. exact Hocc.
    + rewrite (admin_abort_ksubst_no_cocc k body Hocc).
      apply star_refl.
  - unfold abort. apply CP_Shift. exact Hsub.
Qed.

(** Only the empty-spine tail source remains semantic.  The theorem below
    proves that every surrounding right-let spine is structural. *)
Lemma core_parallel_shift_tail_decreasing_residual
    (delta : payload_env) (k : nat) (e p a : expr) :
  core_parallel delta (EShift e) p ->
  tail_step k (EShift e) a ->
  exists r b,
    star (delimited_step k) p b /\
    star (delimited_step k) a r /\
    core_parallel delta r b.
Proof.
  intros Hp Htail. inversion Hp; subst.
  match goal with
  | Hbody : core_parallel ?d e ?e' |- _ =>
      destruct (tail_step_shape k (EShift e) a Htail)
        as [[l [q [Hx [Ha Hocc]]]] | [l [q [Hx Ha]]]]
  end.
  - destruct l as [|z l]; simpl in Hx; [|discriminate].
    inversion Hx; subst q. simpl in Ha. subst a.
    match goal with
    | Hbody : core_parallel (payload_env_klift delta) e ?e' |- _ =>
        pose proof (core_parallel_ksubst0 delta e e' k Hbody) as Hsub;
        pose proof (@core_parallel_klift_expr delta
          (ksubst_e 0 (ICont k CHole) e)
          (ksubst_e 0 (ICont k CHole) e') Hsub) as Hlift;
        exists (abort (ksubst_e 0 (ICont k CHole) e)),
          (abort (ksubst_e 0 (ICont k CHole) e'));
        split; [|split]
    end.
    + destruct (cocc_e 0 e') eqn:Hocc'.
      * apply star_one. right. apply TS_Shift. exact Hocc'.
      * rewrite (admin_abort_ksubst_no_cocc k e' Hocc').
        apply star_refl.
    + apply star_refl.
    + unfold abort. apply CP_Shift. exact Hlift.
  - destruct l as [|z l]; simpl in Hx; [|discriminate].
    unfold abort in Hx. inversion Hx; subst e. simpl in Ha. subst a.
    replace (k + 1) with (S k) in * by lia.
    match goal with
    | Hbody : core_parallel (payload_env_klift delta)
        (ECont (S k) (klift_e 0 1 q)) ?e' |- _ =>
        inversion Hbody; subst
    end.
    + match goal with
      | Hinner : core_parallel ?d (klift_e 0 1 q) ?q' |- _ =>
          exact (@core_parallel_shift_abort_cont_cong delta k q q' Hinner)
      end.
    + match goal with
      | Heq : EShift ?u = klift_e 0 1 q,
        Hinner : core_parallel
          (payload_env_klift (payload_env_klift delta)) ?u ?u' |- _ =>
          symmetry in Heq;
          exact (@core_parallel_shift_abort_contshift
            delta k q u u' Heq Hinner)
      end.
Qed.

Lemma core_parallel_tail_decreasing_from_shift :
  forall k e a,
  tail_step k e a -> forall delta p,
  core_parallel delta e p ->
  exists r b,
    star (delimited_step k) p b /\
    star (delimited_step k) a r /\
    core_parallel delta r b.
Proof.
  intros k e a Htail.
  induction Htail as [k z e a Htail IH | k e Hocc | k e];
    intros delta p Hp.
  - inversion Hp; subst.
    + match goal with
      | Hbody : core_parallel (payload_env_olift delta) e ?pbody,
        Hbinding : core_parallel delta z ?pbinding |- _ =>
          destruct (IH (payload_env_olift delta) pbody Hbody)
            as [r [b [Hpb [Har Hcore]]]];
          exists (ELet z r), (ELet pbinding b);
          split; [|split]
      end.
      * apply delimited_star_let_body. exact Hpb.
      * apply delimited_star_let_body. exact Har.
      * apply CP_Let; assumption.
    + match goal with
      | Hbody : core_parallel (payload_env_olift delta) e ?pbody,
        Hvalue : core_value_parallel delta ?v ?pv |- _ =>
          destruct (IH (payload_env_olift delta) pbody Hbody)
            as [r [b [Hpb [Har Hcore]]]];
          exists (ELet (EVal v) r), (subst_e (subst0 pv) b);
          split; [|split]
      end.
      * apply delimited_star_subst0. exact Hpb.
      * apply delimited_star_let_body. exact Har.
      * apply CP_LetValue; assumption.
  - apply (@core_parallel_shift_tail_decreasing_residual delta k e p
      (abort (ksubst_e 0 (ICont k CHole) e))).
    + exact Hp.
    + apply TS_Shift. exact Hocc.
  - apply (@core_parallel_shift_tail_decreasing_residual delta k
      (klift_e 0 1 (ECont k e)) p e).
    + exact Hp.
    + apply TS_Abort.
Qed.

Lemma core_parallel_cont_tail_decreasing_residual
    (delta : payload_env) (k : nat) (e p a : expr) :
  core_parallel delta e p ->
  tail_step k e a ->
  exists r b,
    star admin_step (ECont k p) b /\
    star admin_step (ECont k a) r /\
    core_parallel delta r b.
Proof.
  intros Hp Htail.
  destruct (@core_parallel_tail_decreasing_from_shift
      k e a Htail delta p Hp)
    as [r [b [Hpb [Har Hcore]]]].
  exists (ECont k r), (ECont k b); split; [|split].
  - apply admin_tail_star_lift. exact Hpb.
  - apply admin_tail_star_lift. exact Har.
  - apply CP_Cont. exact Hcore.
Qed.

Lemma core_parallel_cont_shift_tail_decreasing_residual
    (delta : payload_env) (k : nat) (e p a : expr) :
  core_parallel (payload_env_klift delta) e p ->
  tail_step k (EShift e) a ->
  exists r b,
    star admin_step
      (ksubst_e 0 (ICont k CHole) p) b /\
    star admin_step (ECont k a) r /\
    core_parallel delta r b.
Proof.
  intros Hp Htail.
  destruct (tail_step_shape k (EShift e) a Htail)
    as [[l [q [Hx [Ha Hocc]]]] | [l [q [Hx Ha]]]].
  - destruct l as [|z l]; simpl in Hx; [|discriminate].
    inversion Hx; subst q. simpl in Ha. subst a.
    assert (Henv : payload_env_klift delta =
        payload_env_klift_at 0 delta).
    { rewrite payload_env_klift_at_0. reflexivity. }
    assert (Hsub : core_parallel delta
        (ksubst_e 0 (ICont k CHole) e)
        (ksubst_e 0 (ICont k CHole) p)).
    { exact (@core_parallel_ksubst_factor_expr
        (payload_env_klift delta) e p Hp 0 delta k Henv). }
    pose proof (@core_parallel_klift_expr delta
      (ksubst_e 0 (ICont k CHole) e)
      (ksubst_e 0 (ICont k CHole) p) Hsub) as Hlift.
    exists
      (ECont k
        (abort (ksubst_e 0 (ICont k CHole) e))),
      (ksubst_e 0 (ICont k CHole) p).
    split; [apply star_refl | split; [apply star_refl |]].
    unfold abort.
    rewrite <- (ksubst_klift_cancel_e0 (ICont k CHole)
      (ksubst_e 0 (ICont k CHole) p)).
    apply CP_ContShift.
    exact Hlift.
  - destruct l as [|z l]; simpl in Hx; [|discriminate].
    unfold abort in Hx. inversion Hx; subst e. simpl in Ha. subst a.
    assert (Henv : payload_env_klift delta =
        payload_env_klift_at 0 delta).
    { rewrite payload_env_klift_at_0. reflexivity. }
    assert (Hsub : core_parallel delta
        (ksubst_e 0 (ICont k CHole) (klift_e 0 1 (ECont k q)))
        (ksubst_e 0 (ICont k CHole) p)).
    { exact (@core_parallel_ksubst_factor_expr
        (payload_env_klift delta)
        (klift_e 0 1 (ECont k q)) p Hp 0 delta k Henv). }
    rewrite ksubst_klift_cancel_e0 in Hsub.
    exists (ECont k q), (ksubst_e 0 (ICont k CHole) p).
    split; [apply star_refl | split; [apply star_refl | exact Hsub]].
Qed.

Theorem core_parallel_admin_decreasing :
  forall delta,
  (forall v p,
      core_value_parallel delta v p ->
      forall a, admin_vstep v a ->
      exists r b,
        star admin_vstep p b /\
        star admin_vstep a r /\
        core_value_parallel delta r b) /\
  (forall e p,
      core_parallel delta e p ->
      forall a, admin_step e a ->
      exists r b,
        star admin_step p b /\
        star admin_step a r /\
        core_parallel delta r b).
Proof.
  apply core_admin_decreasing_from_residuals.
  - exact core_parallel_let_shift_decreasing_residual.
  - exact core_parallel_let_assoc_decreasing_residual.
  - exact core_parallel_cont_tail_decreasing_residual.
  - exact core_parallel_cont_shift_tail_decreasing_residual.
Qed.