Require Import List Vbase Relations ExtraRelations actions c11.
Require Import ClassicalDescription.
Set Implicit Arguments.

Lemma release_seq_mon_sb :
  forall mt2 lab sb rf mo a b (HB: release_seq mt2 lab sb rf mo a b)
    (sb' : relation actid) (MON: forall x y (SB: sb x y), sb' x y),
    release_seq mt2 lab sb' rf mo a b.
Proof.
  unfold release_seq, release_seq_elem, NW; ins; desf; desf; eauto;
  unfold same_thread in *;
  try by
  right; repeat split;
  ins; desf; eauto 8 using clos_trans_mon; exploit HB1; eauto; ins; desf;
  eauto 8 using clos_trans_mon.

  induction HB; destruct mt2 as [[]?]; desf; ins; desf; ins;
  eauto using release_seq_alt.
  red in RSthr; ins; eapply clos_trans_mon in RSthr; try eassumption; vauto.
Qed.

Lemma happens_before_mon_sb :
  forall mt2 lab sb asw rf mo a b (HB: happens_before mt2 lab sb asw rf mo a b)
    (sb' : relation actid) (MON: forall x y (SB: sb x y), sb' x y),
    happens_before mt2 lab sb' asw rf mo a b.
Proof.
  unfold happens_before; ins; induction HB as [? ? []|]; vauto;
    constructor 1; eauto;
      unfold synchronizes_with, NW in *; desf;
      eauto 21 using clos_trans_mon, release_seq_mon_sb.
Qed.

Lemma release_seq_mon_rf :
  forall mt2 lab sb rf mo a b (HB: release_seq mt2 lab sb rf mo a b)
    rf' (M: forall c d (RF: rf c = Some d), rf' c = Some d),
    release_seq mt2 lab sb rf' mo a b.
Proof.
  unfold release_seq, release_seq_elem, NW; ins; desf; desf; eauto.
  induction HB; desf; destruct mt2; ins; desf;
  eauto using release_seq_alt.
Qed.

Lemma happens_before_mon_rf :
  forall rf rf' (M: forall c d (RF: rf c = Some d), rf' c = Some d)
    mt2 lab sb asw mo a b (HB : happens_before mt2 lab sb asw rf mo a b),
    happens_before mt2 lab sb asw rf' mo a b.
Proof.
  unfold happens_before; ins; induction HB as [? ? []|]; vauto;
    constructor 1; eauto;
      unfold synchronizes_with, NW in *; desf;
      eauto 20 using release_seq_mon_rf.
Qed.

Definition restrict_rf_once mt2 lab sb asw rf mo a :=
  if excluded_middle_informative
    (exists b l, happens_before mt2 lab sb asw rf mo b a
                 /\ is_writeL (lab b) l /\ is_readL (lab a) l)
  then rf a else None.

Definition restrict_measure acts (rf : actid -> option actid) :=
  length (filter (fun x => match rf x with Some _ => true | None => false end) acts).

Lemma restrict_measure_rf :
  forall mt2 lab sb asw rf mo acts,
    restrict_measure acts (restrict_rf_once mt2 lab sb asw rf mo)
    <= restrict_measure acts rf.
Proof.
  unfold restrict_measure, restrict_rf_once; induction acts; ins; desf; ins; omega.
Qed.

Lemma restrict_measure_rf_dec :
  forall mt2 lab sb asw rf mo acts
         (INA: forall a b, rf a = Some b -> In a acts)
         (NEQ: restrict_rf_once mt2 lab sb asw rf mo <> rf),
    restrict_measure acts (restrict_rf_once mt2 lab sb asw rf mo)
    < restrict_measure acts rf.
Proof.
  ins; assert (H: exists x y, In x acts /\ rf x = Some y /\
                           restrict_rf_once mt2 lab sb asw rf mo x = None).
  { apply NNPP; intro; destruct NEQ; extensionality z; apply NNPP; intro.
    destruct H; exists z; specialize (INA z); unfold restrict_rf_once in *; desf.
    by destruct (rf z); ins; eauto.
  }
  desf; clear INA NEQ; induction acts; ins; desf.
    clear IHacts; pose proof (restrict_measure_rf mt2 lab sb asw rf mo acts).
    unfold restrict_measure in *; ins; desf; ins; omega.
  specialize (IHacts H).
  unfold restrict_measure, restrict_rf_once in *; ins; desf; ins; omega.
