Require Import Omega.
Require Import Vbase Arith Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel GpsModelLemmas GpsGlobal.

Remove Hints plus_n_O mult_n_O.
Hint Immediate plus_n_O mult_n_O.

Local Open Scope string_scope.

Set Implicit Arguments.

Definition is_pred A (rel : A → A → Prop) B a :=
  ∃ b, In b B ∧ clos_refl_trans A rel a b.

Definition depth_metric A (rel: A → A → Prop) V acts :=
  length (filter (mydecf (is_pred rel acts)) V).

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b → a = b ∨ clos_trans T rel a b.
Proof. induction 1; desf; eauto using clos_trans. Qed.

Lemma clos_trans_hbE :
  ∀ lab sb rf a b (HB: clos_trans actid (happens_before lab sb rf) a b),
    happens_before lab sb rf a b.
Proof. induction 1; vauto. Qed.

Lemma length_filter_imp :
  ∀ A (f g : A → Prop) (IMP : ∀ x, f x → g x) l,
    length (filter (mydecf f) l) ≤
    length (filter (mydecf g) l).
Proof.
  unfold mydecf; induction l; ins; desf; ins; eauto; try omega.
  destruct n; eauto.
Qed.

Lemma depth_lt (rel : relation actid) V A B
  (HB : ∀ a, In a A → ¬ In a B →
        ∃ b, In b B ∧ rel a b)
  b (IN : In b B) (NIN: ¬ In b A)
  (NHB: ∀ a, In a A → ¬ clos_trans _ rel b a)
  (SUB: ∀ b, In b B → In b V) :
  depth_metric rel V A < depth_metric rel V B.
