Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsSepAlg GpsModel GpsModelLemmas.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.

Local Open Scope string_scope.

Set Implicit Arguments.

Lemma incoming_upd_ext_esc :
  ∀ acts (ND: NoDup acts) a (IN: In a acts) L b rr,
    incoming acts (upd L (Tesc a b) (rr +!+ L (Tesc a b))) b =
    rr +!+ incoming acts L b.
Proof.
  ins; rewrite !(res_plusC rr); unfold incoming, in_sb, in_rf.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  rewrite !res_plusA; do 2 f_equal.
  unfold in_esc.
  eapply In_NoDup_Permutation in IN; desf.
  rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ IN)));
    simpl; rewrite upds.
  rewrite map_upd_irr, !res_plusA; f_equal; eauto using res_plusC.
  rewrite in_map_iff; intro; desf.
Qed.

Lemma label_restr_fin acts amap sb rf mo sc L E :
  Consistent acts amap sb rf mo sc →
  label_restr acts amap sb rf L E →
  ∃ tel, ∀ te (NIN: ¬ In te tel), L te = res_emp.
Proof.
  ins.
  ∃
    (flatten (map (fun a ⇒ map (Tsb a) acts) acts) ++
     flatten (map (fun a ⇒ map (Trf a) acts) acts) ++
     flatten (map (fun a ⇒ map (Tesc a) acts) acts) ++
     map TsbS acts ++ map TrfS acts ++ flatten (map (fun s ⇒ map (TescS s) acts) E)).
  ins.
  rewrite !in_app_iff, !in_flatten_iff, !in_map_iff in ×.
  repeat match goal with
           H : ¬ (_ ∨ _) |- _ ⇒ apply not_or_and in H; desc
         end.
  destruct te; ins; apply H0; try apply not_and_or; intro; desc; eauto 6 using in_map;
  exploit Consistent_hb_in; eauto; try intro; desf; eauto 8 using in_map.
Qed.

Lemma res_gget_max_list l :
  ∃ n, ∀ n' (LT: n < n') r , In r l → res_gget r n' = None.