Qed.

Fixpoint restrict_rf_n n mt2 lab sb asw rf mo :=
  match n with
    | 0 => rf
    | S n => restrict_rf_once mt2 lab sb asw
               (restrict_rf_n n mt2 lab sb asw rf mo) mo
  end.

Lemma restrict_rf_nC :
  forall mt2 lab sb asw mo n rf,
    restrict_rf_once mt2 lab sb asw (restrict_rf_n n mt2 lab sb asw rf mo) mo =
    restrict_rf_n n mt2 lab sb asw (restrict_rf_once mt2 lab sb asw rf mo) mo.
Proof.
  by induction n; ins; rewrite IHn.
Qed.

Lemma restrict_rf_n_fix_helper :
  forall mt2 lab sb asw mo acts n rf
     (INA: forall a b, rf a = Some b -> In a acts),
    restrict_rf_n (S n) mt2 lab sb asw rf mo = restrict_rf_n n mt2 lab sb asw rf mo
    \/ restrict_measure acts (restrict_rf_n n mt2 lab sb asw rf mo) + n
       <= restrict_measure acts rf.
Proof.
  induction n; ins; try (right; omega).
  rewrite restrict_rf_nC.
  exploit (IHn (restrict_rf_once mt2 lab sb asw rf mo)); ins; desf; eauto.
    by unfold restrict_rf_once in H; desf; eauto.
  apply NNPP; intro X; apply not_or_and in X; desf.
  destruct X; rewrite <- restrict_rf_nC at 2; do 2 f_equal; apply NNPP; intro X.
  eapply restrict_measure_rf_dec with (acts := acts) in X; ins.
  destruct X0; omega.
Qed.

Lemma restrict_rf_n_fix_helper2 :
  forall mt2 lab sb asw mo acts n rf
     (INA: forall a b, rf a = Some b -> In a acts)
     (GT: length acts < n),
    restrict_rf_n (S n) mt2 lab sb asw rf mo
    = restrict_rf_n n mt2 lab sb asw rf mo.
Proof.
  ins; eapply restrict_rf_n_fix_helper in INA; des; [by apply INA|].
  cut (restrict_measure acts rf <= length acts); [omega|].
  clear; unfold restrict_measure; induction acts; ins; desf; ins; omega.
Qed.

Definition restrict_rf mt2 (acts : list actid) lab sb asw rf mo :=
  restrict_rf_n (S (length acts)) mt2 lab sb asw rf mo.

Lemma restrict_rf_n_unchanged :
  forall mt2 lab sb asw n rf mo a b l,
    happens_before mt2 lab sb asw (restrict_rf_n n mt2 lab sb asw rf mo) mo b a ->
    is_writeL (lab b) l ->
    is_readL (lab a) l ->
  restrict_rf_n n mt2 lab sb asw rf mo a = rf a.
Proof.
  induction n; ins.
  unfold restrict_rf_once; desf; ins; desf; eauto.
  destruct n0; repeat eexists; eauto.
  eapply happens_before_mon_rf, H; unfold restrict_rf_once; ins; desf.
Qed.

Lemma restrict_rf_unfold :
  forall mt2 acts rf lab sb asw mo
         (FIN: ExecutionFinite acts lab sb asw)
         (Crf: ConsistentRF lab rf) a,
  restrict_rf mt2 acts lab sb asw rf mo a =
  if excluded_middle_informative
    (exists b l, happens_before mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo b a
                 /\ is_writeL (lab b) l /\ is_readL (lab a) l)
  then rf a else None.
Proof.
  ins; unfold restrict_rf at 1.
  rewrite <- (restrict_rf_n_fix_helper2) with (acts:=acts); ins.
  unfold restrict_rf; unfold restrict_rf_once at 1; ins; desf; desf.
  eapply restrict_rf_n_unchanged with (n := S _); eauto.
  eapply finiteRF in H; desf; eauto.
Qed.

Lemma restrict_rf_mon :
  forall mt2 acts lab sb asw rf mo a b,
    restrict_rf mt2 acts lab sb asw rf mo a = Some b ->
    rf a = Some b.
