Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas.

Set Implicit Arguments.

Lemma location_does_not_vanish:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge) b (SND: hb_snd edge = Some b)
    hmap (VALID: hmap_valid lab sb rf hmap b) hf (MAP: hmap edge = Hdef hf)
    l (ALL: hf l ≠ HVnone),
  ∃ edge´, << EV´: edge_valid lab sb rf edge´ >> ∧ << CON: b = hb_fst edge´ >> ∧
                ∃ hf´, << MAP´: hmap edge´ = Hdef hf´ >> ∧ << ALL´: hf´ l ≠ HVnone >>.
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desf; desc; try (destruct DISJ; desc); destruct edge; try clear TYP; ins; desf;
    try (by specialize (CONS_RF b); desf; desf; rewrite Heq in *; desf);
    rewrite ?(pU0 _ EV), ?MAP in *; desf.

  {
    eapply hsum_preserves_alloc in pEQ; eauto.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply pOK.
    symmetry in qEQ; eapply hplus_alloc in qEQ; eauto; desf.
    × eapply hsum_alloc in qEQ; eauto; desf.
      repeat (rewrite In_map in *; desf).
      ∃ (hb_sb b x0); repeat split; ins; try congruence.
      by apply qOK.
      eby eexists,.
    × ∃ (hb_sink b); repeat split; ins; try congruence.
      by red; desf.
      eby eexists,.
  }

  {
    ∃ (hb_sb b post); repeat split; ins.
    eexists,; eauto.
    unfold hupd; desf; desf.
  }

  {
    ∃ (hb_sb b post); repeat split; ins.
    eexists,; eauto.
    unfold hupd; desf; desf.
  }

  {
    ∃ (hb_sb b post); repeat split; ins; try congruence.
    eby eexists,.
  }

  
  by rewrite rEQ in MAP; inv MAP.

  {
    eexists (hb_sb _ _); repeat split; ins; eauto.
    rewrite hdef_alt in qD; desf; rewrite qD in ×.
    eexists,; eauto.
    eapply hplus_alloc in pEQ´; eauto; desf.
    × unfold hupd in pEQ´0; desf; desf.
      eapply hplus_preserves_alloc_l in qEQ; eauto.
      unfold hupd; desf; desf.
    × rewrite <- hplusA in qEQ; eapply hplus_preserves_alloc_r in qEQ; eauto.
  }

  {
    red in TRAN; desf.
    rewrite TRAN in ×.
    red in rfsSIM; desf.
    specialize (rfsSIM1 l).
    eapply hsum_preserves_alloc in TRAN; eauto.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply rfsOK.
    rewrite HVsim_alloc in TRAN; eauto.
    rewrite hdef_alt in qD; desf; rewrite qD in ×.
    rewrite hplusAC in qEQ.
    eapply hplus_preserves_alloc_l in qEQ; eauto.
    ∃ (hb_sb b post); repeat split; ins.
    eby eexists,.
  }

  {
    ∃ (hb_sb b post); repeat split; ins.
    eexists,; eauto.
    unfold hupd; desf; desf.
  }

  {
    symmetry in UPD; eapply hplus_alloc in UPD; eauto.
      2: eby rewrite <- initialize_alloc.
    desf.
    × ∃ (hb_sb b post); repeat split; ins.
      eby eexists,.
    × red in TRAN; desf.
      rewrite TRAN in ×.
      red in rfsSIM; desf.
      specialize (rfsSIM1 l).
      rewrite <- HVsim_alloc in UPD0; eauto.
      eapply hplus_alloc in TRAN; eauto; desf.
      + eapply hsum_alloc in TRAN; eauto; desf.
        repeat (rewrite In_map in *; desf).
        ∃ (hb_rf b x0); repeat split; ins; try congruence.
        by apply rfsOK.
        eby eexists,.
      + ∃ (hb_sink b); repeat split; ins; try congruence.
        by red; desf.
        eby eexists,.
  }

  {
    ∃ (hb_sb b post); repeat split; ins.
    assert (SIM: Hsim (Hdef hf) (hmap (hb_sb b post))).
    {
      rewrite pEQ, qEQ.
      apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_r in *).
        by apply Hsim_refl; intro U; rewrite U, ?hplus_undef_r in ×.
      by apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_r in *).
    }
    red in SIM; desf.
    eexists,; eauto.
    rewrite <- HVsim_alloc; eauto.
  }
Qed.

Lemma na_propagates_forward:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV1: edge_valid lab sb rf edge1)
    edge2 (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA: is_nonatomic (hf1 l)) (ALL: hf2 l ≠ HVnone),
  is_nonatomic (hf2 l).