Proof.
  induction l; ins; desf; [by ∃ 0|].
  destruct a as [|p [f [n' C]] e].
    by ∃ n; ins; desf; eauto.
  ∃ (n + n'); ins; desf; ins; eauto with arith.
Qed.

Lemma outgoing_upd_sbS b acts L E r a :
  outgoing acts (upd L (TsbS b) (L (TsbS b) +!+ r)) E a =
  if a == b then r +!+ outgoing acts L E a else outgoing acts L E a.
Proof.
  unfold outgoing, out_sb, out_rf, out_esc; ins.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  by unfold upd; desf; ins; desf; rewrite !res_plusA, res_plusAC.
Qed.

Lemma RP_extC (P : RProp) r (H : P r) r' (D: r' +!+ r ≠ Rundef) : P (r' +!+ r).
Proof.
  rewrite res_plusC in *; eapply RP_ext; eauto.
Qed.

Lemma hb_irr :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) a
    (HB: happens_before amap sb rf a a),
    False.
Proof.
  unfold Consistent; ins; desf.
  eapply (ACYC a); revert HB; generalize a at 1 3; induction 1; vauto.
  unfold imm_happens_before, synchronizes_with in *; desf; eauto using clos_trans.
Qed.

Lemma compat_inc_sink :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a b,
  a = b ∨
  happens_before amap sb rf a b ∨
  happens_before amap sb rf b a ∨
  L (TsbS b) +!+ incoming acts L a ≠ Rundef.
Proof.
  ins.
  apply NNPP; intro X.
  apply not_or_and in X; desf.
  apply not_or_and in X0; desf.
  apply not_or_and in X1; desf.
  apply NNPP in X2.
  apply (CC (TsbS b :: map (Tsb^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts)
                     ++ map (Trf^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts)
                     ++ map (Tesc^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts))).
    constructor; [by rewrite !in_app_iff, !in_map_iff; intro; desf|].
    rewrite !nodup_app; repeat apply conj;
    try eapply nodup_map; try eapply nodup_filter; ins; try congruence;
    by unfold disjoint; intro; rewrite ?in_app_iff, !in_map_iff; ins; desf.

    by ins; rewrite !in_app_iff, !in_map_iff in *; desf; rewrite in_filter_iff in *; ins; desf;
       rewrite mhbE in *; desf; unfold mydecf in *; desf; eapply hb_irr; eauto using hb_trans.

  ins; rewrite !map_app, !rsum_app, !rsum_map_map_filter; ins; apply LR; eauto.
Qed.

Lemma replace_edge_ext :
  ∀ A (a : A) f pi l
    (ND: NoDup l)
    (IN : In a l),
  rsum (map (upd f a (f a +!+ pi)) l) = pi +!+ rsum (map f l).
Proof.
  ins; induction ND; ins.
  desf; rewrite ?upds, ?updo; try congruence.
    by rewrite res_plusA, res_plusAC, map_upd_irr.
  by rewrite IHND, res_plusAC.
Qed.

Lemma sat_exch_ext :
  ∀ IE sigma r (M : sat_exch IE sigma r)
         r' (D : r +!+ r' ≠ Rundef),
  sat_exch IE sigma (r +!+ r').
Proof.
  red; ins; edestruct M; eauto using RP_ext.
Qed.

Lemma exch_conform_ext1 IE acts amap sb rf L te r L' EE sigma
  (ECO : exch_conform IE acts amap sb rf (upd L te r) L' EE sigma)
  (NEQ: ∀ a, te ≠ TescS sigma a) r'
  (IMP : res_escr (r +!+ r') sigma → res_escr r sigma) :
  exch_conform IE acts amap sb rf (upd L te (r +!+ r')) L' EE sigma.
Proof.
  red; ins; unfold upd in *; desf.
    edestruct (ECO te) as (a & M); ins; eauto.
      by desf; auto.
    ∃ a; split; ins; desc; des_if; ins.
    by eapply sat_exch_ext; eauto; intro X; rewrite X in ESC.
  edestruct (ECO edge) as (a & M); ins; eauto.
    by desf; auto.
  ∃ a; desf; eauto; congruence.
Qed.

Lemma in_esc_upd_in :
  ∀ acts L a b r1 r,
    In a acts →
    NoDup acts →
    L (Tesc a b) = r1 →
    in_esc acts (upd L (Tesc a b) (r +!+ r1)) b =
    in_esc acts L b +!+ r.
Proof.
  ins; unfold in_esc; eapply in_split in H; desf;
  rewrite !map_app, !rsum_app; ins.
  rewrite nodup_app, nodup_cons in *; desf.
  unfold disjoint in *; ins.
  rupd; rewrite !map_upd_irr, !res_plusA; rewrite ?in_map_iff;
    try intro; desf; eauto.
  by rewrite (res_plusC _ r), !(res_plusAC r).
Qed.

Lemma hb_mhb amap sb rf a b :
  happens_before amap sb rf a b →
  may_happens_before amap sb rf a b.
Proof.
  rewrite mhbE; auto.
Qed.

Lemma ghost_allocE r mm :
  ghost_alloc r mm ↔ r = Rundef ∨ res_gget r mm ≠ None.
Proof.
  destruct r; ins; desf; split; ins; try tauto; desf.
Qed.

Lemma ghost_alloc_conform_helper2 :
  ∀ acts L EE (ND: NoDup EE) r r' a
         (GAC: ghost_alloc_conform acts (upd L (TsbS a) (L (TsbS a) +!+ r)) EE)
         (IMP: ∀ gl (GA: ghost_alloc r' gl)
                 a' (NEQ: a ≠ a') (GA': ghost_alloc (outgoing acts L EE a') gl),
                 False)
         (DEF: outgoing acts (upd L (TsbS a) (L (TsbS a) +!+ r +!+ r')) EE a ≠ Rundef),
    ghost_alloc_conform acts (upd L (TsbS a) (L (TsbS a) +!+ r +!+ r')) EE.
Proof.
  red; ins; destruct (eqP a0 a'); ins.
  eapply GAC with (gl:=gl); ins;
    rewrite ?incoming_upd_irr in *; ins.

  destruct (eqP a a0); desf.
    rewrite outgoing_upd_in in DEF, OUT; ins; rewrite outgoing_upd_in; ins;
    rewrite outgoing_upd_irr in OUT'; ins; eauto.
    rewrite <- res_plusA in ×.
    unfold ghost_alloc; desf; ins; desf; ins; intro; eauto.
    eapply IMP; eauto;
    unfold gres_plus in *; des_eqrefl; desf; ins; clear DEF; inv_lplus gl;
    destruct (gres gl); ins; desf; congruence.
  by rewrite outgoing_upd_irr in OUT; try rewrite outgoing_upd_irr; ins.

  destruct (eqP a a'); desf.
    rewrite outgoing_upd_in in DEF, OUT'; ins; rewrite outgoing_upd_in; ins;
    rewrite outgoing_upd_irr in OUT; ins; eauto.
    rewrite <- res_plusA in ×.
    unfold ghost_alloc; desf; ins; desf; ins; intro; eauto.
    clear DEF.
    eapply IMP with (a'0 := a0); eauto.
    unfold gres_plus in *; des_eqrefl; desf; ins; inv_lplus gl.
    destruct (gres gl); ins; desf; congruence.
  by rewrite outgoing_upd_irr in OUT'; try rewrite outgoing_upd_irr; ins.
Qed.

Lemma outgoing_ee :
  ∀ acts amap sb rf L EE
    (LR : label_restr acts amap sb rf L EE) sigma a,
    outgoing acts L
         (if excluded_middle_informative (In sigma EE)
          then EE
          else sigma :: EE) a =
    outgoing acts L EE a.
Proof.
  unfold outgoing, out_esc; ins; desf; ins; do 3 f_equal.
  red in LR; desc; rewrite LRescS; auto using res_plus_emp_l.
Qed.

Lemma valid_ghost_gget :
  ∀ r r' (VG : valid_ghost r r') r0
         (BAR: ∀ m gr, res_gget r0 m = Some gr →
                            res_gget r m = None →
                            res_gget r' m = None) r''
         (IDEF : r +!+ r0 +!+ r'' ≠ Rundef)
         (ODEF : r' +!+ r0 ≠ Rundef)
         (OUD : r' +!+ r0 +!+ r'' = Rundef),
   ∃ gl : nat,
     res_gget r'' gl ≠ None ∧
     res_gget (r +!+ r0) gl = None ∧
     res_gget (r' +!+ r0) gl ≠ None.
Proof.
  ins; rewrite <- res_plusA in *; red in VG; desf; ins; desf; ins; desf.
  clear ODEF IDEF; rewrite gres_plusC in *; unfold gres_plus in *; repeat des_eqrefl; desf; ins.
  clear p p1 pmap pmap0 p0 Heq Heq2 escr1 escr escr0 escr'.
  symmetry in EQ; apply lift_plus_noneD in EQ; destruct EQ as [l M].
  inv_lplus l; ∃ l; specialize (VGG l); specialize (BAR l).
  remember (o l) as oo; clear Heqoo.
  remember (o1 l) as oo1; clear Heqoo1.
  remember (o0 l) as oo0; clear Heqoo0.
  destruct (gres l), (gres0 l); ins; desf; try specialize (VGG _ eq_refl); desf.
  × exfalso; destruct s; ins; desf; rewrite <- eq_rect_eq in *; ins.
    destruct s0; ins; desf; rewrite <- eq_rect_eq in *; ins.
    by rewrite salg_plusC in *;
       assert (K := salg_plusA _ _ _ Heq5 _ Heq4); desc;
       eapply salg_plusA2 in Heq; eauto; desf;
      eapply VGG0 in Heq; desf.
  × exfalso; clear VGG; exploit BAR; desf.
  × exfalso; destruct s; ins; desf; rewrite <- eq_rect_eq in *; ins; desf.
    rewrite salg_plusC in *; apply VGG0 in Heq0; desf.
Qed.

Lemma exch_conform_upd1_acc IE acts amap sb rf L L' EE sigma te2 r
  (ECO : exch_conform IE acts amap sb rf (upd L te2 r) L' EE sigma) te1 r1
  (N1: ∀ a, te1 = TescS sigma a → sat_exch IE sigma r1) r2
  (N2: ∀ a, te2 = TescS sigma a → sat_exch IE sigma r2)
  (SRC: te_src te1 = te_src te2)
  (T1: te_tgt te1 = None)
  (T2: te_tgt te2 = None)
  (NEQ: te1 ≠ te2)
  (DEF: r1 +!+ r2 ≠ Rundef)
  (EQ: r1 +!+ r2 = L te1 +!+ r) :
  exch_conform IE acts amap sb rf (upd (upd L te1 r1) te2 r2) L' EE sigma.
Proof.
  red; ins; unfold upd in *; desf.
    exploit (proj2 (res_escr_plus _ _ DEF sigma)); vauto.
    rewrite EQ in *; rewrite res_escr_plus; intro K; desf.
      edestruct (ECO te1) as (a & M); ins; try (by desf).
      des_if; ins; try congruence; ∃ a; des_if;
      desc; ins; clarify; split; eauto; try congruence.
    edestruct (ECO te2) as (a & M); ins; try (by desf).
    des_if; ins; try congruence; ∃ a; des_if;
    desc; ins; clarify; split; eauto; try congruence.

    exploit (proj2 (res_escr_plus _ _ DEF sigma)); vauto.
    rewrite EQ in *; rewrite res_escr_plus; intro K; desf.
      edestruct (ECO te1) as (a & M); ins; try (by desf).
      des_if; ins; try congruence; ∃ a; des_if;
      desc; ins; clarify; split; eauto; try congruence.
    edestruct (ECO te2) as (a & M); ins; try (by desf).
    des_if; ins; try congruence; ∃ a; des_if;
    desc; ins; clarify; split; eauto; try congruence.

  edestruct (ECO edge) as (a & M); ins; try (by desf).
  des_if; ins; try congruence; ∃ a; des_if;
  desc; ins; clarify; split; eauto; try congruence.
Qed.

Lemma visible_ghost_one :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (LR: label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) N
    (PC: prefix_closed sb rf N) te
    (IN : In (te_src te) N) gl
    (G : res_gget (L te) gl ≠ None)
    (ND: NoDup acts) (NDE: NoDup E),
  ∃ a,
    << HB : may_happens_before amap sb rf a (te_src te) >> ∧
    << INC : res_gget (incoming acts L a) gl = None >> ∧
    << OUT : res_gget (outgoing acts L E a) gl ≠ None >> ∧
    << INA : In a acts >>.
Proof.
  ins.
  revert G; pattern te.
  eapply edge_depth_ind with (lab:=amap) (V:=N); eauto.
    by red in CONS; desc; intros ? ?; edestruct ACYC; eauto.
  clear te IN; ins; desf; unfold NW.
  assert (∀ sigma a, edge = TescS sigma a → In sigma E).
    by ins; apply NNPP; intro; desf; red in LR; ins; desf; rewrite LRescS in G; ins; vauto.
  assert (∀ a, te_tgt edge = Some a → In a acts).
    by ins; eapply lab_tgt_in_acts; eauto; intro X; rewrite X in *; ins.

  destruct (classic (res_gget (incoming acts L (te_src edge)) gl = None)).
    eexists; repeat split; vauto.
    2: by eapply lab_src_in_acts; eauto; intro X; rewrite X in *; ins.
    rewrite <- (updI L edge), outgoing_upd_in_alt; ins; desf; eauto.
    rewrite res_gget_plus; intro; desf.
    rewrite <- outgoing_upd_in_alt, updI in H2; ins; desf; eauto.
    eapply helper_out_def; eauto.

  unfold incoming, in_sb, in_rf, in_esc in H1.
  rewrite !res_gget_plus, !res_gget_rsum in ×.
  repeat match goal with
             H : ¬ (_ ∨ _) |- _ ⇒ apply not_or_and in H; desc
           | H : ¬ (_ ∧ _) |- _ ⇒ apply not_and_or in H; des
           | H : ¬ _ |- _ ⇒ apply not_all_ex_not in H; desc
         end;
  repeat (rewrite in_map_iff in *; desf);
  clear G;
  (assert (HB: happens_before amap sb rf x0 (te_src edge));
  [match goal with H : res_gget (L ?tee) _ ≠ None |- _ ⇒
     let X := fresh in eapply hb_one with (te := tee); eauto; intro X; rewrite X in *; ins
   end | edestruct IH as [a' ?]; eauto; ins; desc; ∃ a'; split; eauto using mhb_trans, hb_mhb]).
Qed.

Lemma visible_ghost2 :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (GAC: ghost_alloc_conform acts L E)
    (CC: compat amap sb rf L) te a gl
    (G : res_gget (L te) gl ≠ None)
    (INC : res_gget (incoming acts L a) gl = None)
    (OUT : res_gget (outgoing acts L E a) gl ≠ None)
    (LR: label_restr acts amap sb rf L E)
    (ND: NoDup acts) (NDE: NoDup E) (INA: In a acts),
  may_happens_before amap sb rf a (te_src te).
Proof.
  ins; eapply visible_ghost_one with (N:=acts) in G; eauto using Consistent_prefix_closed; desf.
  2: by ins; eapply lab_src_in_acts; eauto; intro X; rewrite X in *; ins.
  assert (a = a0); desf.
  eapply GAC with (gl := gl); eauto; red; ins; desf;
  rewrite ghost_allocE in *; desf; eapply compat_inc in H; eauto.
Qed.

Lemma sat_exch_emp IE sigma : ¬ sat_exch IE sigma res_emp.
Proof.
  unfold sat_exch; red; ins.
  destruct IE as [p e A B]; ins.
  specialize (A sigma res_emp); specialize (B sigma res_emp).
  destruct (e sigma); specialize (H _ _ eq_refl).
  desf; [apply A|apply B]; repeat eexists; eauto using res_plus_emp_l; ins.
Qed.

Lemma ghost_elim_sat_exch IE P1 P2 Q r r' sigma :
   interp_exch IE sigma = (P1, P2) →
   ghost_elim P1 P2 Q r r' → sat_exch IE sigma r'.
Proof.
  destruct 2; [left|right]; congruence.
Qed.

Lemma three_sat_exch IE r1 r2 r3 sigma :
  sat_exch IE sigma r1 →
  sat_exch IE sigma r2 →
  sat_exch IE sigma r3 →
  r1 +!+ r2 +!+ r3 = Rundef.
Proof.
  unfold sat_exch; destruct IE as [p e A B]; ins.
  specialize (A sigma); specialize (B sigma).
  destruct (e sigma) as [P Q]; ins.
  apply NNPP; intro X.
  specialize (H _ _ eq_refl);
  specialize (H0 _ _ eq_refl); desf.
  1: by rewrite <- res_plusA in X; destruct (A (r1 +!+ r2));
        repeat eexists; ins; kundef.
  3: by rewrite <- res_plusA in X; destruct (B (r1 +!+ r2));
        repeat eexists; ins; kundef.
 specialize (H1 _ _ eq_refl); desf.
   by destruct (A (r2 +!+ r3)); repeat eexists; ins; kundef.
   by rewrite res_plusAC in X; destruct (B (r1 +!+ r3));
      repeat eexists; ins; kundef.
 specialize (H1 _ _ eq_refl); desf.
   by rewrite res_plusAC in X; destruct (A (r1 +!+ r3));
      repeat eexists; ins; kundef.
   by destruct (B (r2 +!+ r3)); repeat eexists; ins; kundef.
Qed.

Lemma ghost_step :
  ∀ b acts (NIN: ¬ In b acts) amap sb rf mo sc r P
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (PI: pres_in sb rf b acts) IE
    (GM: ghost_move IE r P) L EE
    (V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L EE a)
    (CC: compat amap sb rf (upd L (TsbS b) (L (TsbS b) +!+ r)))
    (CO: conform (b::acts) amap mo L acts)
    (ECO: ∀ sigma,
           exch_conform IE (b::acts) amap sb rf
                         (upd L (TsbS b) (L (TsbS b) +!+ r))
                         (upd L (TsbS b) (L (TsbS b) +!+ r)) EE sigma)
    (GAC: ghost_alloc_conform (b::acts)
                (upd L (TsbS b) (L (TsbS b) +!+ r)) EE)
    (VG: valid_ghost (incoming (b::acts) L b)
                     (r +!+ out_esc (b::acts) L EE b))
    (RS: res_lt (res_strip (incoming (b::acts) L b)) r)
    (EO: ∀ c, L (Tesc b c) = res_emp)
    (LR : label_restr (b::acts) amap sb rf L EE)
    (Osb : out_sb (b :: acts) L b = res_emp)
    (Orf : out_rf (b :: acts) L b = res_emp)
    (ND' : NoDup EE),
  ∃ L' EE' r,
    << IN': P r >> ∧
    << V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L' EE' a >> ∧
    << CC: compat amap sb rf (upd L' (TsbS b) (L' (TsbS b) +!+ r)) >> ∧
    << CO: conform (b::acts) amap mo L' acts >> ∧
    << ECO: ∀ sigma,
              exch_conform IE (b::acts) amap sb rf
                           (upd L' (TsbS b) (L' (TsbS b) +!+ r))
                           (upd L' (TsbS b) (L' (TsbS b) +!+ r)) EE' sigma >> ∧
    << GAC: ghost_alloc_conform (b::acts)
                (upd L' (TsbS b) (L' (TsbS b) +!+ r)) EE' >> ∧
    << VG: valid_ghost (incoming (b::acts) L' b)
                       (r +!+ out_esc (b::acts) L' EE' b) >> ∧
    << RS: res_lt (res_strip (incoming (b::acts) L' b)) r >> ∧
    << EO: ∀ c, L' (Tesc b c) = res_emp >> ∧
    << Esb: ∀ a b, L' (Tsb a b) = L (Tsb a b) >> ∧
    << Erf: ∀ a b, L' (Trf a b) = L (Trf a b) >> ∧
    << EsbS: ∀ a, L' (TsbS a) = L (TsbS a) >> ∧
    << ErfS: ∀ a, L' (TrfS a) = L (TrfS a) >> ∧
    << NDE : NoDup EE' >> ∧
    << EEE : ∀ sigma, In sigma EE → In sigma EE' >> ∧
    << LR : label_restr (b::acts) amap sb rf L' EE' >>.
Proof.
  induction 6; ins; unfold NW; desc.
    by eexists L, EE, r; repeat (split; ins).

Case "transitivity".
  exploit IHGM; eauto.
  clear r V CC CO ECO GAC VG EO RS IHGM GM GM' LR.
  intro; desf; exploit H; eauto.
    by rewrite <- Osb; unfold out_sb; f_equal; try done;
       clear - Esb; induction (b :: acts); ins; f_equal.
    by rewrite <- Orf; unfold out_rf; f_equal; try done;
       clear - Erf; induction (b :: acts); ins; f_equal.
  by intro; desf; repeat (eexists; try edone); eauto using eq_trans.

Case "Ghost allocation".
  assert (MM: ∃ mm,
                res_gget r mm = None ∧
                ∀ te, res_gget (L te) mm = None).
    clear - CONS LR.
    destruct (label_restr_fin CONS LR) as [myL EMP].
    destruct (res_gget_max_list (r :: map L myL)) as [mm X].
    ∃ (S mm); split; ins. eapply X; ins; vauto.
    destruct (classic (In te myL)); eauto using in_map.
    by rewrite EMP; ins.

  desf; assert (DEF: r ≠ Rundef) by (intro; subst; red in VG; desf).

  assert (CC' : compat amap sb rf (upd L (TsbS b)
           (L (TsbS b) +!+ r +!+
            Rdef (fun _ ⇒ p_bot) (gres_one mm gone) (fun _ ⇒ false)))).
    red; red; ins; eapply CC; eauto.
    revert H.
    destruct (classic (In (TsbS b) E)) as [C|C];
      [eapply In_NoDup_Permutation in C; desf;
       rewrite !(Permutation_rsum (Permutation_map _ C)); simpl; rewrite !upds|];
    rewrite !map_upd_irr; try done.
    rewrite !res_plusA, !(res_plusAC (Rdef _ _ _)), res_plusC; intro.
    apply NNPP; intro.
     revert H; apply res_gget_def; ins.
    unfold out_esc; repeat (rewrite res_gget_plus; right; split; ins).
    by rewrite res_gget_rsum; right; ins; rewrite in_map_iff in *; desf.

  eexists L, EE,
    (res_plus r (Rdef (fun _ ⇒ p_bot) (gres_one mm gone) (fun _ ⇒ false)));
    split; try edone; repeat (apply conj; try done).
    by eapply PEQ; eauto using gres_plus_emp_r, res_gget_def.

    ins; rewrite <- res_plusA; eapply exch_conform_ext1; try done.
    2: by intro ESC; apply res_escr_plusE in ESC; desf.

    red; ins; eapply ECO in ESC; ins; destruct ESC as (a' & M & M').
    ∃ a'; split; desf; eauto.
    rewrite incoming_upd_irr in *; ins.
    right; ins; edestruct M' as [gl Z]; desc; eauto.
    ∃ gl; repeat split; ins.
    destruct (eqP b a'); desf; [|by rewrite outgoing_upd_irr in *].
    revert Z1; rewrite res_plusA, !outgoing_upd_in, <- res_plusA; ins.
    rewrite res_gget_plus; intro; desf.
    apply res_gget_def in H; ins.
    repeat first [ apply res_gget_rsum; right; ins;
                   repeat (rewrite in_map_iff in *; desf)
                 | apply res_gget_plus; right; split; ins].
    by intro X; rewrite X in ×.

    eapply ghost_alloc_conform_helper2; eauto using helper_out_def, in_eq.
    ins; desf; desf; apply ghost_allocE in GA'; desf.
      by eapply helper_out_def in GA'; eauto using compat_mon_upd.
    clear - GA' MM0; unfold outgoing, out_sb, out_rf, out_esc in GA'.
    by repeat first
       [ rewrite res_gget_rsum in GA'; apply not_or_and in GA';
         destruct GA' as [_ GA']; apply not_all_ex_not in GA'; desc;
         apply imply_to_and in GA'; rewrite in_map_iff in *; desf
       | rewrite res_gget_plus in GA'; apply not_or_and in GA';
         destruct GA' as [_ GA']; apply not_and_or in GA'; desf].

    red in VG; ins; desf.
    rewrite !res_plusA, res_plusAC, res_plusC.
    eapply res_gget_def2 with (mm := mm) (gone := gone) in VG0; eauto; desf.
    do 7 (eexists; eauto); unnw.
    assert (KK: res_gget (incoming (b :: acts) L b) mm = None).
      unfold incoming, in_sb, in_rf, in_esc;
      repeat (rewrite res_gget_plus; right; split; ins);
      by rewrite res_gget_rsum; right; ins; rewrite in_map_iff in *; desf.
    rewrite VG in KK; simpls.
    clear - KK VG0 VGG; ins; specialize (VGG _ _ RG); desc; ins.
    destruct gm as [A gm]; ins.
    unfold gres_plus, gres_one in VG0; des_eqrefl; desf; ins.
    by inv_lplus gl; desf; desf; rewrite VGG in *; ins; desf; ins; eauto.

    by unfold out_esc; repeat (rewrite res_gget_plus; right; split; ins);
       rewrite res_gget_rsum; right; ins; rewrite in_map_iff in *; desf.

  by eapply res_lt_trans, res_lt_plus_r, res_lt_refl.

Case "Ghost update".
  assert (GG: ∃ g'', gres_plus (gres_strip g) g' = Some g''). {
    generalize (GDEF (gres_strip g)); rewrite gres_plus_strip_idemp, gres_plusC.
    destruct (gres_plus (gres_strip g) g'); vauto.
    by intro X; specialize (X eq_refl).
  }
  desc.
  assert (GDEF' : ∀ gF,
         gres_plus g'' gF = None → gres_plus g gF = None).
    clear - GG GDEF; ins.
    case_eq (gres_plus g gF) as EQ; ins; exfalso.
    rewrite gres_plusC in GG.
    eapply (gres_plusA2 GG) in H; desf.
      by apply (gres_plusA (gres_plus_strip_idemp g)) in EQ; desf.
    apply (gres_plusA (gres_plus_strip_idemp g)) in EQ; desf.
    by rewrite GDEF in ×.

  assert (CC': compat amap sb rf (upd L (TsbS b) (L (TsbS b) +!+ Rdef p g'' e))).
    repeat red; intros; eapply CC; eauto; revert H.
    destruct (classic (In (TsbS b) E)) as [C|C];
      [eapply In_NoDup_Permutation in C; desf;
       rewrite !(Permutation_rsum (Permutation_map _ C)); simpl; rewrite !upds|];
    rewrite !map_upd_irr; try done.
    rewrite !res_plusA, 2!(res_plusAC (Rdef _ _ _)); simpl; desf.
    apply GDEF' in Heq1; congruence.

  eexists L, EE, (Rdef p g'' e); repeat (apply conj; try done).
    assert (XX: Rdef p g'' e =
          Rdef p g' e +!+ Rdef (fun _ ⇒ p_bot) (gres_strip g) (fun _ ⇒ false)).
      by rewrite res_plusC; ins; rewrite lift_plus_emp_l, GG.
    by rewrite XX; eapply RP_ext; congruence.

  {
    red; intros.
    exploit (ECO sigma edge); eauto.
      apply res_plus_eq_empD, proj1 in Osb; rewrite Osb, res_plus_emp_l in ×.
      by revert ESC; unfold upd; desf.
    intros (a' & M & M'); ∃ a'; revert M M'.
    rewrite !updo, !incoming_upd_irr; ins; split; ins.
    clear VG; desf; eauto; right; ins.
    edestruct M' as [gl Z]; desc; eauto;
    ∃ gl; repeat split; ins.
    destruct (eqP b a'); desf; [|by rewrite outgoing_upd_irr in *].
    revert Z1; rewrite !outgoing_upd_in; ins.
    rewrite res_plusC in Z1; rewrite res_plusC; ins; desf; ins.
    2: apply GDEF' in Heq1; congruence.
    clear - Z1 Heq2 Heq1 GG.
    unfold gres_plus, gres_strip in *; repeat des_eqrefl; ins; desf; ins.
    inv_lplus gl; destruct (g gl), (o1 gl); ins; desf; congruence.
  }

  {
    eapply ghost_alloc_conform_helper1; eauto using helper_out_def, in_eq; subst.
    rewrite (proj1 (res_plus_eq_empD _ _ Osb)), !res_plus_emp_l.
    clear - GDOM GG; ins; intro X; specialize (GDOM _ X).
    unfold gres_plus, gres_strip in *; des_eqrefl; desf; ins.
    inv_lplus gl; rewrite X in *; ins; desf; congruence.
  }

  desf; clear - RS GG VG GDEF GDEF' GDOM; unfold valid_ghost in *; ins; desf.
  2: by apply GDEF' in Heq1; congruence.
  rewrite VG; do 7 eexists; eauto.
  unnw.
  assert (GDOM' : ∀ gl, g gl = None ↔ g'' gl = None).
  { clear - GG GDOM.
    unfold gres_plus, gres_strip in GG; repeat des_eqrefl; desf; split; ins; inv_lplus gl.
    rewrite H, (GDOM _ H) in *; ins; desf.
    by rewrite H in *; destruct (g gl), (g' gl); ins; desf.
  }

  rewrite VG in *; simpls.

  clear - GG Heq1 Heq2 VGG RS GDEF GDEF' GDOM'; ins; specialize (VGG _ _ RG); desc.
  destruct gm as [A gm]; ins.
  rewrite gres_plusC in Heq1, Heq2.
  unfold gres_plus, gres_strip in Heq1, Heq2; repeat des_eqrefl; desf; ins.
  inv_lplus gl; specialize (GDOM' gl); rewrite VGG in ×.
  destruct (gres gl) as [[B gg]|]; ins; desf;
  try rewrite <- eq_rect_eq in *; desf;
  try (by exploit GDOM');
  try (by exploit GDOM'0); eauto.

   repeat eexists; eauto; ins.
   clear GDOM' GDOM'0.
   unfold gres_plus in GG; des_eqrefl; desf; ins.
   eapply VGG0; clear VGG0.

   rewrite salg_plusC in Heq1, Heq3.
   eapply salg_plusA2 in SPN; eauto; desf; eauto using salg_plusA3.

   clear GDEF; specialize (GDEF' (gres_one gl (Some (existT _ A yz)))).

   unfold gres_plus in GDEF'; repeat des_eqrefl; ins; desf; try (by exploit GDEF');
   clear GDEF'; inv_lplus gl; desf; desf;
   try rewrite Heq in *; try rewrite Heq0 in *; ins; desf; try rewrite <- eq_rect_eq in *; desf; desf;
   ins; desf; try rewrite <- eq_rect_eq in *; desf; eauto using salg_plusA4;
   match goal with
       H : None = _ |- _ ⇒
       symmetry in H; apply lift_plus_noneD in H; desf;
       unfold olift_plus in *; ins; desf; ins; desf; ins; desf;
       try rewrite <- eq_rect_eq in *; clarify; eauto using salg_plusA3
   end; eauto using salg_plusA4.

   rewrite <- H0; clear H0.
   unfold gres_plus in GG; des_eqrefl; desf; ins.
   assert (∃ t, o1 gl = Some (existT _ A t)).
     by clear GDEF'; inv_lplus gl; rewrite H1 in *; ins; desf; eauto.
   desc; repeat eexists; eauto; ins.
   specialize (GDEF' (gres_one gl (Some (existT _ A fr)))).
   unfold gres_plus in GDEF'; repeat des_eqrefl; ins; desf; try (by exploit GDEF');
   clear GDEF'; inv_lplus gl; desf; desf;
   try rewrite H in *; ins; desf; desf; try rewrite <- eq_rect_eq in *; clarify.
   by symmetry in EQ0; apply lift_plus_noneD in EQ0; desf;
      symmetry in EQ1; apply lift_plus_noneD in EQ1; desf; clarify;
      unfold olift_plus in *; ins; desf; ins; desf; ins; desf;
      try rewrite <- eq_rect_eq in *; clarify; eauto.

  rewrite res_lt_strip_l in ×.
  eapply res_lt_trans; eauto.
  ∃ (Rdef (fun _ ⇒ p_bot) (gres_strip g') (fun _ ⇒ false)).
  desf; clear - GG; ins.
  apply gres_strip_plus in GG; rewrite gres_strip_idemp in GG; rewrite GG.
  rewrite lift_plusC, lift_plus_emp_l; ins; auto using prot_plusC; f_equal; ins.
  by extensionality l; rewrite orbF.

Case "Escrow introduction".
  assert ((r1 +!+ Rdef (fun _ : nat ⇒ p_bot) gres_emp (eq_op^~ sigma)) +!+
          res_strip r2 ≠ Rundef).
    by desf; rewrite res_plusC, res_plusAC, <- res_plusA; auto with rpd.

  assert (ESE : ∀ a, ¬ In sigma EE → L (TescS sigma a) = res_emp).
    by intros; apply LR; auto.

  assert (CC': compat amap sb rf (upd L (TsbS b)
                 (L (TsbS b) +!+ r1 +!+
                  Rdef (fun _ : nat ⇒ p_bot) gres_emp (eq_op^~ sigma) +!+ r2))).
  { rewrite (res_plusC _ r2).
    clarify; clear - NIN CC; repeat red; ins; eapply CC; eauto.
    revert H.
    destruct (classic (In (TsbS b) E)) as [C|C];
      [eapply In_NoDup_Permutation in C; desf;
       rewrite !(Permutation_rsum (Permutation_map _ C)); simpl; rewrite !upds|];
    rewrite !map_upd_irr; eauto.
    by rewrite !res_plusA, !(res_plusAC (Rdef _ _ _)); simpl; desf;
       rewrite ?gres_plusI, ?lift_plus_emp_l in ×.
  }

  eexists (upd L (TescS sigma b) (L (TescS sigma b) +!+ r2)),
          (if excluded_middle_informative (In sigma EE) then EE else sigma :: EE),
          ((r1 +!+ Rdef (fun _ : nat ⇒ p_bot) gres_emp (eq_op^~ sigma)) +!+ res_strip r2);
    split; try edone.
    by eapply RP_ext; eauto.
  repeat (match goal with |- _ ∧ _ ⇒ apply conj end;
          auto using in_eq, in_cons; try done); try (by intros; apply updo).
  clear - ESE NIN V; ins; specialize (V _ IN); unfold valid_node in *; desc.
  eexists r; ins.
  unfold incoming, out_esc, out_sb, out_rf, in_sb, in_rf, in_esc in *; ins.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  unfold NW.

  repeat split;
    try by unfold upd; ins; desf; ins; try rewrite ESE, res_plus_emp_l; eauto.

  rupd; rewrite updC; try done; eapply compat_upd2_acc; try done.
  by rewrite !res_plusA, (res_plusC (res_strip r2)), res_plus_strip_idemp.

  clear - NIN CO; red; ins.
  unfold outgoing, out_sb, out_esc, out_rf; ins.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  unfold upd; desf; eapply CO; ins.

  assert (DEF': L (TescS sigma b) +!+ r2 ≠ Rundef).
    subst; clear - ND' ESE VG; red in VG; unfold out_esc in *; desf; ins.
    revert VG0.
    destruct (classic (In sigma EE)) as [C|];
      [eapply In_NoDup_Permutation in C; desf;
       rewrite (Permutation_rsum (Permutation_map _ (Permutation_map _ C)))|
      rewrite ESE, res_plus_emp_l]; ins;
    try rewrite res_plusC; rewrite !res_plusA, <- (res_plusA r2), res_plusAC in *;
    intro X; rewrite X in *; ins.

  {
  clear CC'; ins.

  red; ins.

  destruct (eqP (te_src edge) b) as [|NEQ].
    destruct (classic (sigma = sigma0)) as [|X].
       by desc; ∃ b; clarify; rewrite mhbE; rupd; split; eauto;
          red; ins; rewrite EI in *; desf; eauto using RP_extC.

    assert (M: ∃ a,
              sat_exch IE sigma0 (L (TescS sigma0 a)) ∧
              (may_happens_before amap sb rf a b ∨
              ∀ r : resource,
                 sat_exch IE sigma0 r →
                 incoming (b :: acts) L a +!+ r ≠ Rundef →
                 ∃ gl : nat,
                   res_gget r gl ≠ None ∧
                   res_gget (incoming (b :: acts) L a) gl = None ∧
                   res_gget (outgoing (b :: acts) (upd L (TsbS b) (L(TsbS b) +!+ r1 +!+ r2)) EE a)
                gl ≠ None)).
    { clear RINS DEF'; unfold upd in ESC; revert ESC; desf.
      intro.
        apply res_plus_eq_empD, proj1 in Osb; rewrite Osb, res_plus_emp_l in ×.
        rewrite res_plusA, res_plusAC in ESC.
        destruct edge; unfold te_src in *; try done.
        apply res_escr_plusE in ESC; ins; desf; desf.

      ins; exploit (ECO sigma0 (TsbS a)); rupd; eauto.
        eapply res_escr_plusI; ins; apply res_escr_plusE in ESC; ins; desf; eauto.
        by destruct r2; ins; eauto.
      by intro M; desc; revert M M0; rewrite !incoming_upd_irr; rupd; ins; eauto.

      intro.
        apply res_plus_eq_empD, proj1 in Osb; rewrite Osb, res_plus_emp_l in ×.
        destruct edge; unfold te_src in *; try done.
        apply res_escr_plusE in ESC; ins; desf; desf.

      by ins; destruct (ECO sigma0 (TescS sigma a)) as [? M]; desc;
         try revert M M0; rewrite ?incoming_upd_irr; rupd; ins; eauto.

      ins; destruct (ECO sigma0 (TsbS a)) as [? M];
      try revert M; rupd; eauto.
      by eapply res_escr_plusI; ins; desf; eauto.

      by rewrite ?incoming_upd_irr; eauto.

      ins; exploit (ECO sigma0 edge); eauto.
        by revert ESC; rupd; intro; desf.
      intros (a & M & M'); ∃ a; revert M M';
        rewrite ?incoming_upd_irr; rupd; ins.
    }

    desc; clarify; ∃ a; split; rupd; try congruence.
    clear RINS; des; eauto; right; rewrite !incoming_upd_irr; ins.
    edestruct M0 as [gl K]; eauto; desc; ∃ gl.
    repeat split; ins; rupd.
    rewrite outgoing_upd2_acc, !res_plusA, res_plus_strip_l, (res_plusC (Rdef _ _ _));
      ins; try (by desf; vauto).
    rewrite outgoing_upd_sbS, ?res_plusA, (outgoing_ee LR), !(res_plusAC (Rdef _ _ _)) in ×.
    desf; desf.
    by rewrite res_gget_plus; intro; desf;
       rewrite res_plusC in H0; apply res_plus_escr_def in H0; ins;
       intro XX; rewrite XX in *; ins.

  exploit (ECO sigma0 edge); eauto.
    by revert ESC; rupd; intro; desf.
  intros (a & M & M'); ∃ a; revert M M'; rewrite !incoming_upd_irr; ins.
  rewrite outgoing_upd2_acc; ins; try (by clear RINS; desf; vauto).
  split.
    by clear M'; revert M; unfold upd; des_if; eauto using sat_exch_ext.
  rupd; rewrite !res_plusA, res_plus_strip_l, (res_plusC (Rdef _ _ _)).
  rewrite outgoing_upd_sbS, (outgoing_ee LR) in ×.
  clear RINS; desf; desf; eauto.
  right; ins; exploit M'; eauto; intros [gl Z]; desc; ∃ gl; repeat split; ins.
  rewrite !res_plusA, !(res_plusAC (Rdef _ _ _)) in ×.
  by rewrite res_gget_plus; intro; desf;
     rewrite res_plusC in H0; apply res_plus_escr_def in H0; ins;
     intro XX; rewrite XX in *; ins.
  }

  rupd; clear RINS.
  eapply ghostalloc_upd2_acc; intros; clarify;
    try (by desf; eauto using in_eq, in_cons, NoDup).
  rewrite !res_plusA, res_plus_strip_l; subst.
  eapply ghost_alloc_conform_helper1.
    by desf; vauto.
    by instantiate (1 := L (TsbS b) +!+ r1 +!+ r2);
       desf; clear -LR GAC n; red in LR; desc;
       red; intros; eapply GAC; eauto;
       revert OUT OUT'; unfold outgoing, out_esc; simpl; rupd;
       rewrite !LRescS, !res_plus_emp_l; ins; vauto.
    intro; rewrite !ghost_allocE; intro X; desf.
    destruct (CC' (TsbS b :: nil));
      (try (by clear; ins; desf; rupd; rewrite ?res_plus_emp_r; vauto)).
    by ins; rupd; rewrite ?res_plus_emp_r; vauto.
    by right; rewrite (res_plusC _ r2), <- (res_plusA r1), <- res_plusA in X;
       rewrite res_gget_plus in X; apply not_or_and in X;
       destruct X as [_ X]; apply not_and_or in X; desf.
  by eapply helper_out_def; desf; eauto using NoDup, in_eq, lr_ext_esc.

  clear RINS.
  remember (b :: acts) as acts'; clear Heqacts'.
  unfold incoming, in_esc, in_sb, in_rf in *; ins.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  unfold out_esc in *; ins; rupd.
  rewrite map_upd_irr with (l := map (Tesc b) acts');
    try (by rewrite in_map_iff; intro; desf).
  clarify.

  clear CC'.
  replace (rsum
       (map (upd L (TescS sigma b) (L (TescS sigma b) +!+ r2))
            (map (TescS^~ b)
                 (if excluded_middle_informative (In sigma EE)
                  then EE
                  else sigma :: EE))))
    with (r2 +!+ rsum (map L (map (TescS^~ b) EE))).
  2: desf; ins; rupd.
  2: rewrite replace_edge_ext; try apply nodup_map; try apply in_map_iff;
     eauto; congruence.
  2: rewrite map_upd_irr; try rewrite in_map_iff; try intro; desf.
  2: by red in LR; desc; rewrite LRescS, res_plus_emp_l; auto.
  rewrite !res_plusA in ×.
  rewrite (res_plusAC _ r1), (res_plusAC r2).
  rewrite <- (res_plusA r2), res_plus_strip_idemp.
  red in VG; desf; rewrite VG, VG0; ins; rewrite lift_plus_emp_l, gres_plusI; ins.
  do 7 eexists; ins; desf; eauto; try apply/orP; try rewrite VG1 in *; desf;
    eauto using eqxx.

  clarify; clear - H RS RDEF.
  rewrite incoming_upd_irr; ins.
  rewrite res_lt_strip_l, !res_strip_plus, !res_strip_idemp in *; ins.
    by rewrite res_plusA, res_plusAC; auto using res_lt_plus_l.
  by intro X; rewrite X in ×.

  by ins; rupd.

  by desf; vauto.

  by desf; vauto.

  by desf; auto using in_eq, lr_ext_esc.

Case "Escrow elimination 1".

  subst.

  edestruct (ECO sigma (TsbS b)) as (a & M & M'); rupd; eauto.
    by apply res_plus_eq_empD, proj1 in Osb; rewrite Osb, res_plus_emp_l in ×.
  rewrite updo in M; ins.
  rewrite incoming_upd_irr in M'; ins.

  assert (INS: In sigma EE).
    clear - M LR ESCR; apply NNPP; intro X.
    red in LR; desc; rewrite LRescS in M; auto.
    by apply sat_exch_emp in M.

  assert (INA: In a (b :: acts)).
    clear - M LR ESCR; apply NNPP; intro X.
    red in LR; desc; rewrite LRescS in M; auto.
    by apply sat_exch_emp in M.

  destruct (eqP a b) as [|NEQ]; subst.
  { clear M'.
    assert (DEF1: rE +!+ L (TsbS b) +!+ r0 +!+ L (TescS sigma b) ≠ Rundef).
      intro; destruct (CC (TsbS b :: TescS sigma b :: nil)); ins.
        by repeat constructor; ins; intro; desf.
        by desf.
      rupd; try congruence.
      revert H.
      rewrite res_plus_emp_r, (proj1 (res_plus_eq_empD _ _ Osb)), !res_plus_emp_l.
      by rewrite res_plusA.

    assert (DEF': (r0 +!+ res_strip rE) +!+ L (TescS sigma b) ≠ Rundef).
      intro X; apply DEF1; clear -X Osb.
      rewrite (proj1 (res_plus_eq_empD _ _ Osb)), res_plus_emp_l.
      rewrite res_plusA in X.
      by rewrite <- (res_plus_strip_idemp rE), !res_plusA, (res_plusAC r0),
                 X, res_plus_undef.

    eexists (upd L (TescS sigma b) rE),
            EE, ((r0 +!+ res_strip rE) +!+ L (TescS sigma b)).
    split; rupd.
      clear - DEF' DEF1 M GEL ESCR.
      rewrite <- !res_plusA, res_plusC, <- !res_plusA in DEF1.
      specialize (M _ _ ESCR); destruct GEL; desf.
      by destruct (@interp_exchOK1 IE sigma (L (TescS sigma b) +!+ rE));
         rewrite ESCR; ins; repeat eexists; ins; kundef.
      by eapply IN'; split; ins; do 3 eexists; eauto; split; eauto; kundef.
      by eapply IN'; split; ins; do 3 eexists; eauto; split; eauto; kundef.
      by destruct (@interp_exchOK2 IE sigma (L (TescS sigma b) +!+ rE));
         rewrite ESCR; ins; repeat eexists; ins; kundef.
    split; ins.
      by repeat apply valid_node_upd_irr; eauto; simpl; try intro; desf.
    split.
      rewrite updC, <- res_plusA; rupd; try (by intro; desf).
      by eapply compat_upd2_swap; ins; rewrite !res_plusA, res_plus_strip_l, (res_plusC r0).
    split.
      by red; unfold out_rf; ins; rewrite !map_upd_irr, !updo in *; ins;
         try (by rewrite in_map_iff; intro; desf); eapply CO.
    split.
      ins; rewrite updC, <- !res_plusA; rupd; ins.
      eapply exch_conform_upd2_swap; rupd; ins; desf.
      rewrite !res_plusA, res_plus_strip_l.
      rewrite updC; ins.
      rewrite (res_plusC r0 rE).
      eapply exch_conform_upd1_acc; eauto; ins; desf.
          by eauto using ghost_elim_sat_exch.
        by rewrite !(res_plusAC (res_strip rE)), <- res_plusA, res_plus_strip_l.
      clear; rewrite !(res_plusAC (res_strip rE)), <- res_plusA, res_plus_strip_l.
      by rewrite res_plusAC, <- !res_plusA, res_plusC, !res_plusA.
    split.
      rewrite updC, <- !res_plusA; rupd; ins.
      eapply ghostalloc_upd2_swap; rupd; ins; desf; try congruence.
      by rewrite !res_plusA, res_plus_strip_l, (res_plusC r0).
    inv ND.
    rewrite incoming_upd_irr; try done.
    rewrite out_esc_upd_in2; rupd; ins; try congruence.
    repeat (match goal with |- _ ∧ _ ⇒ split end; eauto 6 using in_eq, in_cons, pres_in_hb);
      ins; try by intros; rewrite ?updo; try intro; desf; eauto using in_eq.

    rewrite (res_plusC _ rE); rewrite !res_plusA in ×.
    rewrite !(res_plusAC rE), !(res_plusAC (L (TescS sigma b))).
    rewrite (res_plusAC (res_strip rE)), <- (res_plusA rE), res_plus_strip_idemp.
    by rewrite res_plusC, !res_plusA, <- out_esc_upd_in2, updI; ins.

    apply res_lt_plus_r.
    by rewrite res_lt_strip_l, res_strip_plus, res_strip_idemp in *; ins;
       try kundef; rewrite res_plusC.
  }


  assert (HB: happens_before amap sb rf a b).
  {
    rewrite outgoing_upd_irr in M'; ins; try congruence.
    rewrite mhbE in *; desf.
    inv ND;
    edestruct (compat_inc_sink)
    with (a := a) (b:= b)
         (L := upd L (TsbS b) (L (TsbS b) +!+ rE +!+ r0))
      as [|[|[|ZZZ]]];
    eauto using in_eq; desf.
    by exfalso; eauto using prefix_closed_hb.

    rewrite incoming_upd_irr, upds, !res_plusA, (res_plusAC r0) in ZZZ; ins.


    exploit (M' rE); clear M'; eauto using ghost_elim_sat_exch.
      by rewrite res_plusC; kundef.
    intro K; desc.
    exploit (visible_ghost2 CONS GAC CC (TsbS b) a gl); rupd; eauto using in_eq, in_cons;
      rewrite ?incoming_upd_irr, ?outgoing_upd_irr; ins; try congruence.
      rewrite (proj1 (res_plus_eq_empD _ _ Osb)), res_plus_emp_l in ×.
      by rewrite res_gget_plus; intro; desf.
    rewrite mhbE in *; desf.
  }
  clear M'.

  assert (DEF: L (TescS sigma a) +!+ (rE +!+ r0) +!+
                          out_esc (b :: acts) L EE b ≠ Rundef).
  {
    unfold out_esc.
    rewrite rsum_map_map_eq_empI with (l := b :: acts), res_plus_emp_r; ins.
    rewrite !res_plusA; intro Z.
    eapply CC with (E := (TescS sigma a :: TsbS b :: map (TescS^~ b) EE)).
      by repeat constructor; ins; try apply nodup_map; ins;
         try rewrite in_map_iff; try intro; desf.
      by ins; desf; ins; rewrite in_map_iff in *; desf; eauto.
    ins; rewrite upds, !updo; ins; try congruence.
    rewrite map_upd_irr; try (by rewrite in_map_iff; intro; desf).
    subst; eapply res_plus_eq_empD, proj1 in Osb.
    by rewrite Osb, res_plus_emp_l, !res_plusA.
  }

  ins; desf.

  assert (DEFi: L (TescS sigma a) +!+ incoming (b :: acts) L b ≠ Rundef).
     by desf; rewrite res_plusC; eapply helper_plus_inc_escS_def;
        eauto using compat_mon_upd.

  assert (MYDEF: (r0 +!+ res_strip rE) +!+ L (TescS sigma a) ≠ Rundef).
    rewrite res_plusC, <- res_plusA; apply res_plus_strip_def; rewrite res_plusA.
    by intro X; apply DEF; clear - X; rewrite <- res_plusA, (res_plusC rE);
       rewrite X.

  assert (VIS: ∀ gl,
            res_gget (incoming (b :: acts) L b) gl = None →
            res_gget ((rE +!+ r0) +!+ out_esc (b :: acts) L EE b) gl ≠ None →
            res_gget (L (TescS sigma a)) gl = None).
    ins; apply NNPP; intro K.
    exploit (visible_ghost2 CONS GAC CC (TescS sigma a) b gl); rupd; eauto using in_eq, in_cons;
      rewrite ?incoming_upd_irr, ?outgoing_upd_in; ins; try congruence.
      by unfold outgoing; rewrite Osb, Orf, !res_plus_emp_l, res_plusC.
    by eauto 3 using hb_irr, mhb_hb_trans.

  eexists (upd (upd (upd L (TescS sigma a) res_emp)
                    (Tesc a b) (L (TescS sigma a) +!+ L (Tesc a b)))
               (TescS sigma b) (L (TescS sigma b) +!+ rE)),
          EE, ((r0 +!+ res_strip rE) +!+ L (TescS sigma a)).
  split; desf.
      clear - MYDEF DEF M GEL ESCR.
      rewrite <- !res_plusA in DEF.
      specialize (M _ _ ESCR); destruct GEL; desf.
      by destruct (@interp_exchOK1 IE sigma (L (TescS sigma a) +!+ rE));
         rewrite ESCR; ins; repeat eexists; ins; kundef.
      by eapply IN'; split; ins; do 3 eexists; eauto; split; eauto; kundef.
      by eapply IN'; split; ins; do 3 eexists; eauto; split; eauto; kundef.
      by destruct (@interp_exchOK2 IE sigma (L (TescS sigma a) +!+ rE));
         rewrite ESCR; ins; repeat eexists; ins; kundef.
  split; ins.
  destruct (eqP a0 a); clarify.
  2: by repeat apply valid_node_upd_irr; eauto; simpl; try intro; desf.
  apply valid_node_upd_irr; ins.
  by apply valid_node_upd_esc; eauto using in_eq.

  split.
    rupd; rewrite updC; try (by intro; desf); eapply compat_upd2_acc; ins;
    rupd; try (by intro; desf).
    eapply compat_upd3; eauto; try done; rewrite ?M, ?res_plus_emp_l;
      auto using res_lt_plus_l, res_lt_refl, res_lt_emp_l;
      try congruence.
    by rewrite !res_plusA, !(res_plusAC (L (TescS sigma a))), (res_plusC _ rE),
               res_plus_strip_idemp, (res_plusC rE); apply res_lt_refl.

  split.
    by red; unfold out_rf; ins; rewrite !map_upd_irr, !updo in *; ins;
       try (by rewrite in_map_iff; intro; desf); eapply CO.

  split.
    ins; rupd.
    eapply exch_conform_upd2_acc; rupd; ins; try congruence.
    rewrite !res_plusA, <- (res_plusAC (res_strip rE)), res_plus_strip_l,
            (res_plusC (L (TescS sigma a)) rE), (res_plusAC rE).

    assert (DEF' : outgoing (b :: acts) L EE b +!+ rE +!+ r0 +!+ L (TescS sigma a) ≠ Rundef).
      rewrite <- !res_plusA, (res_plusA _ rE).
      unfold outgoing; rewrite Osb, Orf, !res_plus_emp_l.
      by rewrite (res_plusC _ (rE +!+ r0)), res_plusC.

    destruct (classic (sigma0 = sigma)).
    { red; ins; subst.
      clear ESC; ∃ b; split; rupd.

      rewrite res_plusC; eapply sat_exch_ext; ins; eauto using ghost_elim_sat_exch.
      intro X; apply DEF.
      rewrite res_plusA, (res_plusAC r0).
      unfold out_esc.
      eapply In_NoDup_Permutation in INS; desc; ins.
      rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ INS)));
      ins.
      by rewrite res_plusA, <- (res_plusA rE), X; ins; rewrite ?res_plus_undef.

      rewrite incoming_upd_irr, updC, incoming_upd_irr, res_plusC, incoming_upd_in,
              <- res_plusA, <- incoming_upd_in, updI; ins; auto.
      rewrite outgoing_upd_in, 2!outgoing_upd_irr; rupd; ins; desf; try congruence.
      right; ins.
      rewrite res_plusA in IDEF.
      rewrite <- !res_plusA, (res_plusA _ rE).
      unfold outgoing; rewrite Osb, Orf, !res_plus_emp_l, (res_plusC _ (rE +!+ r0)).
      eapply valid_ghost_gget; ins.
        apply NNPP; intro K.
        exploit (visible_ghost2 CONS GAC CC (TescS sigma a) b m); rupd; eauto using in_eq, in_cons;
          rewrite ?incoming_upd_irr, ?outgoing_upd_in; ins; try congruence.
          by unfold outgoing; rewrite Osb, Orf, !res_plus_emp_l, res_plusC.
        by eauto 3 using hb_irr, mhb_hb_trans.
      by rewrite res_plusC.

      rewrite res_plusC, <- !res_plusA.
      assert (X := three_sat_exch M SE (ghost_elim_sat_exch _ _ ESCR GEL)).
      by rewrite <- res_plusA in X; rewrite X.
    }
 
    assert (DEF'' : L (TescS sigma b) +!+ rE +!+ L (TsbS b) +!+ r0 +!+
                      res_strip rE +!+ L (TescS sigma a) ≠ Rundef).
    { clear - DEF INS ND' Osb.
      rewrite (proj1 (res_plus_eq_empD _ _ Osb)), res_plus_emp_l.
      rewrite (res_plusAC (res_strip rE)), <- (res_plusA rE), res_plus_strip_idemp.
      rewrite <- (res_plusA rE), res_plusAC, <- res_plusA, res_plusC, <- !res_plusA.
      intro X; apply DEF.
      eapply In_NoDup_Permutation in INS; desc; ins; unfold out_esc.
      rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ INS))).
      by ins; rewrite <- !res_plusA, X; ins.
    }
    eapply exch_conform_upd1_acc; rupd; ins; try rewrite res_plusA; ins;
    try congruence.
    rewrite updC; ins; eapply exch_conform_irr1; ins.
    rewrite res_plusAC, (res_plusAC (res_strip rE)),
            <- (res_plusA rE), res_plus_strip_idemp.
    eapply exch_conform_upd3 with
      (r4 := L (TescS sigma a))
      (rr := L (TsbS b) +!+ rE +!+ r0);
      try rewrite res_plus_emp_l; ins; desf; eauto using res_plusC.
    2: by rewrite !res_plusA.
    2: by rewrite outgoing_upd_in, !res_plusA; ins.
    2: by rewrite outgoing_upd_in, res_plusC in M2; ins;
          unfold outgoing in M2; rewrite Osb, Orf, !res_plus_emp_l in M2; eauto.
    {
      rewrite <- (res_plusA rE), <- res_plusA.
      red; ins; rupd; unfold upd in ESC; desf; [eapply res_escr_plus in ESC; desf|].
      3: by rewrite (proj1 (res_plus_eq_empD _ _ Osb)), res_plus_emp_l, res_plusA; kundef.
      × edestruct (ECO sigma0 (TsbS b)) as [a' Z]; rupd; ins.
        ∃ a'; revert Z; rupd; congruence.
      × edestruct (ECO sigma0 (TescS sigma a)) as [a' Z]; rupd; ins.
        ∃ a'; revert Z; rupd; try congruence; ins; des; split;
        eauto using mhb_trans, hb_mhb.
      × edestruct (ECO sigma0 edge) as [a' Z]; rupd; ins.
        ∃ a'; revert Z; rupd; congruence.
    }

  split.
  { eapply ghostalloc_upd2_acc; rupd; ins; try congruence.
    eapply ghostalloc_upd3; eauto; rewrite ?res_plus_emp_l; ins; desf; eauto using res_plusC.
      by rewrite res_plusC, !res_plusA, res_plusAC,
            (res_plusAC (res_strip rE)), <- (res_plusA rE), res_plus_strip_idemp.
    rewrite outgoing_upd_in; unfold outgoing; ins; rewrite Osb, Orf, !res_plus_emp_l.
    by rewrite res_plusC, res_plusA, res_plusAC, <- res_plusA in DEF.
  }
  inv ND.
  revert VG DEF.
  rewrite incoming_upd_irr, updC, incoming_upd_irr; try done.
  rewrite incoming_upd_ext_esc; ins; eauto using pres_in_hb.
  rewrite out_esc_upd_in, !out_esc_upd_irr; rupd; ins; try congruence.
  repeat (match goal with |- _ ∧ _ ⇒ split end; eauto 6 using in_eq, in_cons, pres_in_hb);
    ins; try by intros; rewrite !updo; try intro; desf; eauto.
  {
    rewrite (res_plusC _ rE); rewrite !res_plusA in ×.
    rewrite !(res_plusAC rE), !(res_plusAC (L (TescS sigma a))).
    rewrite (res_plusAC (res_strip rE)), <- (res_plusA rE), res_plus_strip_idemp.
    red in VG; desc; rewrite VG in ×.
    destruct (L (TescS sigma a)); ins; desf.
    do 7 eexists; ins; unnw.
    clear - VIS Heq Heq0 VGG.
    ins; unfold gres_plus in *; repeat des_eqrefl; desf; ins.
    inv_lplus gl; specialize (VIS gl); specialize (VGG gl); rewrite RG in ×.
    destruct (gres gl) as [[A gg]|]; ins; desf; eauto;
    try specialize (VGG _ eq_refl); desf; ins;
    try (by exploit VIS);
    try rewrite <- H1; try rewrite <- H0; eauto.
    eexists; split; ins.
    by case_eq (salg_plus A s0 fr) as N;
       rewrite salg_plusC in Heq1, Heq3; eapply salg_plusA in N; eauto;
       desf; rewrite VGG0 in N; ins; eapply salg_plusA2 in SPN; eauto; desf.
  }
  rewrite res_plusC.
  rewrite res_lt_strip_l in *; apply res_lt_strip_frame.
  2: by rewrite res_plusC.
  rewrite res_plusC; revert RS; rewrite !res_strip_plus, res_strip_idemp; ins.
  by rewrite res_plusC; intro X; rewrite X in *; desf.
Qed.