Proof.
  unfold restrict_rf; intros until 0; induction (S _); ins.
  unfold restrict_rf_once in *; desf; ins; desf; eauto.
Qed.

Lemma happens_before_restrict_rf :
  forall mt2 acts lab sb asw rf mo a b,
    happens_before mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo a b ->
    happens_before mt2 lab sb asw rf mo a b.
Proof.
  eauto using happens_before_mon_rf, restrict_rf_mon.
Qed.

Theorem Consistent_restrict_rf :
  forall mt (MT: mt <> MTorig) mt2 mtsc acts lab sb dsb asw rf mo sc,
    Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc ->
  Consistent mt mt2 mtsc acts lab sb dsb asw (restrict_rf mt2 acts lab sb asw rf mo) mo sc.
Proof.
  unfold Consistent, Semiconsistent; ins; desf; unfold NW; intuition.
  by repeat red; intros; eapply IRR; ins; desf;
     eauto using happens_before_restrict_rf.

  red in ACYC; red; desf; unfold rfna in *; try (by exfalso; eauto);
  by repeat red; intros; desf; ins; eapply clos_trans_mon, ACYC in H; ins; desf;
     eauto using happens_before_restrict_rf; rewrite restrict_rf_unfold in *; desf; eauto.
  by repeat red; ins; eapply CmoH; eauto using happens_before_restrict_rf.
  by red in Csc; desf; red; intuition; repeat red; ins; eapply Chbsc;
     eauto using happens_before_restrict_rf.
  by red; ins; rewrite restrict_rf_unfold in * |-; desf; edestruct Cscr; vauto; desf;
     eauto using happens_before_restrict_rf.
  by intro a; rewrite restrict_rf_unfold at 1; ins; desf;
     eauto 8 using happens_before_restrict_rf.
  by red; ins; rewrite restrict_rf_unfold in * |-; unfold NW; desf; desf;
     eauto 8 using happens_before_restrict_rf.
  by red; ins; rewrite restrict_rf_unfold in *; ins; desf; eapply Crf in RF; desf; unfold NW;
     eauto 8 using happens_before_restrict_rf.
  by red; ins; rewrite restrict_rf_unfold in *; ins; desf; eapply CrfH in RF; desf; unfold NW;
     eauto 8 using happens_before_restrict_rf.
  by red; ins; rewrite restrict_rf_unfold in *; desf; eapply Crr;
     eauto using happens_before_restrict_rf.
  by red; ins; rewrite restrict_rf_unfold in *; desf; eapply Cwr;
     eauto using happens_before_restrict_rf.
  by red; ins; rewrite restrict_rf_unfold in *; desf; eapply Crw;
     eauto using happens_before_restrict_rf.
  by red; ins; rewrite restrict_rf_unfold in *; desf; eapply Crmw;
     eauto using happens_before_restrict_rf.
Qed.

Theorem racy_restrict_rf mt2 acts lab sb asw rf mo :
  racy mt2 lab sb asw rf mo ->
  racy mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo.
Proof.
  ins; unfold racy in *; desc; unnw; repeat (eexists; try edone);
  eauto using happens_before_restrict_rf.
Qed.

Corollary race_free_restrict_rf mt2 acts lab sb asw rf mo :
  race_free mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo ->
  race_free mt2 lab sb asw rf mo.
Proof.
  rewrite !race_free_iff_not_racy; eauto using racy_restrict_rf.
Qed.

Definition RATord x y :=
  match x, y with
    | RATna, RATna => true
    | RATna, _ => false
    | _, RATna => false
    | RATrlx, _ => true
    | _, RATrlx => false
    | RATacq, _ => true
    | _, RATacq => false
    | RATsc, RATsc => true
  end.

Definition WATord x y :=
  match x, y with
    | WATna, WATna => true
    | WATna, _ => false
    | _, WATna => false
    | WATrlx, _ => true
    | _, WATrlx => false
    | WATrel, _ => true
    | _, WATrel => false
    | WATsc, WATsc => true
  end.