Proof.
  ins; destruct edge1 as [a b´ | a b´ | a];
       destruct edge2 as [b c | b c | b];
       ins; inv CON; red in VALID; desf;
       try (by specialize (CONS_RF c); rewrite EV2, Heq in CONS_RF; desf);
       try (by specialize (CONS_RF b); rewrite EV1, Heq in CONS_RF; desf);
       try (by red in EV2; rewrite Heq in EV2; desf).

  {
    desc.
    eapply hsum_has_nonatomic in pEQ; eauto.
      2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite pOK.
    symmetry in qEQ; eapply hplus_is_nonatomic_full in qEQ; eauto; desf.
    × eapply hsum_is_nonatomic_all in qEQ; desf; try done.
      by do 2 (rewrite In_map; eexists; split; eauto); rewrite qOK.
    × eapply hsum_nalloc_all in qEQ; desf; eauto; try done.
        instantiate (1 := (hmap (hb_sb b c))) in qEQ; congruence.
      by do 2 (rewrite In_map; eexists; split; eauto); rewrite qOK.
  }

  {
    unfold unique in *; desf; rewrite (pU0 a), (qU0 c) in *; try done.
    {
      rewrite MAP2 in qEQ; inv qEQ.
      unfold hupd in *; desf; try done.
      rewrite MAP1 in pEQ; inv pEQ.
    }
    {
      rewrite MAP2 in qEQ; inv qEQ.
      unfold hupd in *; desf; ins.
      × subst l0.
        rewrite MAP1 in pEQ; inv pEQ.
        by rewrite NALL in NA.
      × rewrite MAP1 in pEQ; inv pEQ.
    }
  }

  {
    unfold unique in *; desc; rewrite (pU0 a), (qU0 c) in *; try done; rewrite MAP1, MAP2 in *; destruct DISJ.
    {
      desf.
    }
    {
      desc; clear TYP.
      inv pEQ.
      eapply hplus_is_nonatomic_full in pEQ´; eauto; desf.
      × by exfalso; clear - pEQ´1; unfold hupd in *; desf.
      × symmetry in qEQ; rewrite <- hplusA in qEQ; eapply hplus_has_nonatomic_r in qEQ; eauto; ins.
        inv H.
    }
  }

  {
    unfold unique in *; desc; rewrite (pU0 a), (qU0 c) in *; try done; rewrite MAP1, MAP2 in *; destruct DISJ.
    {
      by unfold hupd in *; desf.
    }
    {
      desc; clear TYP.
      inv pEQ.
      apply (is_nonatomic_initialize _ _ l0) in NA.
      symmetry in UPD.
      eapply hplus_is_nonatomic_full in UPD; eauto; desf.
    }
  }

  {
    desf.
    apply (is_nonatomic_sim (hf1 l)); try done.
    cut (Hsim (Hdef hf1) (Hdef hf2)).
      by clear; ins; red in H; desf.
    unfold unique in *; desc; rewrite (pU0 a), (qU0 c) in *; try done; rewrite MAP1, MAP2, pEQ, qEQ in ×.
    apply hplus_sim; try done.
      by apply Hsim_refl; destruct hF; ins.
    apply hplus_sim; try done.
    by intro CONTRA; rewrite CONTRA, hplus_undef_r in ×.
  }

  {
    desc; destruct DISJ.
    {
      desf.
      rewrite rEQ in MAP2; inv MAP2.
    }
    {
      desc; clear TYP; ins; desf.
      red in TRAN; desf.
      rewrite ((proj2 pU) a) in *; ins.
      rewrite MAP1 in pEQ; inv pEQ.
      apply (is_nonatomic_initialize _ _ l0) in NA.
      symmetry in UPD; rewrite hplusC in UPD.
      eapply hplus_is_nonatomic_full in UPD; eauto; desf.
      × rewrite Hsim_sym in rfsSIM; red in rfsSIM; desf.
        rewrite (is_nonatomic_sim _ (hf´ l) (rfsSIM1 l)) in UPD1.
        eapply hplus_is_nonatomic_full in rfsSIM0; eauto; desf.
        + eapply hsum_is_nonatomic_all in rfsSIM0; desf; eauto; try done.
          by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
        + eapply hsum_nalloc_all in rfsSIM0; desf; eauto; try done.
            instantiate (1 := (Hdef hf2)) in rfsSIM0; congruence.
          by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      × eapply Hsim_nalloc in rfsSIM; eauto; desf.
        symmetry in rfsSIM; eapply hplus_nalloc in rfsSIM; eauto; desf.
        symmetry in rfsSIM; eapply hsum_nalloc_all in rfsSIM; desf; eauto; try done.
          instantiate (1 := (Hdef hf2)) in rfsSIM; congruence.
        by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
    }
  }

  {
    rewrite MAP2 in *; desc.
    eapply hsum_has_nonatomic in pEQ; eauto.
      2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite pOK.
    symmetry in qEQ; eapply hplus_is_nonatomic_full in qEQ; eauto; desf.
  }

  {
    unfold unique in *; desc; rewrite (pU0 a) in *; try done; rewrite MAP1, MAP2 in *; destruct DISJ.
    {
      desf.
      inv sEQ.
    }
    {
      exfalso.
      desc; clear TYP.
      inv pEQ.
      unfold hupd in ALL; desf; desf.
      eapply hplus_is_nonatomic_full in pEQ´; desf; eauto.
      by unfold hupd in pEQ´1; desf.
      by unfold hupd in pEQ´2; desf.
    }
  }

  {
    unfold unique in *; desc; rewrite (pU0 a) in *; try done; rewrite MAP1, MAP2 in *; destruct DISJ.
    {
      desf.
      inv sEQ.
    }
    {
      desc; clear TYP.
      inv pEQ.
      apply (is_nonatomic_initialize _ _ l0) in NA.
      symmetry in UPD; rewrite hplusC in UPD.
      eapply hplus_is_nonatomic_full in UPD; desf; eauto.
      × rewrite Hsim_sym in rfsSIM; red in rfsSIM; desf.
        rewrite (is_nonatomic_sim _ (hf´ l) (rfsSIM1 l)) in UPD1.
        eapply hplus_is_nonatomic_full in rfsSIM0; eauto; desf.
      × eapply Hsim_nalloc in rfsSIM; eauto; desf.
        symmetry in rfsSIM; eapply hplus_nalloc in rfsSIM; eauto; desf.
    }
  }

  {
    unfold unique in *; desc; rewrite (qU0 c) in *; try done; destruct DISJ.
    {
      desf.
      rewrite rEQ in MAP1; inv MAP1.
    }
    {
      desc; clear TYP.
      red in rfsSIM; desf.
      eapply hsum_has_nonatomic in rfsSIM; desf; eauto.
        2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      rewrite (is_nonatomic_hsim l rfsSIM1) in rfsSIM.
      rewrite MAP2, hplusAC in qEQ; symmetry in qEQ.
      eapply hplus_has_nonatomic_l in qEQ; ins; desf; eauto.
    }
  }

  {
    desc; destruct DISJ.
    {
      desf.
      rewrite rEQ in MAP1; inv MAP1.
    }
    {
      desc; clear TYP.
      red in rfsSIM; desf.
      eapply hsum_has_nonatomic in rfsSIM; desf; eauto.
        2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      rewrite (is_nonatomic_hsim l rfsSIM1) in rfsSIM.
      rewrite hdef_alt in qD; desf.
      rewrite qD, <- hplusA in qEQ.
      symmetry in qEQ; apply hplus_def_inv_l in qEQ; desf.
      rewrite hplus_unfold in qEQ; desf.
      specialize (h l); red in h; desf.
      unfold hupd in Heq0; desf; desf.
      rewrite sEQ in MAP2; inv MAP2.
      unfold hupd in ALL; desf; desf.
    }
  }