Proof.
  unfold depth_metric; ins.
  assert (IMP: ∀ x, is_pred rel A x → is_pred rel B x).
    clear -HB; unfold is_pred, mydecf; ins; desf.
    destruct (classic (In b B)); eauto.
    by exploit HB; eauto; ins; desf; eauto using clos_refl_trans.
  assert (P1: is_pred rel B b).
    by unfold is_pred; desf; eauto using clos_refl_trans.
  assert (P2: ¬ is_pred rel A b).
    clear -NHB NIN; unfold is_pred; intro; desf.
    by apply clos_refl_transD in H0; unfold not in *; desf; eauto.
  assert (IN' : In b V) by eauto.
  eapply In_split in IN'; desf; rewrite !filter_app, !app_length; ins.
  unfold mydecf at 2 6; desf; ins.
  generalize (length_filter_imp _ _ IMP l1), (length_filter_imp _ _ IMP l2).
  ins; omega.
Qed.

Lemma edge_depth_ind lab sb rf V
  (IRR : irreflexive (happens_before lab sb rf) )
  (HC: prefix_closed sb rf V) (P : tagged_edge → Prop) :
  (∀ edge
    (IH: ∀ edge'
            (LT: happens_before lab sb rf (te_src edge') (te_src edge)),
      P edge')
    (IN : In (te_src edge) V),
    P edge) →
  ∀ edge, In (te_src edge) V → P edge.
Proof.
  intros until edge.
  generalize (S (depth_metric (happens_before lab sb rf) V (te_src edge :: nil))),
      (lt_n_Sn (depth_metric (happens_before lab sb rf) V (te_src edge :: nil))).
  intro n'.
  revert edge; induction n'; ins; try omega.
  eapply H; ins; eapply IHn'; ins; eauto using prefix_closed_hb.
  eapply lt_le_trans, lt_n_Sm_le, H0.
  eapply depth_lt; ins; desf; eauto; instantiate;
    intro; desf; [rewrite H2 in *|]; eauto using t_step, t_trans, clos_trans_hbE.
Qed.

Lemma res_get_plus_alloc r r' l :
  res_get (res_plus r r') l ≠ p_bot →
  res_get r l ≠ p_bot ∨ res_get r' l ≠ p_bot.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto.
  right; congruence.
Qed.

Lemma res_get_rsum_alloc rl l :
  res_get (rsum rl) l ≠ p_bot →
  ∃ r, In r rl ∧ res_get r l ≠ p_bot.
Proof.
  induction rl; ins; eapply res_get_plus_alloc in H; desf; eauto.
  specialize (IHrl H); desf; eauto.
Qed.

Lemma incoming_allocated :
  ∀ acts L b l (IN: res_get (incoming acts L b) l ≠ p_bot),
    ∃ te, te_tgt te = Some b ∧ res_get (L te) l ≠ p_bot.
Proof.
  ins; repeat first [apply res_get_plus_alloc in IN; desf|
                     apply res_get_rsum_alloc in IN; desf];
  repeat (rewrite in_map_iff in *; desf); eexists; split; eauto; ins.
Qed.

Lemma res_get_plus_bot r r' (D: res_plus r r' ≠ Rundef) l :
  res_get (res_plus r r') l = p_bot ↔ res_get r l = p_bot ∧ res_get r' l = p_bot.
Proof.
  split; ins; desf.
  2: by apply NNPP; intro X; apply res_get_plus_alloc in X; desf.
  destruct r, r'; ins; desf; ins; inv_lplus l; unfold prot_plus in *;
    desf; split; congruence.
Qed.

Lemma res_get_rsum_bot rl (D: rsum rl ≠ Rundef) l :
  res_get (rsum rl) l = p_bot ↔ ∀ r, In r rl → res_get r l = p_bot.
Proof.
  induction rl; ins.
  rewrite res_get_plus_bot, IHrl; ins.
  2: by destruct a; ins; desf.
  clear; intuition; desf.
Qed.

Lemma guar_allocated :
  ∀ IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l
    (GET: res_get r l = p_bot)
    (NA: ¬ ∃ l' n, act = Aalloc l' n ∧ l' ≤ l ≤ l' + n),
    r_sb +!+ r_rf ≠ Rundef ∧
    res_get r_sb l = p_bot ∧
    res_get r_rf l = p_bot.
Proof.
  destruct act; ins; desf; desf; ins; rewrite ?res_plus_emp_r; try done.

  by destruct r; ins; repeat split; try done; desf; desf; destruct NA;
     eauto 10.

  by repeat split; try done; intro X; rewrite X in *; ins.
  by repeat split; try done; intro X; rewrite X in *; ins.

  repeat split; try done; try (by destruct r).
  unfold res_upd; desf; ins; case eqnP; ins; desf; congruence.

  repeat split; try done; try (by destruct r).
  unfold res_upd; desf; ins; case eqnP; ins; desf; congruence.

  unfold atomic_guar in *; desf; destruct (eqP l0 l); desf; try congruence;
  by split; try eapply res_get_plus_bot; ins; rewrite REQ;
     destruct r; ins; desf; desf.

  unfold atomic_guar in *; desf; destruct (eqP l0 l); desf; try congruence;
  by split; try eapply res_get_plus_bot; ins; rewrite REQ;
     destruct r; ins; desf; desf.
Qed.

Lemma outgoing_allocated :
   ∀ IE acts M amap rf L E edge
     (V: valid_node IE acts M amap rf L E (te_src edge)) l
     (G: res_get (L edge) l ≠ p_bot)
     (IN: ∀ b, te_tgt edge = Some b → In b acts)
     (IN': ∀ sigma a, edge = TescS sigma a → In sigma E)
     (NA: ¬ ∃ l' n, amap (te_src edge) = Aalloc l' n ∧ l' ≤ l ≤ l' + n),
   res_get (incoming acts L (te_src edge)) l ≠ p_bot.
Proof.
  ins; red in V; desf.
  cut (res_get (r +!+ out_esc acts L E (te_src edge)) l ≠ p_bot).
    by clear - VG; red in VG; desf; rewrite VG, VG0.
  clear - GUAR VG G NA IN IN'.
  red in VG; desf.
  intro X; unfold out_esc in *; rewrite !res_get_plus_bot, res_get_rsum_bot in *;
    desf; try (by intro M; rewrite M, ?res_plus_undef in *).
  eapply guar_allocated in GUAR; desf; eauto.
  unfold out_rf, out_sb in *; rewrite !res_get_plus_bot, res_get_rsum_bot in *;
    desf; try (by intro M; rewrite M, ?res_plus_undef in *).
  destruct edge; ins; destruct G; eauto using in_map.
  eapply X0, in_map, in_map_iff; eauto.
Qed.

Lemma nemp_of_get_at r l tau S : res_get r l = p_at tau S → r ≠ res_emp.
Proof.
  red; ins; desf.
Qed.

Lemma nemp_of_get_nbot r l : res_get r l ≠ p_bot → r ≠ res_emp.
Proof.
  red; ins; desf.
Qed.

Hint Resolve nemp_of_get_at nemp_of_get_nbot.

Lemma prefix_closed_pres_in sb rf N a :
  prefix_closed sb rf N →
  In a N →
  pres_in sb rf a N.
Proof.
  unfold prefix_closed, pres_in; ins; desf; eauto.
Qed.

Lemma hb_one :
  ∀ acts amap sb rf L E
    (LR : label_restr acts amap sb rf L E) te b,
  te_tgt te = Some b →
  L te ≠ res_emp →
  happens_before amap sb rf (te_src te) b.
Proof.
  ins; apply NNPP; intro; destruct te, H0; ins; desf;
    apply LR; intro; destruct H1; eauto.
Qed.

Lemma lab_src_in_acts :
  ∀ acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (LR : label_restr acts amap sb rf L E) te
    (G : L te ≠ res_emp),
  In (te_src te) acts.
Proof.
  ins; apply NNPP; intro X.
  assert (Y: L te = res_emp); [|by rewrite Y in *].
  destruct te; ins; eapply LR; eauto; intro HB;
  destruct X; eapply proj1, Consistent_hb_in; eauto.
Qed.

Lemma lab_tgt_in_acts :
  ∀ acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (LR : label_restr acts amap sb rf L E) te
    (G : L te ≠ res_emp) b
    (T : te_tgt te = Some b),
  In b acts.
Proof.
  ins; apply NNPP; intro X.
  assert (Y: L te = res_emp); [|by rewrite Y in *].
  destruct te; ins; eapply LR; eauto; intro HB; desf;
  destruct X; eapply proj2, Consistent_hb_in; eauto.
Qed.

Lemma visible_allocation_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) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) te l
    (G: res_get (L te) l ≠ p_bot) (X: In (te_src te) N),
  ∃ a l' n, may_happens_before amap sb rf a (te_src te) ∧
            amap a = Aalloc l' n ∧
            l' ≤ l ≤ l' + n.
Proof.
  intros; 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 X; ins.
  destruct (classic (∃ l' n, amap (te_src edge) = Aalloc l' n ∧ l' ≤ l ≤ l' + n)).
    desf; repeat eexists; eauto; apply mhbE; eauto.
  assert (K:=G).
  eapply outgoing_allocated, incoming_allocated in K; eauto using lab_tgt_in_acts; desf.
  exploit IH; try eexact K0; ins; desf; eauto; eauto using hb_one.
    by repeat eexists; eauto; eapply mhb_trans, mhbE; eauto using hb_one.
  by ins; apply NNPP; intro; red in LR; desf; rewrite LRescS in G; vauto.
Qed.

Lemma visible_allocation :
  ∀ 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) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) b (IN: pres_in sb rf b N) l
    (G: res_get (incoming acts L b) l ≠ p_bot),
  ∃ a l' n, happens_before amap sb rf a b ∧
            amap a = Aalloc l' n ∧
            l' ≤ l ≤ l' + n.
Proof.
  ins; eapply incoming_allocated in G; desf.
  assert (X: In (te_src te) N).
    eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  exploit visible_allocation_one; eauto; intro; desf.
  repeat eexists; eauto.
  rewrite mhbE in *; desf; eauto using hb_trans, hb_one.
Qed.

Definition is_na r l v := ∃ k, res_get r l = p_na k v.

Lemma res_get_plus_naE r r' l k v :
  res_get (res_plus r r') l = p_na k v →
  ∃ k, res_get r l = p_na k v ∨ res_get r' l = p_na k v.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto;
    try solve [∃ k0; left; congruence | ∃ k; right; congruence].
Qed.

Lemma res_get_rsum_naE rl l k v :
  res_get (rsum rl) l = p_na k v →
  ∃ r k, In r rl ∧ res_get r l = p_na k v.
Proof.
  induction[k] rl; ins; eapply res_get_plus_naE in H; desf; eauto.
  specialize (IHrl _ H); desf; eauto.
Qed.

Lemma is_na_plusE r r' l v :
  is_na (res_plus r r') l v → is_na r l v ∨ is_na r' l v.
Proof.
  unfold is_na; ins; desf; eapply res_get_plus_naE in H; desf; eauto.
Qed.

Lemma is_na_rsumE rl l v :
  is_na (rsum rl) l v → ∃ r, In r rl ∧ is_na r l v.
Proof.
  induction rl; ins; [red in H|eapply is_na_plusE in H]; desf; eauto.
  specialize (IHrl H); desf; eauto.
Qed.

Lemma incoming_na :
  ∀ acts L b l v (IN: is_na (incoming acts L b) l v),
    ∃ te, te_tgt te = Some b ∧ is_na (L te) l v.
Proof.
  ins; repeat first [apply is_na_plusE in IN; desf|
                     apply is_na_rsumE in IN; desf];
  repeat (rewrite in_map_iff in *; desf); eexists; split; eauto; ins.
Qed.

Lemma is_na_plus r r' (D: res_plus r r' ≠ Rundef) l v :
  is_na (res_plus r r') l v ↔
  is_na r l v ∨ is_na r' l v.
Proof.
  split; ins; desf; eauto using is_na_plusE;
  unfold is_na in *; desf;
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; desf;
  try rewrite H in *; eauto.
Qed.

Lemma is_na_rsum rl (D: rsum rl ≠ Rundef) l v :
  is_na (rsum rl) l v ↔ ∃ r, In r rl ∧ is_na r l v.
Proof.
  induction rl; ins; rewrite ?is_na_plus, ?IHrl; try split; ins; desf; eauto.
    by red in H; desf.
  by destruct a; ins; desf.
Qed.

Lemma guar_na_sb :
  ∀ IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l v
    (GET: is_na r_sb l v)
    (NW: ¬ is_writeLV act l v),
    is_na r l v.
Proof.
  destruct act; ins; desf; desf; ins; rewrite ?res_plus_emp_r; try done.

  by unfold is_na in *; desf; destruct r; ins; desf; vauto.
  by unfold is_na in *; desf; destruct r; ins; desf; desf; desf; vauto; destruct NW; desf.
  by unfold is_na in *; desf; destruct r; ins; desf; desf; desf; vauto; destruct NW; desf.

  unfold is_na, atomic_guar in *; desf;
  assert (REQ':= REQ);
  eapply (f_equal (fun f ⇒ res_get f l0)) in REQ'; destruct r; ins;
  destruct (eqnP l0 l); desf; try congruence;
  destruct r_sb; ins; desf; inv_lplus l0; try rewrite GET in *; ins; desf; try congruence;
  eauto using eq_trans.

  unfold is_na, atomic_guar in *; desf;
  assert (REQ':= REQ);
  eapply (f_equal (fun f ⇒ res_get f l0)) in REQ'; destruct r; ins;
  destruct (eqnP l0 l); desf; try congruence;
  destruct r_sb; ins; desf; inv_lplus l0; try rewrite GET in *; ins; desf; try congruence;
  eauto using eq_trans.
Qed.

Lemma guar_na_rf :
  ∀ IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l v
    (GET: is_na r_rf l v)
    (NW: ¬ is_writeLV act l v),
    is_na r l v.
Proof.
  unfold is_na; destruct act; ins; desf; desf; ins; rewrite ?res_plus_emp_r; try done.

  unfold atomic_guar in *; desf; rewrite res_plusC in *;
  assert (REQ':= REQ);
  eapply (f_equal (fun f ⇒ res_get f l0)) in REQ'; destruct r; ins; desf; try congruence;
  destruct r_rf; ins; desf; inv_lplus l0; try rewrite GET in *; ins; desf; try congruence;
  eauto using eq_trans.

  unfold atomic_guar in *; desf; rewrite res_plusC in *;
  assert (REQ':= REQ);
  eapply (f_equal (fun f ⇒ res_get f l0)) in REQ'; destruct r; ins; desf; try congruence;
  destruct r_rf; ins; desf; inv_lplus l0; try rewrite GET in *; ins; desf; try congruence;
  eauto using eq_trans.
Qed.

Lemma guar_def :
  ∀ IE (r_pre r : resource) (act : act) (r_sb r_rf : resource),
  guar IE r_pre r act r_sb r_rf →
  r_sb ≠ Rundef ∧ r_rf ≠ Rundef.
Proof.
  destruct act; ins; desf; desf; try red in AG; desf;
    try (by destruct r; ins);
    try (by destruct r_sb, r_rf).
Qed.

Lemma outgoing_na :
   ∀ IE acts M amap rf L E edge
     (V: valid_node IE acts M amap rf L E (te_src edge)) l v
     (G: is_na (L edge) l v)
     (IN: ∀ b, te_tgt edge = Some b → In b acts)
     (IN': ∀ sigma a, edge = TescS sigma a → In sigma E)
     (NW: ¬ is_writeLV (amap (te_src edge)) l v),
   is_na (incoming acts L (te_src edge)) l v.
Proof.
  ins; red in V; desf.
  cut (is_na (r +!+ out_esc acts L E (te_src edge)) l v).
    by clear - VG; red in VG; desf; rewrite VG, VG0.
  clear - GUAR VG G NW IN IN'.
  red in VG; desf; unfold out_esc in *;
  rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × ).
  destruct edge; ins; eauto 10 using in_map.
    eapply guar_na_sb in GUAR; eauto; unfold out_sb in *; eapply guar_def in GUAR; desc;
    rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.

    eapply guar_na_sb in GUAR; eauto; unfold out_sb in *; eapply guar_def in GUAR; desc;
    rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.

    eapply guar_na_rf in GUAR; eauto; unfold out_rf in *; eapply guar_def in GUAR; desc;
    rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.

    eapply guar_na_rf in GUAR; eauto; unfold out_rf in *; eapply guar_def in GUAR; desc;
    rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.

    right; right;
    rewrite is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.
Qed.

Lemma res_get_plus_na_or_bot r r' l v :
  is_na r l v ∨ res_get r l = p_bot →
  is_na r' l v ∨ res_get r' l = p_bot →
  is_na (r +!+ r') l v ∨ res_get (r +!+ r') l = p_bot.
Proof.
  unfold is_na; ins; destruct r, r'; ins; desf; ins; inv_lplus l;
  rewrite ?H, ?H0 in *; ins; desf; desf; eauto.
Qed.

Lemma res_get_rsum_na_or_bot rl l v :
  (∀ r, In r rl → is_na r l v ∨ res_get r l = p_bot) →
  is_na (rsum rl) l v ∨ res_get (rsum rl) l = p_bot.
Proof.
  induction rl; ins; try eapply res_get_plus_na_or_bot; eauto.
Qed.

Lemma compat_def2 :
  ∀ 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) edge
    (NE : L edge ≠ res_emp) edge'
    (NE': L edge' ≠ res_emp)
    (NEQ : edge ≠ edge')
    (NHB : ∀ b (TGT: te_tgt edge = Some b)
             (MHB: may_happens_before amap sb rf b (te_src edge')), False)
    (NHB': ∀ b (TGT: te_tgt edge' = Some b)
             (MHB: may_happens_before amap sb rf b (te_src edge)), False)
    (DEF : L edge +!+ L edge' = Rundef),
  False.
Proof.
  ins; apply (CC (edge :: edge' :: nil)); ins; rewrite ?res_plus_emp_r;
  desf; desf; eauto; try (by constructor; vauto; intro; ins; desf);
  eapply hb_one in TGT; eauto; rewrite mhbE in *; desf;
  red in CONS; desc; edestruct ACYC; eauto using hb_trans, hb_in_ct.
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 :
  ∀ 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,
  incoming acts L a ≠ Rundef.
Proof.
  red; ins.
  apply (CC (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))).
    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 2 using hb_trans.

  by ins; rewrite !map_app, !rsum_app, !rsum_map_map_filter; ins; apply LR; eauto.
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 ∨
  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 NNPP in X1.
  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 compat_inc_nonsink :
  ∀ 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 edge b
    (E : te_tgt edge = Some b),
  may_happens_before amap sb rf a (te_src edge) ∨
  may_happens_before amap sb rf b a ∨
  L edge +!+ incoming acts L a ≠ Rundef.
Proof.
  ins.
  rewrite !mhbE.
  apply NNPP; intro X.
  apply not_or_and in X; desf.
  apply not_or_and in X; desf.
  apply not_or_and in X0; desf.
  apply not_or_and in X0; desf.
  apply NNPP in X2.
  destruct (classic (L edge = res_emp)) as [EMP|NEMP].
    by rewrite EMP, res_plus_emp_l in *; eapply compat_inc in X2; eauto.
  eapply hb_one in NEMP; eauto.
  apply (CC (edge :: 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; ins; 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; desf; try rewrite in_filter_iff in *; ins; desf;
       rewrite mhbE in *; desf; unfold mydecf in *; desf;
       try solve [eauto 3 using hb_trans | eapply hb_irr; eauto 3 using hb_trans].

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

Definition writeL_pre x :=
  match x with
    | p_bot ⇒ False
    | p_na k v ⇒ k = pe_full
    | _ ⇒ True
  end.

Lemma is_writeL_inc IE acts M amap rf a l L E :
  is_writeL (amap a) l →
  valid_node IE acts M amap rf L E a →
  writeL_pre (res_get (incoming acts L a) l).
Proof.
  unfold valid_node; ins; desf.
  red in GUAR; red in VG; desf; desf; try red in AG; desf; rewrite VG; ins; desf;
  by destruct r; ins; desf; inv_lplus l; red; unfold prot_plus in *; desf; desf.
Qed.

Lemma is_writeL_in IE acts M amap rf a l L E :
  is_writeL (amap a) l →
  valid_node IE acts M amap rf L E a →
  ∃ edge', te_tgt edge' = Some a ∧ res_get (L edge') l ≠ p_bot.
Proof.
  unfold valid_node; ins; desf.
  apply (incoming_allocated acts).
  cut (res_get r l ≠ p_bot).
    red; ins; red in VG; desf; rewrite VG in *; ins.
    destruct r; ins; desf.
    by inv_lplus l; rewrite H1 in *; unfold prot_plus in *; desf.
  destruct (amap a); ins; desf; unfold atomic_guar in *; desf;
  try congruence.
Qed.

Lemma res_plus_is_na_writeL_pre r r' l v :
  is_na r l v →
  writeL_pre (res_get r' l) →
  r +!+ r' = Rundef.
Proof.
  unfold is_na; ins; desf; destruct r, r'; ins; desf.
  inv_lplus l; unfold prot_plus in *; desf; ins; desf.
  destruct k; ins.
Qed.

Lemma visible_na_one :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) te
    (IN : In (te_src te) N) b
    (T : te_tgt te = Some b) l v
    (G : is_na (L te) l v),
  ∃ a,
    << HB : happens_before amap sb rf a b >> ∧
    << WRI: is_writeLV (amap a) l v >> ∧
    << OTH: ∀ a' (W: is_writeL (amap a') l) (N: In a' N)
              (HB1: ¬ may_happens_before amap sb rf b a'),
              may_happens_before amap sb rf a' a >>.
Proof.
  ins; desf.
  assert (MHB: may_happens_before amap sb rf b b) by vauto.
  assert (OTH: ∀ a' (W: is_writeL (amap a') l) (N: In a' N)
              (HB1: happens_before amap sb rf a' b),
              happens_before amap sb rf a' b).
    by ins; rewrite mhbE; eauto.

  revert MHB OTH; generalize b at 2 3.
  revert b G T; 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; unfold NW.
  destruct (classic (is_writeL (amap (te_src edge)) l)).
    desf; repeat eexists; eauto.
    by red in G; desf; eapply hb_one; eauto; intro X; rewrite X in ×.
  { clear IH.
    assert (∀ edge', te_src edge' = te_src edge →
                          is_na (L edge') l v ∨
                          res_get (L edge') l = p_bot).
      ins; destruct (classic (edge = edge')); desf; vauto.
      apply NNPP; intro; apply (CC (edge :: edge' :: nil)).
        by constructor; vauto; ins; intro; desf.
      by red in G; desc; ins; desf; desf;
         try eapply hb_one in T; eauto; try (by intro Z; rewrite Z in *; ins);
         try eapply hb_one in TGT; eauto; try (by intro Z; rewrite Z in *; ins);
         try rewrite H0 in *;
         red in CONS; desc; rewrite mhbE in *; desf; edestruct ACYC;
         eauto using hb_trans, hb_in_ct.
      ins; rewrite res_plus_emp_r.
      destruct (L edge); ins; desf; ins; destruct H2.
      inv_lplus l; unfold is_na, prot_plus in *; ins; desf; vauto.
    assert (is_na (out_sb acts L (te_src edge)) l v ∨
            res_get (out_sb acts L (te_src edge)) l = p_bot).
      eapply res_get_plus_na_or_bot; eauto.
      eapply res_get_rsum_na_or_bot; eauto.
      by intros; repeat (rewrite in_map_iff in *; desf); eauto.
    specialize (V _ IN); red in V; desf; red in GUAR; desf; ins; subst; split; ins;
    unfold is_na, atomic_guar in *; desf;
    rewrite ?GUAR0, ?Gsb in *; ins; rewrite ?res_get_upds in *; desf;
      try (by intro Z; rewrite Z in × ).
  }
  {
    ins; clear IH.
    eapply is_writeL_inc in W; eauto.
    eapply compat_inc_nonsink with (a:=a') in T; eauto; desf.
    by destruct T; eauto using res_plus_is_na_writeL_pre.
  }

  assert (K:=G); red in G; desc.
  eapply outgoing_na, incoming_na in K; eauto; desf.
  2: by ins; eapply lab_tgt_in_acts; eauto; intro Z; rewrite Z in ×.
  assert (K':=K); eapply IH in K'; clear IH; desf; eauto.
  2: by red in K0; desc; eapply hb_one; eauto; intro X; rewrite X in ×.
  2: by eapply mhbE; eauto.
  repeat eexists; eauto.
  eapply hb_trans; eauto.
  by eapply hb_one; eauto; intro X; rewrite X in ×.

  ins; destruct (classic (may_happens_before amap sb rf (te_src edge) a')); eauto.

  ins; apply NNPP; intro X.
  assert (J := is_writeL_inc _ W (V _ N0)); desf.

  eapply compat_inc_nonsink with (a:=a') in T; eauto.
   desf; eauto.
     by rewrite mhbE in *; desf; eauto using hb_irr, hb_trans.
  by destruct T; eapply res_plus_is_na_writeL_pre; vauto.

  by ins; apply NNPP; intro; red in LR; desf; rewrite LRescS in G; vauto.
Qed.

Lemma visible_na :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) (ND: NoDup acts) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l v
    (G : is_na (incoming acts L b) l v),
  ∃ a,
    << HB : happens_before amap sb rf a b >> ∧
    << WRI: is_writeLV (amap a) l v >> ∧
    << OTH: ∀ a' (W: is_writeL (amap a') l) (N: In a' N)
              (NMHB: ¬ may_happens_before amap sb rf b a'),
              may_happens_before amap sb rf a' a >>.
Proof.
  ins; unfold NW; eapply incoming_na in G; desf; eauto.
  assert (X: In (te_src te) N).
    red in G0; desc; eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  eapply visible_na_one; eauto.
Qed.

Lemma res_get_plus_uninitE r r' l :
  res_get (res_plus r r') l = p_uninit →
  res_get r l = p_uninit ∨ res_get r' l = p_uninit.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto;
  try (left; congruence); right; congruence.
Qed.

Lemma res_get_rsum_uninitE rl l :
  res_get (rsum rl) l = p_uninit →
  ∃ r, In r rl ∧ res_get r l = p_uninit.
Proof.
  induction rl; ins; eapply res_get_plus_uninitE in H; desf; eauto.
  specialize (IHrl H); desf; eauto.
Qed.

Lemma res_get_plus_uninit r r' (D: res_plus r r' ≠ Rundef) l :
  res_get (res_plus r r') l = p_uninit ↔
  res_get r l = p_uninit ∨ res_get r' l = p_uninit.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto;
  split; ins; desf;
    try solve [left; congruence | right; congruence | congruence].
Qed.

Lemma res_get_rsum_uninit rl (D: rsum rl ≠ Rundef) l :
  res_get (rsum rl) l = p_uninit ↔
  ∃ r, In r rl ∧ res_get r l = p_uninit.
Proof.
  induction rl; ins; rewrite ?res_get_plus_uninit, ?IHrl; try split; ins; desf; eauto.
  by destruct a; ins; desf.
Qed.

Lemma incoming_uninit :
  ∀ acts L b l (IN: res_get (incoming acts L b) l = p_uninit),
    ∃ te, te_tgt te = Some b ∧ res_get (L te) l = p_uninit.
Proof.
  ins; repeat first [apply res_get_plus_uninitE in IN; desf|
                     apply res_get_rsum_uninitE in IN; desf];
  repeat (rewrite in_map_iff in *; desf); eexists; split; eauto; ins.
Qed.

Lemma mhb_hb_trans:
  ∀ (amap : actid → act) (sb : actid → actid → Prop)
    (rf : actid → option actid) (a b c : actid),
  may_happens_before amap sb rf a b →
  happens_before amap sb rf b c → happens_before amap sb rf a c.
Proof.
  ins; rewrite mhbE in *; desf; eauto using hb_trans.
Qed.

Lemma helper_out_def :
  ∀ a acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts)
    (ND': NoDup E)
    (CC: compat amap sb rf L)
    (LR : label_restr acts amap sb rf L E),
  outgoing acts L E a ≠ Rundef.
Proof.
  ins; intro; eapply (CC (TrfS a :: TsbS a ::
      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 (TescS^~ a) E ++
      map (Tesc a) (filter (mydecf (happens_before amap sb rf a)) (acts)))).
      repeat constructor; try by rewrite ?in_cons_iff, ?in_app_iff, ?in_map_iff; intro; desf.
      rewrite !nodup_app; intuition; try eapply nodup_map; eauto; ins; try congruence;
      unfold disjoint; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; eauto using nodup_filter.
    red in CONS; desf; ins.
    assert (te_src te = a); subst; [|clear IN].
      by clear -IN; ins; desf; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; ins; desf.
    by ins; desf; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; ins; desf;
       rewrite ?filter_In in *; desf; unfold mydecf in *; desf;
       edestruct ACYC; eauto using mhb_hb_trans, hb_in_ct.
  unfold outgoing, out_sb, out_rf, out_esc in H;
  rewrite !res_plusA, !(res_plusAC (L (TrfS _))) in H.
  by ins; rewrite !map_app, !rsum_app, !rsum_map_map_filter; ins;
     apply LR; intro; desf; eauto.
Qed.

Lemma outgoing_uninit :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) edge l
    (GG : res_get (L edge) l = p_uninit),
  res_get (outgoing acts L E (te_src edge)) l = p_uninit.
Proof.
  ins; assert (DEF := helper_out_def (te_src edge) CONS ND ND' CC LR).
  unfold outgoing, out_esc, out_rf, out_sb in ×.
  rewrite !res_get_plus_uninit, !res_get_rsum_uninit;
    try (by intro X; rewrite X, ?res_plus_undef in *).
  assert (∀ b, te_tgt edge = Some b → In b acts).
    by apply (lab_tgt_in_acts CONS LR); ins; intro X; rewrite X in *; ins.
  assert (IN': ∀ sigma a, edge = TescS sigma a → In sigma E).
    by ins; apply NNPP; intro; red in LR; desf; rewrite LRescS in GG; vauto.
  by destruct edge; ins; eauto 10 using in_map.
Qed.

Lemma vnode_uninit :
  ∀ acts M amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) IE edge
    (V: valid_node IE acts M amap rf L E (te_src edge)) l
    (GG : res_get (L edge) l = p_uninit)
    (NA : ¬ ∃ l' n, amap (te_src edge) = Aalloc l' n ∧
                         l' ≤ l ≤ l' + n),
  res_get (incoming acts L (te_src edge)) l = p_uninit.
Proof.
  unfold valid_node; ins; desf.
  cut (res_get (r +!+ out_esc acts L E (te_src edge)) l = p_uninit).
    by clear - VG; red in VG; desc; rewrite VG, VG0.
  rewrite res_get_plus_uninit; [|red in VG; desf; congruence].
  clear VG VrfM VrfS VrfS' RS.
  eapply outgoing_uninit in GG; eauto.
  unfold outgoing in GG; rewrite <- res_plusA in GG.
  apply res_get_plus_uninitE in GG; desf; eauto; left.
  red in GUAR; desf; desf;
    rewrite ?GUAR, ?GUAR0, ?GUAR1, ?res_plus_emp_r in *; ins.

  by destruct r; ins; desf; desf; edestruct NA; eauto 8.
  by destruct r; ins; desf.
  by destruct r; ins; desf.
  by red in AG; desf; rewrite REQ in *; destruct r; ins; desf.
  by red in AG; desf; rewrite REQ in *; destruct r; ins; desf.
Qed.

Lemma is_writeL_out :
  ∀ acts M amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) edge l
    (GG: res_get (L edge) l = p_uninit)
    (W : is_writeL (amap (te_src edge)) l) IE
    (V : valid_node IE acts M amap rf L E (te_src edge)),
  False.
Proof.
  ins; eapply outgoing_uninit in GG; eauto.
  remember (te_src edge) as b; clear edge Heqb.
  red in V; desf.
  unfold outgoing in GG; rewrite <- res_plusA in GG.
  apply res_get_plus_uninitE in GG; desf.

  red in GUAR; desf; desf;
  rewrite ?GUAR, ?GUAR0, ?GUAR1, ?res_plus_emp_r in *; ins; desf.

  by rewrite res_get_upds in *; desf; intro; desf.
  by rewrite res_get_upds in *; desf; intro; desf.
  by red in AG; desf; rewrite REQ, res_get_upds in GG; desf; intro; desf.
  by red in AG; desf; rewrite REQ, res_get_upds in GG; desf; intro; desf.

  assert (GG': res_get r l = p_bot); [|clear GG].
    red in VG; desf; destruct r; ins; desf.
    by inv_lplus l; ins; rewrite GG in *; destruct (pmap l); ins.

  red in GUAR; desf; desf;
  rewrite ?GUAR, ?GUAR0, ?GUAR1, ?res_plus_emp_r in *; ins; desf; try congruence.
  red in AG; desf; congruence.
Qed.

Lemma visible_uninit2 :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l
    (IN: res_get (incoming acts L b) l = p_uninit) a
    (W: is_writeL (amap a) l)
    (PI': pres_in sb rf a N)
    (J : res_get (incoming acts L a) l ≠ p_bot),
    may_happens_before amap sb rf b a.
Proof.
  ins.
  eapply incoming_uninit in IN; desf.
  apply incoming_allocated in J; destruct J as (edge' & J); desf.
  assert (X: In (te_src te) N).
    clear PI'; eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  assert (X': In (te_src edge') N).
    clear PI; eapply pres_in_hb; eauto.
    by eapply hb_one; eauto.
  clear PI PI'; revert b IN IN0; pattern te.
  eapply edge_depth_ind with (lab:=amap) (V:=N); eauto.
    by red in CONS; desc; intros ? ?; edestruct ACYC; eauto.
  clear te X; ins.
  destruct (classic (∃ l' n, amap (te_src edge) = Aalloc l' n ∧ l' ≤ l ≤ l' + n)).
  {
    exploit visible_allocation_one; eauto.
    intro K; desf.
      assert (C:=CONS); red in C; desc.
      pose proof (Ca _ _ _ H _ _ _ K0); desf; try (exfalso; omega).
      rewrite K0 in H; desf.
    apply NNPP; intro T.
    eapply (compat_def2 CONS LR CC) with (edge := edge) (edge' := edge'); eauto.
      by intro Z; rewrite Z in *; desf.
      by intro Z; rewrite Z in *; desf; destruct T; apply mhbE; auto.

      ins; rewrite TGT in *; desf.
      by eapply T, mhb_trans, mhbE; eauto using hb_one.

      ins; rewrite TGT in *; desf.
      eapply hb_one in TGT; eauto.
      by rewrite mhbE in *; desf; try rewrite K in *;
         edestruct ACYC; eapply hb_in_ct; eauto using hb_trans.

      destruct (L edge), (L edge'); ins; desf.
      by inv_lplus l; rewrite IN1 in *; ins; desf.
  }

  assert (IN': res_get (incoming acts L (te_src edge)) l = p_uninit).
    by eapply vnode_uninit; eauto.
  eapply incoming_uninit in IN'; desf.
  exploit (IH te); clear IH; eauto.
    by eapply hb_one; eauto; intro Z; rewrite Z in ×.
  intro; apply NNPP; intro T.
  destruct (classic (te = edge')); desf.
    by eapply is_writeL_out with (edge := edge); eauto.
  destruct (classic (edge = edge')); desf.
    by apply T, mhbE; eauto.

  destruct (classic (happens_before amap sb rf (te_src edge') (te_src edge))).
  {
    eapply (compat_def2 CONS LR CC) with (edge := te) (edge' := edge'); eauto.
      by intro Z; rewrite Z in *; desf.

      ins; rewrite TGT in *; desf.
      by red in CONS; desc; eapply ACYC, hb_in_ct; eauto using mhb_hb_trans.

      ins; rewrite TGT in *; desf.
      eapply hb_one in IN'; eauto; try (by intro Z; rewrite Z in *; ins).
      by red in CONS; desc; eapply ACYC, hb_in_ct; eauto using mhb_hb_trans, mhb_trans.

    destruct (L te), (L edge'); ins; desf.
    by inv_lplus l; unfold prot_plus in *; ins; desf.
  }

  eapply (compat_def2 CONS LR CC) with (edge := edge) (edge' := edge'); eauto.
    by intro Z; rewrite Z in *; desf.

    ins; rewrite TGT in *; desf.
    by eapply T, mhb_trans, mhbE; eauto using hb_one.

    ins; rewrite TGT in *; desf.
    eapply hb_one in TGT; eauto.
    by rewrite mhbE in MHB; desf; eauto using hb_trans.

  destruct (L edge), (L edge'); ins; desf.
  by inv_lplus l; unfold prot_plus in *; ins; desf.
Qed.

Lemma visible_uninit :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND' : NoDup E) L
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l
    (IN: res_get (incoming acts L b) l = p_uninit) a
    (W: is_writeL (amap a) l) (INa: In a N),
    may_happens_before amap sb rf b a.
Proof.
  ins.
  eapply incoming_uninit in IN; desf.
  assert (X: In (te_src te) N).
    eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  clear PI; revert b IN IN0; pattern te.
  eapply edge_depth_ind with (lab:=amap) (V:=N); eauto.
    by red in CONS; desc; intros ? ?; edestruct ACYC; eauto.
  clear te X; ins.
  destruct (classic (∃ l' n, amap (te_src edge) = Aalloc l' n ∧ l' ≤ l ≤ l' + n)).
  {
    assert (J := is_writeL_in _ W (V _ INa)); desf.
    exploit visible_allocation_one; eauto.
      by eapply prefix_closed_hb; eauto using hb_one.
    intro K; desf.
      assert (C:=CONS); red in C; desc.
      pose proof (Ca _ _ _ H _ _ _ K0); desf; try (exfalso; omega).
      rewrite K0 in H; desf.
    apply NNPP; intro T.
    eapply (compat_def2 CONS LR CC) with (edge := edge) (edge' := edge'); eauto.
      by intro Z; rewrite Z in *; desf.
      by intro Z; rewrite Z in *; desf; destruct T; apply mhbE; auto.

      ins; rewrite TGT in *; desf.
      by eapply T, mhb_trans, mhbE; eauto using hb_one.

      ins; rewrite TGT in *; desf.
      eapply hb_one in TGT; eauto.
      by rewrite mhbE in *; desf; try rewrite K in *;
         edestruct ACYC; eapply hb_in_ct; eauto using hb_trans.

      destruct (L edge), (L edge'); ins; desf.
      by inv_lplus l; rewrite IN1 in *; ins; desf.
  }

  assert (IN': res_get (incoming acts L (te_src edge)) l = p_uninit).
    by eapply vnode_uninit; eauto.
  eapply incoming_uninit in IN'; desf.
  exploit (IH te); clear IH; eauto.
    by eapply hb_one; eauto; intro Z; rewrite Z in ×.
  intro; apply NNPP; intro T.
  assert (J := is_writeL_in _ W (V _ INa)); desf.
  destruct (classic (te = edge')); desf.
    by eapply is_writeL_out with (edge := edge); eauto.
  destruct (classic (edge = edge')); desf.
    by apply T, mhbE; eauto.

  destruct (classic (happens_before amap sb rf (te_src edge') (te_src edge))).
  {
    eapply (compat_def2 CONS LR CC) with (edge := te) (edge' := edge'); eauto.
      by intro Z; rewrite Z in *; desf.

      ins; rewrite TGT in *; desf.
      by red in CONS; desc; eapply ACYC, hb_in_ct; eauto using mhb_hb_trans.

      ins; rewrite TGT in *; desf.
      eapply hb_one in IN'; eauto; try (by intro Z; rewrite Z in *; ins).
      by red in CONS; desc; eapply ACYC, hb_in_ct; eauto using mhb_hb_trans, mhb_trans.

    destruct (L te), (L edge'); ins; desf.
    by inv_lplus l; unfold prot_plus in *; ins; desf.
  }

  eapply (compat_def2 CONS LR CC) with (edge := edge) (edge' := edge'); eauto.
    by intro Z; rewrite Z in *; desf.

    ins; rewrite TGT in *; desf.
    by eapply T, mhb_trans, mhbE; eauto using hb_one.

    ins; rewrite TGT in *; desf.
    eapply hb_one in TGT; eauto.
    by rewrite mhbE in MHB; desf; eauto using hb_trans.

  destruct (L edge), (L edge'); ins; desf.
  by inv_lplus l; unfold prot_plus in *; ins; desf.
Qed.