Definition UATord x y :=
  match x, y with
    | UATrlx, _ => true
    | _, UATrlx => false
    | UATacq, UATrel => false
    | UATacq, _ => true
    | UATrel, UATacq => false
    | UATrel, _ => true
    | UATrel_acq, UATrel_acq => true
    | UATrel_acq, UATsc => true
    | UATsc, UATsc => true
    | _, _ => false
  end.

Definition FATord x y :=
  match x, y with
    | FATacq, FATrel => false
    | FATacq, _ => true
    | FATrel, FATacq => false
    | FATrel, _ => true
    | FATrel_acq, FATrel_acq => true
    | FATrel_acq, FATsc => true
    | FATsc, FATsc => true
    | _, _ => false
  end.

Definition act_ord x y :=
  match x, y with
    | Askip tid, Askip tid' => tid = tid'
    | Askip tid, Afence tid' typ => tid = tid'
    | Aalloc tid l n, Aalloc tid' l' n' =>
      tid = tid' /\ l = l' /\ n = n'
    | Aload tid typ l v, Aload tid' typ' l' v' =>
      tid = tid' /\ RATord typ typ' /\ l = l' /\ v = v'
    | Astore tid typ l v, Astore tid' typ' l' v' =>
      tid = tid' /\ WATord typ typ' /\ l = l' /\ v = v'
    | Armw tid typ l v w, Armw tid' typ' l' v' w' =>
      tid = tid' /\ UATord typ typ' /\ l = l' /\ v = v' /\ w = w'
    | Afence tid typ, Afence tid' typ' =>
      tid = tid' /\ FATord typ typ'
    | _, _ => False
  end.

Lemma act_ord_refl x : act_ord x x.
Proof. destruct x; ins; desf; ins; destruct typ; ins. Qed.

Section act_ord_lemmas.

Variables x y : act.
Hypothesis (AO : act_ord x y).

Ltac tac :=
  generalize AO; unfold act_ord; desf; ins; desf;
  match goal with
   | typ : write_access_type |- _ => solve [destruct typ; ins; desf]
   | typ : read_access_type |- _ => solve [destruct typ; ins; desf]
   | typ : rmw_access_type |- _ => solve [destruct typ; ins; desf]
   | typ : fence_access_type |- _ => solve [destruct typ; ins; desf]
  end.

Lemma act_ord_loc : loc x = loc y.
Proof. tac. Qed.

Lemma act_ord_thread : thread x = thread y.
Proof. tac. Qed.

Lemma act_ord_na : is_na x -> is_na y.
Proof. tac. Qed.

Lemma act_ord_na_rev : is_na y -> is_na x.
Proof. tac. Qed.

Lemma act_ord_sc : is_sc x -> is_sc y.
Proof. tac. Qed.

Lemma act_ord_rmw : is_rmw x -> is_rmw y.
Proof. tac. Qed.

Lemma act_ord_rmw_rev : is_rmw y -> is_rmw x.
Proof. tac. Qed.

Lemma act_ord_writeLV_rev l v : is_writeLV y l v -> is_writeLV x l v.
Proof. tac. Qed.

Lemma act_ord_readLV_rev l v : is_readLV y l v -> is_readLV x l v.
Proof. tac. Qed.

Lemma act_ord_write : is_write x -> is_write y.
Proof. tac. Qed.

Lemma act_ord_writeL l : is_writeL x l -> is_writeL y l.
Proof. tac. Qed.

Lemma act_ord_writeL_rev l : is_writeL y l -> is_writeL x l.
Proof. tac. Qed.

Lemma act_ord_writeLV l v : is_writeLV x l v -> is_writeLV y l v.
Proof. tac. Qed.

Lemma act_ord_access : is_access x -> is_access y.
Proof. tac. Qed.

Lemma act_ord_readL l : is_readL x l -> is_readL y l.
Proof. tac. Qed.

Lemma act_ord_readLV l v : is_readLV x l v -> is_readLV y l v.
Proof. tac. Qed.

Lemma act_ord_release_write : is_release_write x -> is_release_write y.
Proof. tac. Qed.

Lemma act_ord_release_fence : is_release_fence x -> is_release_fence y.
Proof. tac. Qed.

Lemma act_ord_acquire_read : is_acquire_read x -> is_acquire_read y.
Proof. tac. Qed.