Qed.

Lemma na_propagates_back:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV1: edge_valid lab sb rf edge1)
    edge2 (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (ALL: hf1 l ≠ HVnone) (NA: is_nonatomic (hf2 l)),
  is_nonatomic (hf1 l).
Proof.
  ins; destruct edge1 as [a b´ | a b´ | a];
       destruct edge2 as [b c | b c | b];
       ins; inv CON; red in VALID; desf;
       try (by specialize (CONS_RF c); rewrite EV2, Heq in CONS_RF; desf);
       try (by specialize (CONS_RF b); rewrite EV1, Heq in CONS_RF; desf);
       try (by red in EV2; rewrite Heq in EV2; desf).

  {
    desc.
    symmetry in qEQ; exploit hplus_def_inv; eauto; intro D; desf.
    rewrite D, D0 in ×.
    eapply hsum_has_nonatomic in D; desf; eauto.
      2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite qOK.
    eapply hplus_has_nonatomic_l in qEQ; ins; desf; eauto.
    eapply hsum_is_nonatomic_all in pEQ; desf; eauto; try done.
    by do 2 (rewrite In_map; eexists; split; eauto); rewrite pOK.
  }

  {
    unfold unique in *; desf; rewrite (pU0 a), (qU0 c) in *; try done;
      rewrite MAP2 in qEQ; inv qEQ; rewrite MAP1 in pEQ; inv pEQ; unfold hupd in NA; desf; desf.
  }

  {
    unfold unique in *; desc; rewrite (pU0 a), (qU0 c) in *; try done; rewrite MAP1, MAP2 in *; destruct DISJ.
    {
      desf.
    }
    {
      desc; clear TYP.
      inv pEQ.
      symmetry in qEQ; eapply hplus_is_nonatomic_full in qEQ; desf; eauto.
      × unfold hupd in qEQ1; desf; desf.
      × eapply hplus_is_nonatomic_full in qEQ0; desf; eauto.
        + unfold hupd in qEQ2; desf; desf.
          apply hplus_def_inv in pEQ´; desf.
          specialize (PLUSv l); unfold hupd in PLUSv; desf; desf; ins.
          congruence.
        + eapply hplus_has_nonatomic_r; ins; eauto.
          congruence.
    }
  }

  {
    unfold unique in *; desc; rewrite (pU0 a), (qU0 c) in *; try done; rewrite MAP1, MAP2 in *; destruct DISJ.
    {
      unfold hupd in *; desf; desf.
      destruct (hf l0); desf.
    }
    {
      desc; clear TYP.
      inv pEQ.
      symmetry in UPD; eapply hplus_has_nonatomic_l in UPD; ins; desf; eauto.
      eby eapply initialize_is_nonatomic.
    }
  }

  {
    desf.
    apply (is_nonatomic_sim _ (hf2 l)); try done.
    cut (Hsim (Hdef hf1) (Hdef hf2)).
      by clear; ins; red in H; desf.
    unfold unique in *; desc; rewrite (pU0 a), (qU0 c) in *; try done; rewrite MAP1, MAP2, pEQ, qEQ in ×.
    apply hplus_sim; try done.
      by apply Hsim_refl; destruct hF; ins.
    apply hplus_sim; try done.
    by intro CONTRA; rewrite CONTRA, hplus_undef_r in ×.
  }

  {
    desc; destruct DISJ.
    {
      desf.
      rewrite rEQ in MAP2; inv MAP2.
    }
    {
      desc; clear TYP TRAN.
      rewrite ((proj2 pU) a) in *; ins.
      rewrite MAP1 in pEQ; inv pEQ.
      red in rfsSIM; desf.
      apply hplus_has_nonatomic_l with (l := l) in rfsSIM; ins; desf.
      × rewrite (is_nonatomic_hsim _ rfsSIM1) in rfsSIM.
        symmetry in UPD.
        eapply hplus_has_nonatomic_r in UPD; ins; desf; eauto.
        eby eapply initialize_is_nonatomic.
      × eapply hsum_has_nonatomic; eauto.
        by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
    }
  }

  {
    rewrite MAP2 in *; desc.
    symmetry in qEQ; eapply hplus_has_nonatomic_r in qEQ; ins; desf; eauto.
    eapply hsum_is_nonatomic_all in pEQ; ins; desf; eauto; try done.
    by do 2 (rewrite In_map; eexists; split; eauto); rewrite pOK.
  }

  {
    unfold unique in *; desc; rewrite (pU0 a) in *; try done; rewrite MAP1, MAP2 in *; destruct DISJ.
    {
      desf.
      inv sEQ.
    }
    {
      desc; inv sEQ; clear - NA.
      unfold hupd in NA; desf; desf.
    }
  }

  {
    unfold unique in *; desc; rewrite (pU0 a) in *; try done; rewrite MAP1, MAP2 in *; destruct DISJ.
    {
      desf.
      inv sEQ.
    }
    {
      desc; clear TYP.
      inv pEQ.
      red in rfsSIM; desf.
      eapply hplus_has_nonatomic_r in rfsSIM; ins; desf; eauto.
      rewrite (is_nonatomic_hsim _ rfsSIM1) in rfsSIM.
      symmetry in UPD.
      eapply hplus_has_nonatomic_r in UPD; ins; desf; eauto.
      eby eapply initialize_is_nonatomic.
    }
  }

  {
    unfold unique in *; desc; rewrite (qU0 c) in *; try done; destruct DISJ.
    {
      desf.
      rewrite rEQ in MAP1; inv MAP1.
    }
    {
      desc; clear TYP.
      rewrite MAP2, hplusAC in qEQ.
      symmetry in qEQ; eapply hplus_is_nonatomic_full in qEQ; ins; desf; eauto.
      × red in rfsSIM; desf.
        rewrite <- (is_nonatomic_hsim _ rfsSIM1) in qEQ1.
        eapply hsum_is_nonatomic_all in rfsSIM; ins; desf; desf; eauto.
        by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      × eapply Hsim_nalloc in rfsSIM; desf; eauto.
        eapply hsum_nalloc_all with (h := Hdef hf1) in rfsSIM; desf; eauto; try done.
        by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
    }
  }

  {
    desc; destruct DISJ.
    {
      desf.
      rewrite rEQ in MAP1; inv MAP1.
    }
    {
      desc; clear TYP.
      rewrite MAP2 in sEQ; inv sEQ; clear - NA.
      unfold hupd in NA; desf; desf.
    }
  }
Qed.

Lemma no_triangle_after_nabla:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV1: edge_valid lab sb rf edge1) edge2 (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA1: is_nonatomic (hf1 l)) (NA2: is_nonatomic (hf2 l)) (LAB1: HVlabeled (hf1 l) HLnabla),
  ¬ HVlabeled (hf2 l) HLtriangle.
Proof.
  ins; intro LAB2.

  ins; unfold hmap_valid, unique in VALID.
  desf; desc; try (destruct DISJ; desc);
    destruct edge1 as [a b´ | a b´ | a], edge2 as [b c | b c | b]; ins; try revert TYP; desf;
    try (by specialize (CONS_RF c); rewrite EV2, Heq in CONS_RF; desf);
    try (by specialize (CONS_RF b); rewrite EV1, Heq in CONS_RF; desf);
    try (by red in EV2; rewrite Heq in EV2; desf);
    rewrite ?(pU0 _ EV1), ?(qU0 _ EV2) in *;
    try (by rewrite rEQ in MAP1; inv MAP1);
    try (by rewrite rEQ in MAP2; inv MAP2).

  {
    eapply hsum_has_nonatomic_eq with (hf := hf1) in pEQ; eauto.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply pOK.
    rewrite <- pEQ in ×.
    symmetry in qEQ; eapply hplus_is_nonatomic_eq in qEQ; eauto; desf.
    × rewrite <- qEQ1 in ×.
      eapply hsum_is_nonatomic_eq with (hf := hf2) in qEQ; eauto.
        2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply qOK.
      desf.
      + rewrite qEQ in LAB2; clear - NA1 LAB1 LAB2.
        destruct (hf0 l); ins; congruence.
      + rewrite qEQ in *; ins.
    × eapply hsum_nalloc_all with (h := Hdef hf2) in qEQ; eauto.
        2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply qOK.
      desf.
      rewrite qEQ3 in *; ins.
  }

  {
    rewrite MAP2 in ×.
    symmetry in qEQ; eapply hplus_has_nonatomic_r_eq in qEQ; eauto; desf.
    rewrite <- qEQ in ×.
    eapply hsum_is_nonatomic_eq with (hf := hf1) in pEQ; eauto; desf.
      3: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply pOK.
    × rewrite pEQ in ×. clear - NA1 LAB1 LAB2. destruct (hf l); ins; congruence.
    × rewrite pEQ in *; ins.
  }

  {
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    unfold hupd in *; desf; desf.
    clear - NA2 LAB1 LAB2; destruct (hf l); ins; congruence.
  }

  {
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    unfold hupd in *; desf; desf.
    clear - NA2 LAB1 LAB2; destruct (hf l); ins; congruence.
  }

  {
    rewrite MAP1, MAP2 in ×.
    inv qEQ.
    clear - NA2 LAB1 LAB2; destruct (hf l); ins; congruence.
  }

  {
    rewrite MAP1, MAP2 in ×.
    inv sEQ.
  }

  {
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    eapply hplus_is_nonatomic_eq in pEQ´; eauto; desf.
      by rewrite <- pEQ´1 in NA1; clear - NA1; unfold hupd in NA1; desf; desf.
    rewrite <- pEQ´2 in ×.
    rewrite <- hplusA in qEQ.
    symmetry in qEQ; eapply hplus_has_nonatomic_r_eq in qEQ; eauto; desf.
    rewrite <- qEQ in ×.
    clear - NA1 LAB1 LAB2; destruct (hf2 l); ins; congruence.
  }

  {
    rewrite sEQ in MAP2.
    inv MAP2.
    clear - NA2; unfold hupd in NA2; desf; desf.
  }

  {
    red in TRAN; desf.
    rewrite TRAN, MAP2 in ×.
    red in rfsSIM; desf.
    eapply hsum_has_nonatomic_eq with (hf := hf1) in TRAN; eauto.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
    specialize (rfsSIM1 l); rewrite TRAN in ×.
    rewrite (is_nonatomic_sim _ _ rfsSIM1) in NA1.
    rewrite hplusAC in qEQ.
    symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto; desf.
    rewrite qEQ in ×.
    clear - NA2 LAB2; unfold HlabeledExact; intro TYP; desf.
    × specialize (TYP0 l); destruct (hf l); ins; congruence.
    × specialize (TYP2 l); destruct (hf l); ins; congruence.
  }

  {
    rewrite sEQ in MAP2.
    inv MAP2.
    clear - NA2; unfold hupd in NA2; desf; desf.
  }

  {
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    unfold hupd in *; desf; desf.
    clear - NA2 LAB1 LAB2; destruct (hf l); ins; congruence.
  }

  {
    rewrite sEQ in MAP2.
    inv MAP2.
  }

  {
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    symmetry in UPD; eapply hplus_has_nonatomic_l_eq in UPD; eauto.
    rewrite <- UPD in *; ins; clear - NA1 LAB1 LAB2.
    unfold initialize, hupd in *; desf; first [rewrite Heq0 in × | destruct (hf l)]; ins; congruence.
  }

  {
    rewrite MAP1 in ×.
    inv pEQ.
    red in TRAN; desf.
    assert (R := hplus_def_inv_l _ _ TRAN); desf; rewrite R in ×.
    eapply hsum_has_nonatomic_eq with (hf := hf2) in R; eauto.
      2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
    rewrite <- R in ×.
    eapply hplus_has_nonatomic_l_eq in TRAN; eauto.
    rewrite <- TRAN in ×.
    ins; clear - TRAN3 LAB2 NA2.
    specialize (TRAN3 l); destruct (hf0 l); ins; congruence.
  }

  {
    rewrite MAP2 in ×.
    red in TRAN; desf.
    eapply hplus_has_nonatomic_r_eq in TRAN; eauto.
    rewrite <- TRAN in ×.
    ins; clear - TRAN3 LAB2 NA2.
    specialize (TRAN3 l); destruct (hf0 l); ins; congruence.
  }

  {
    rewrite MAP1, MAP2 in ×.
    symmetry in pEQ; eapply hplus_is_nonatomic_eq in pEQ; eauto; desf.
    × rewrite <- pEQ1 in ×.
      symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto.
      rewrite qEQ in ×.
      clear - NA1 LAB1 LAB2; destruct (hf0 l); ins; congruence.
    × rewrite <- pEQ2 in ×.
      eapply hplus_is_nonatomic_eq in pEQ0; eauto; desf.
      + rewrite <- pEQ4 in ×.
        clear - NA1 LAB1 RELlabel.
        red in RELlabel; desf.
        specialize (RELlabel0 l); destruct (hf l); ins; congruence.
      + rewrite <- pEQ5 in ×.
        red in ACQsim; desf.
        rewrite (is_nonatomic_sim _ _ (ACQsim1 l)) in NA1.
        rewrite <- hplusA in qEQ.
        symmetry in qEQ; eapply hplus_has_nonatomic_r_eq in qEQ; eauto.
        rewrite qEQ in ×.
        clear - NA2 LAB2 ACQlabel´.
        red in ACQlabel´; desf.
        specialize (ACQlabel´0 l); destruct (hf l); ins; congruence.
  }