Lemma act_ord_acquire_fence : is_acquire_fence x -> is_acquire_fence y.
Proof. tac. Qed.

End act_ord_lemmas.

Hint Resolve act_ord_na act_ord_na_rev act_ord_sc
  act_ord_rmw act_ord_write act_ord_writeL act_ord_writeLV
  act_ord_access act_ord_readL act_ord_readLV
  act_ord_release_write act_ord_release_fence
  act_ord_acquire_read act_ord_acquire_fence : act_ord_lemmas.

Lemma release_seq_mon :
  forall lab lab' (LO: forall a, act_ord (lab' a) (lab a))
    (sb sb' : relation actid) (SBO: forall a b, sb' a b -> sb a b)
    rf rf' (RFO: forall c d (RF: rf' c = Some d), rf c = Some d)
    mt2 mo a b
    (RS: release_seq mt2 lab' sb' rf' mo a b),
  release_seq mt2 lab sb rf mo a b.
Proof.
  ins.
  eapply release_seq_mon_sb; eauto; clear SBO.
  eapply release_seq_mon_rf; eauto; clear RFO.
  unfold release_seq, release_seq_elem in *; ins.
  destruct (snd mt2); unfold same_thread in *.

  rewrite <- (act_ord_thread _ _ (LO a)), <- (act_ord_thread _ _ (LO b)); unfold NW;
  desf; vauto; right; intuition; eauto using clos_trans_mon with act_ord_lemmas;
    try by exploit RSO; eauto;
    try rewrite <- (act_ord_thread _ _ (LO c));
    intuition eauto using clos_trans_mon with act_ord_lemmas.

  destruct mt2 as [[] ?]; induction RS; ins;
    unfold same_thread in *;
    try rewrite !(fun x => act_ord_thread _ _ (LO x)) in *;
    eauto using release_seq_alt with act_ord_lemmas.
Qed.

Lemma happens_before_mon :
  forall lab lab' (LO: forall a, act_ord (lab' a) (lab a))
    (sb sb' : relation actid) (SBO: forall a b, sb' a b -> sb a b)
    mt2 asw rf mo a b (HB: happens_before mt2 lab' sb' asw rf mo a b),
  happens_before mt2 lab sb asw rf mo a b.
Proof.
  ins; eapply (clos_trans_mon _ HB).
  intuition; right; left; unfold synchronizes_with, NW, diff_thread in *; des;
    try rewrite (act_ord_thread _ _ (LO a0)) in *;
    try rewrite (act_ord_thread _ _ (LO b0)) in *;
    [left|right;left|do 2 right;left|do 3 right]; repeat eexists;
    eauto using clos_trans_mon, release_seq_mon with act_ord_lemmas.
Qed.

Theorem Semiconsistent_mon :
  forall mt (MT: mt <> MTorig) mt2 mtsc (MTSC: mtsc <> MTSCorig) acts lab sb dsb asw rf mo sc
    (CONS: Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
    lab' (LO: forall a, act_ord (lab' a) (lab a))
    (sb' : relation actid) (SBO: forall a b, sb' a b -> sb a b)
    (CSb': ConsistentSB lab' sb') (DSBO: inclusion _ dsb (clos_trans _ sb')),
  exists sc',
    Semiconsistent mt mt2 mtsc acts lab' sb' dsb asw rf mo sc'.