Qed.

Lemma step_from_normal:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 edge2 (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA1: is_nonatomic (hf1 l)) (LAB: HVlabeled (hf1 l) HLnormal) (ALL: hf2 l ≠ HVnone),
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnormal ∧ is_sb edge2) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLtriangle ∧ is_sb edge2 ∧ is_release_fence (lab (hb_fst edge2))) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnabla ∧ is_rf edge2 ∧ is_release_write (lab (hb_fst edge2))) ∨
  is_sink edge2.
Proof.
  ins.
  assert (NA2: is_nonatomic (hf2 l)).
    eby eapply na_propagates_forward with (edge1 := edge1) (edge2 := edge2); eauto.

  unfold hmap_valid, unique in VALID.
  desf; desc; try (destruct DISJ; desc);
    destruct edge1 as [a b´ | a b´ | a], edge2 as [b c | b c | b]; ins; try revert TYP; desfh;
    try (by eauto);
    try (by specialize (CONS_RF c); rewrite EV2, Heq in CONS_RF; desf);
    try (by specialize (CONS_RF b); rewrite EV1, Heq in CONS_RF; desf);
    try (by red in EV2; rewrite Heq in EV2; desf);
    rewrite ?(pU0 _ EV1), ?(qU0 _ EV2) in *;
    try (by rewrite rEQ in MAP1; inv MAP1);
    try (by rewrite rEQ in MAP2; inv MAP2);
    try (by left; split; try done; rewrite MAP1, MAP2 in *; inv pEQ; unfold hupd in *; desf; desf).

  {
    left; split; ins.
    eapply hsum_has_nonatomic_eq with (hf := hf1) in pEQ; eauto.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply pOK.
    rewrite <- pEQ in ×.
    symmetry in qEQ; eapply hplus_is_nonatomic_eq in qEQ; eauto; desf.
    × rewrite <- qEQ1 in ×.
      eapply hsum_is_nonatomic_eq with (hf := hf2) in qEQ; eauto; desf.
        2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply qOK.
      by rewrite qEQ.
    × eapply hsum_nalloc_all with (h := Hdef hf2) in qEQ; eauto; desf.
        by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply qOK.
  }

  {
    left; split; try done. clear TYP.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    eapply hplus_is_nonatomic_eq in pEQ´; eauto; desf.
      by rewrite <- pEQ´1 in NA1; clear - NA1; unfold hupd in NA1; desf; desf.
    rewrite <- pEQ´2 in ×.
    rewrite <- hplusA in qEQ.
    symmetry in qEQ; eapply hplus_has_nonatomic_r_eq in qEQ; eauto; desf.
    by rewrite qEQ.
  }

  {
    exfalso.
    red in TRAN; desf.
    specialize (TRAN3 l).
    eapply hsum_has_nonatomic_eq with (hf := hf1) in TRAN; eauto.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
    rewrite TRAN in ×.
    clear - TRAN3 LAB NA1; destruct (hf1 l); ins; congruence.
  }

  {
    left; split; try done.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    symmetry in UPD; eapply hplus_has_nonatomic_l_eq in UPD; eauto.
    clear - LAB UPD NA2.
    rewrite <- UPD in ×.
    unfold initialize, hupd in *; desf; rewrite ?Heq0 in *; ins; congruence.
  }

  {
    destruct (classic (typ = ATrlx ∨ typ = ATacq)) as [T|T].
    {
      ins; exfalso.
      assert (L: HlabeledExact hr HLtriangle) by (desf).
      clear T TYP.
      rewrite MAP1 in *; inv pEQ.
      apply (initialize_preserves_label _ _ l0) in LAB; try done.
      apply (is_nonatomic_initialize _ _ l0) in NA1.
      symmetry in UPD; eapply hplus_is_nonatomic_eq in UPD; eauto; desf.
      × rewrite UPD, <- UPD1 in ×.
        red in rfsSIM; desf.
        specialize (rfsSIM1 l); rewrite UPD2 in ×.
        red in rfsSIM1; desf.
        symmetry in rfsSIM; eapply hplus_nalloc in rfsSIM; eauto; desf.
        symmetry in rfsSIM; eapply hsum_nalloc_all with (h := Hdef hf2) in rfsSIM; eauto; desf.
        by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
      × rewrite <- UPD2 in ×.
      clear - LAB NA1 NA L.
      by red in L; desf; specialize (L0 l); destruct (hf l); ins; congruence.
    }
    {
      red in TRAN; desfh.
      apply not_or_and in T; desc.
      right; right; left; repeat split; try by desf.
      clear TYP; specialize (TRAN3 l).
      assert (R := hplus_def_inv_l _ _ TRAN); desf; rewrite R in ×.
      eapply hsum_has_nonatomic_eq with (hf := hf2) in R; eauto.
        2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
      rewrite <- R in ×.
      eapply hplus_has_nonatomic_l_eq in TRAN; eauto.
      rewrite <- TRAN in ×.
      by apply nonatomic_label.
    }
  }

  {
    destruct (classic (typ = ATsc ∨ typ = ATar)) as [T|T].
    {
      rewrite MAP1, MAP2 in ×.
      revert T.
      symmetry in pEQ; eapply hplus_is_nonatomic_eq in pEQ; eauto; desfh.
      × rewrite <- pEQ1 in ×.
        symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto.
        rewrite qEQ in ×.
        by left; split.
      × rewrite <- pEQ2 in ×.
        eapply hplus_is_nonatomic_eq in pEQ0; eauto; desfh.
        + rewrite <- pEQ4 in ×.
          right; left; repeat split; try by desf.
          clear T.
          red in RELsim; desfh.
          specialize (RELsim1 l).
          rewrite is_nonatomic_sim in NA1; eauto.
          red in RELlabel´; desfh.
          specialize (RELlabel´0 l).
          rewrite nonatomic_label in RELlabel´0; ins.
          symmetry in qEQ; rewrite hplusAC in qEQ.
          eapply hplus_has_nonatomic_l_eq in qEQ; eauto; desfh.
          congruence.
        + rewrite <- pEQ5 in ×.
          red in ACQlabel; desfh.
          specialize (ACQlabel0 l).
          clear - ACQlabel0 LAB NA1; destruct (hf l); ins; congruence.
    }
    apply not_or_and in T; desf.
    {
      rewrite MAP1, MAP2 in ×.
      exploit ACQ; ins; desf.
      rewrite hplus_emp_l in ×.
      symmetry in pEQ; eapply hplus_is_nonatomic_eq in pEQ; eauto; desf.
      × rewrite <- pEQ1 in ×.
        symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto.
        rewrite qEQ in ×.
        by left; split.
      × rewrite <- pEQ2 in ×.
        clear - ACQlabel LAB NA1.
        red in ACQlabel; desf; specialize (ACQlabel0 l); destruct (hf l); ins; desf.
    }
    {
      rewrite MAP1, MAP2 in ×.
      exploit REL; ins; desf.
      rewrite hplus_emp_r in ×.
      symmetry in pEQ; eapply hplus_is_nonatomic_eq in pEQ; eauto; desf.
      × rewrite <- pEQ1 in ×.
        symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto.
        rewrite qEQ in ×.
        by left; split.
      × right; left; repeat split; try done.
        rewrite <- pEQ2 in ×.
        red in RELsim; desf.
        rewrite (is_nonatomic_hsim _ RELsim1) in NA1.
        rewrite hplusAC in qEQ.
        symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto; desf.
        rewrite qEQ.
        clear - RELlabel´ NA1.
        red in RELlabel´; desf; specialize (RELlabel´0 l); destruct (hf l); desf.
    }
  }