Proof.
  ins; exists (fun a b => sc a b /\ is_sc (lab' a) /\ is_sc (lab' b)).
  unfold Semiconsistent in *; desf; unfold NW; intuition.
  { split; unfold NW; ins; desf; apply FIN; eauto.
    by specialize (LO a); intro X; rewrite X in *; destruct (lab' a); ins; desf. }
  by repeat red; intros; eapply IRR; ins; desf;
     eauto using happens_before_mon.
  red in ACYC; red; desf; unfold rfna in *; try (by exfalso; eauto);
  by repeat red; intros; desf; ins; eapply clos_trans_mon, ACYC in H; ins; desf;
     eauto using happens_before_mon with act_ord_lemmas.
  { red; red in Cdsb; repeat split; ins; desf.
    by apply Cdsb0 in DSB; specialize (LO a); destruct (lab a), (lab' a); ins.
    by apply Cdsb1 in DSB; specialize (LO b); destruct (lab b), (lab' b); ins. }
  { red in Cmo; desf; red; unfold NW; intuition.
      by apply CmoD in MO; desf; eauto using act_ord_writeL_rev.
      by red; ins; eapply CmoF; eauto with act_ord_lemmas. }
  by repeat red; ins; eapply CmoH; eauto using happens_before_mon, act_ord_writeL.
  { red in Csc; desf; red; unfold NW; intuition; red; ins; desf; eauto.
      by eapply CscF in NEQ; desf; eauto using act_ord_sc.
      by split; try done; apply Chbsc; eauto using act_ord_sc, happens_before_mon.
      by split; try done; apply Cmosc; eauto using act_ord_sc, happens_before_mon. }
  { destruct mtsc; ins; try (by exfalso; eauto).
    red; ins; exploit Cscr; eauto using act_ord_sc; ins; desf.
    case_eq (is_sc (lab' a)) as isSCa; [left|right; split; ins].
      unfold sc_restr in *; red in x0; desc; split; repeat split; eauto with act_ord_lemmas.
          by generalize (LO a), x2; clear; destruct (lab' a); ins; destruct (lab a); ins.
        by generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO b)); congruence.
      ins; desf; exploit (x1 c); repeat split; eauto with act_ord_lemmas.
        by generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO c)); congruence.
      by generalize (act_ord_loc _ _ (LO b)), (act_ord_loc _ _ (LO c)); congruence.

      unfold sc_restr in SC0; desf.
      destruct x0 as [A B]; red in A; desc; apply (B x); red; intuition; try rewrite A1;
        eauto with act_ord_lemmas;
        try by generalize (act_ord_loc _ _ (LO b)), (act_ord_loc _ _ (LO x)); congruence.
      by red in Csc; desc; apply CscD in A; desc; eauto using act_ord_sc, happens_before_mon.

    right; split; ins; eauto using act_ord_sc.
    unfold sc_restr in *; desc; eapply (x1 x); repeat split;
      eauto using happens_before_mon with act_ord_lemmas.
    by generalize (act_ord_loc _ _ (LO b)), (act_ord_loc _ _ (LO x)); congruence.
  }
  by red; ins; eauto 10 using happens_before_mon, act_ord_writeLV_rev, act_ord_readLV_rev
          with act_ord_lemmas.
  by red; unfold NW; ins; eapply Crf in RF; desf;
     eauto 10 using happens_before_mon, act_ord_writeLV_rev, act_ord_readLV_rev
              with act_ord_lemmas.
  by red; unfold NW; ins; eapply CrfH in RF; desf;
     eauto 10 using happens_before_mon, act_ord_writeLV_rev, act_ord_readLV_rev
              with act_ord_lemmas.
  by red; ins; eapply Crr; eauto using happens_before_mon;
     generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO b)); congruence.
  by red; ins; eapply Cwr; eauto using happens_before_mon;
     generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO b)); congruence.
  by red; ins; eapply Crw; eauto using happens_before_mon;
     generalize (act_ord_loc _ _ (LO a)), (act_ord_loc _ _ (LO b)); congruence.
  by red; ins; eapply Crmw; eauto using happens_before_mon with act_ord_lemmas.
  by red; ins; eapply Ca; generalize (LO a), (LO b);
     rewrite ALLOCa, ALLOCb; ins; desf; desf.
Qed.

Corollary Consistent_mon :
  forall mt (MT: mt <> MTorig) mt2 mtsc (MTSC: mtsc <> MTSCorig)
         acts lab sb dsb asw rf mo sc
    (CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
    lab' (LO: forall a, act_ord (lab' a) (lab a))
    (sb' : relation actid) (SBO: forall a b, sb' a b -> sb a b)
    (CSb': ConsistentSB lab' sb') (DSBO: inclusion _ dsb (clos_trans _ sb')),
  exists rf' sc',
    Consistent mt mt2 mtsc acts lab' sb' dsb asw rf' mo sc'.
Proof.
  ins; red in CONS; desc.
  edestruct Semiconsistent_mon with (sb' := sb'); eauto.
    by unfold Semiconsistent, NW; intuition eauto.
  eauto using Consistent_restrict_rf.
Qed.