Qed.

Lemma step_from_nabla:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 edge2 (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA1: is_nonatomic (hf1 l)) (LAB: HVlabeled (hf1 l) HLnabla) (ALL: hf2 l ≠ HVnone),
  (HVlabeled (hf2 l) HLnabla ∧ ¬ is_rf edge2) ∨
  (is_rf edge1 ∧ HVlabeled (hf2 l) HLnormal ∧ ¬ is_rf edge2 ∧ is_acquire_read (lab (hb_fst edge2))) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnormal ∧ is_sb edge2 ∧ is_acquire_fence (lab (hb_fst edge2))).
Proof.
  ins.
  assert (NA2: is_nonatomic (hf2 l)).
    eby eapply na_propagates_forward with (edge1 := edge1) (edge2 := edge2); eauto.

  unfold hmap_valid, unique in VALID.
  desf; desc; try (destruct DISJ; desc);
    destruct edge1 as [a b´ | a b´ | a], edge2 as [b c | b c | b]; ins; try revert TYP; desfh;
    try (by eauto);
    try (by rewrite sEQ in MAP2; inv MAP2);
    try (by specialize (CONS_RF c); rewrite EV2, Heq in CONS_RF; desf);
    try (by specialize (CONS_RF b); rewrite EV1, Heq in CONS_RF; desf);
    try (by red in EV2; rewrite Heq in EV2; desf);
    rewrite ?(pU0 _ EV1), ?(qU0 _ EV2) in *;
    try (by rewrite rEQ in MAP1; inv MAP1);
    try (by rewrite rEQ in MAP2; inv MAP2);
    try (by left; split; try done; rewrite MAP1, MAP2 in *; inv pEQ; unfold hupd in *; desf; desf;
            instantiate; eauto).

  {
    left; split; ins; eauto.
    eapply hsum_has_nonatomic_eq with (hf := hf1) in pEQ; eauto.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply pOK.
    rewrite <- pEQ in ×.
    symmetry in qEQ; eapply hplus_is_nonatomic_eq in qEQ; eauto; desf.
    × rewrite <- qEQ1 in ×.
      eapply hsum_is_nonatomic_eq with (hf := hf2) in qEQ; eauto; desf.
        2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply qOK.
      by rewrite qEQ.
    × eapply hsum_nalloc_all with (h := Hdef hf2) in qEQ; eauto; desf.
        by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply qOK.
  }

  {
    left; split; ins; eauto.
    eapply hsum_has_nonatomic_eq with (hf := hf1) in pEQ; eauto.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply pOK.
    rewrite <- pEQ in ×.
    symmetry in qEQ; eapply hplus_is_nonatomic_eq in qEQ; eauto; desf.
    × rewrite qEQ0 in *; desf.
    × rewrite qEQ0 in *; desf.
      by rewrite qEQ2; eauto.
  }

  {
    left; split; ins; eauto.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    unfold hupd in *; desf; desf.
    rewrite NALL in NA1; desf.
  }

  {
    left; split; eauto. clear TYP.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    eapply hplus_is_nonatomic_eq in pEQ´; eauto; desf.
      by rewrite <- pEQ´1 in NA1; clear - NA1; unfold hupd in NA1; desf; desf.
    rewrite <- pEQ´2 in ×.
    rewrite <- hplusA in qEQ.
    symmetry in qEQ; eapply hplus_has_nonatomic_r_eq in qEQ; eauto; desf.
    by rewrite qEQ.
  }

  {
    red in TRAN; desfh.
    rewrite TRAN in ×.
    eapply hsum_has_nonatomic_eq with (hf := hf1) in TRAN; eauto; desfh.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
    rewrite <- TRAN in ×.
    red in rfsSIM; desc.
    inv rfsSIM.
    rewrite (is_nonatomic_hsim _ rfsSIM1) in NA1.
    rewrite MAP2, hplusAC in qEQ.
    symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto.
    rewrite qEQ in ×.
    ins; desfh.
    × red in TYP; desc; inv TYP; specialize (TYP0 l); eapply nonatomic_label in TYP0; eauto.
    × red in TYP1; desc; inv TYP1; specialize (TYP2 l).
      right; left; repeat split; desf; eauto.
      eby eapply nonatomic_label.
  }

  {
    exfalso.
    rewrite MAP2 in sEQ; inv sEQ.
    clear - NA2; unfold hupd in NA2; desf; desf.
  }

  {
    left; split; eauto.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    unfold hupd in *; desf; desf.
    clear - LAB IV; red in LAB; desf.
  }

  {
    left; split; eauto.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    symmetry in UPD; eapply hplus_has_nonatomic_l_eq in UPD; eauto.
    clear - LAB UPD NA2.
    rewrite <- UPD in ×.
    unfold initialize, hupd in *; desf; rewrite ?Heq0 in *; ins; congruence.
  }

  {
    red in TRAN; desfh.
    assert (R := hplus_def_inv_l _ _ TRAN); desf; rewrite TRAN, R in ×.
    eapply hsum_has_nonatomic_eq with (hf := hf2) in R; eauto.
      2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
    rewrite <- R in ×.
    eapply hplus_has_nonatomic_l_eq in TRAN; eauto.
    rewrite <- TRAN in ×.
    red in rfsSIM; desc.
    inv rfsSIM.
    rewrite (is_nonatomic_hsim _ rfsSIM1) in NA2.
    symmetry in UPD; eapply hplus_has_nonatomic_r_eq in UPD; eauto.
    rewrite MAP1 in pEQ.
    inv pEQ.
    clear - UPD LAB NA1; unfold HlabeledExact; ins; exfalso; desf.
    × specialize (TYP0 l). rewrite <- UPD in ×.
      unfold HVlabeled, initialize, hupd in *; desf.
    × specialize (TYP2 l). rewrite <- UPD in ×.
      unfold HVlabeled, initialize, hupd in *; desf.
  }

  {
    left; clear TYP.
    red in TRAN; desfh.
    rewrite MAP2 in TRAN.
    eapply hplus_has_nonatomic_r_eq in TRAN; eauto.
    rewrite <- TRAN in ×.
    specialize (TRAN3 l).
    rewrite nonatomic_label in TRAN3; eauto.
  }

  {
    rewrite MAP1, MAP2 in ×.
    symmetry in pEQ; eapply hplus_is_nonatomic_eq in pEQ; eauto; desfh.
    × rewrite <- pEQ1 in ×.
      symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto.
      rewrite qEQ in *; eauto.
    × rewrite <- pEQ2 in ×.
      eapply hplus_is_nonatomic_eq in pEQ0; eauto; desfh.
      + exfalso.
        rewrite <- pEQ4 in ×.
        clear - RELlabel LAB NA1.
        red in RELlabel; desf; specialize (RELlabel0 l); destruct (hf l); ins; desf.
      + rewrite <- pEQ5 in ×.
        red in ACQsim; desfh.
        specialize (ACQsim1 l).
        rewrite is_nonatomic_sim in NA1; eauto.
        red in ACQlabel´; desfh.
        specialize (ACQlabel´0 l).
        rewrite nonatomic_label in ACQlabel´0; eauto.
        symmetry in qEQ; rewrite <- hplusA in qEQ; eapply hplus_has_nonatomic_r_eq in qEQ; eauto.
        rewrite qEQ in ×.
        right; right; repeat split; try done.
        desf.
        exploit REL; ins.
        inv x0.
        clear - ACQsim1 ALL; red in ACQsim1; desf.
  }
Qed.

Lemma step_from_triangle:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 edge2 (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA1: is_nonatomic (hf1 l)) (LAB: HVlabeled (hf1 l) HLtriangle) (ALL: hf2 l ≠ HVnone),
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLtriangle ∧ ¬ is_rf edge2) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnabla ∧ is_rf edge2 ∧ is_write (lab (hb_fst edge2))) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnabla ∧ is_sink edge2).
Proof.
  ins.
  assert (NA2: is_nonatomic (hf2 l)).
    eby eapply na_propagates_forward with (edge1 := edge1) (edge2 := edge2); eauto.

  unfold hmap_valid, unique in VALID.
  desf; desc; try (destruct DISJ; desc);
    destruct edge1 as [a b´ | a b´ | a], edge2 as [b c | b c | b]; ins; try revert TYP; desfh;
    try (by eauto);
    try (by rewrite sEQ in MAP2; inv MAP2);
    try (by specialize (CONS_RF c); rewrite EV2, Heq in CONS_RF; desf);
    try (by specialize (CONS_RF b); rewrite EV1, Heq in CONS_RF; desf);
    try (by red in EV2; rewrite Heq in EV2; desf);
    rewrite ?(pU0 _ EV1), ?(qU0 _ EV2) in *;
    try (by rewrite rEQ in MAP1; inv MAP1);
    try (by rewrite rEQ in MAP2; inv MAP2);
    try (by left; split; try done; rewrite MAP1, MAP2 in *; inv pEQ; unfold hupd in *; desf; desf;
            instantiate; eauto).

  {
    left; split; ins.
    eapply hsum_has_nonatomic_eq with (hf := hf1) in pEQ; eauto.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply pOK.
    rewrite <- pEQ in ×.
    symmetry in qEQ; eapply hplus_is_nonatomic_eq in qEQ; eauto; desf.
    × rewrite <- qEQ1 in ×.
      eapply hsum_is_nonatomic_eq with (hf := hf2) in qEQ; eauto; desf.
        2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply qOK.
      by rewrite qEQ; eauto.
    × eapply hsum_nalloc_all with (h := Hdef hf2) in qEQ; eauto; desf.
        by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply qOK.
  }

  {
    left; split; ins.
    eapply hsum_has_nonatomic_eq with (hf := hf1) in pEQ; eauto.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply pOK.
    rewrite <- pEQ in ×.
    symmetry in qEQ; eapply hplus_is_nonatomic_eq in qEQ; eauto; desf.
    × rewrite qEQ0 in *; desf.
    × rewrite qEQ0 in *; desf.
      by rewrite qEQ2; eauto.
  }

  {
    left; split; ins.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    unfold hupd in *; desf; desf.
    rewrite NALL in NA1; desf.
    eauto.
  }

  {
    left; split; try done. clear TYP.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    eapply hplus_is_nonatomic_eq in pEQ´; eauto; desf.
      by rewrite <- pEQ´1 in NA1; clear - NA1; unfold hupd in NA1; desf; desf.
    rewrite <- pEQ´2 in ×.
    rewrite <- hplusA in qEQ.
    symmetry in qEQ; eapply hplus_has_nonatomic_r_eq in qEQ; eauto; desf.
    by rewrite qEQ; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    specialize (TRAN3 l).
    eapply hsum_has_nonatomic_eq with (hf := hf1) in TRAN; eauto; desfh.
      2: by rewrite <- MAP1; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
    rewrite TRAN in ×.
    clear - TRAN3 NA1 LAB.
    red in LAB; desf.
  }

  {
    exfalso.
    rewrite MAP2 in sEQ; inv sEQ.
    clear - NA2; unfold hupd in NA2; desf; desf.
  }

  {
    left; split; try done.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    unfold hupd in *; desf; desf.
    clear - LAB IV; red in LAB; desf.
    eauto.
  }

  {
    left; split; try done.
    rewrite MAP1, MAP2 in ×.
    inv pEQ.
    symmetry in UPD; eapply hplus_has_nonatomic_l_eq in UPD; eauto.
    clear - LAB UPD NA2.
    rewrite <- UPD in ×.
    unfold initialize, hupd in *; desf; rewrite ?Heq0 in *; ins; split; congruence.
  }

  {
     right; left; clear TYP.
     red in TRAN; desfh.
     assert (R := hplus_def_inv_l _ _ TRAN); desc; rewrite R in ×.
     eapply hsum_has_nonatomic_eq with (hf := hf2) in R; eauto.
       2: by rewrite <- MAP2; do 2 (rewrite In_map; eexists,; eauto); apply rfsOK.
     rewrite <- R in ×.
     eapply hplus_has_nonatomic_l_eq in TRAN; eauto.
     rewrite <- TRAN in ×.
     specialize (TRAN3 l).
     rewrite nonatomic_label in TRAN3; eauto.
  }


  {
    right; right; clear TYP.
    rewrite MAP2 in TRAN.
    red in TRAN; desfh.
    eapply hplus_has_nonatomic_r_eq in TRAN; eauto.
    rewrite <- TRAN in ×.
    specialize (TRAN3 l).
    rewrite nonatomic_label in TRAN3; eauto.
  }

  {
    rewrite MAP1, MAP2 in ×.
    symmetry in pEQ; eapply hplus_is_nonatomic_eq in pEQ; eauto; desfh.
    × rewrite <- pEQ1 in ×.
      symmetry in qEQ; eapply hplus_has_nonatomic_l_eq in qEQ; eauto.
      rewrite qEQ in *; eauto.
    × rewrite <- pEQ2 in ×.
      eapply hplus_is_nonatomic_eq in pEQ0; eauto; desfh.
      + exfalso.
        rewrite <- pEQ4 in ×.
        clear - RELlabel LAB NA1.
        red in RELlabel; desf; specialize (RELlabel0 l); destruct (hf l); ins; desf.
      + exfalso.
        rewrite <- pEQ5 in ×.
        clear - ACQlabel LAB NA1.
        red in ACQlabel; desf; specialize (ACQlabel0 l); destruct (hf l); ins; desf.
  }
Qed.