(*********************************************************************) (* Stability in Weak Memory Models *) (* *) (* Jade Alglave INRIA Paris-Rocquencourt, France *) (* University of Oxford, UK *) (* *) (* Copyright 2010 Institut National de Recherche en Informatique et *) (* en Automatique. All rights reserved. This file is distributed *) (* under the terms of the Lesser GNU General Public License. *) (*********************************************************************) Require Import Ensembles. Require Import Bool. Require Import util. Require Import wmm. Require Import basic. Require Import hierarchy. Require Import valid. Require Import covering. Require Import Classical_Prop. Require Import drf. Require Import racy. Import OEEvt. Set Implicit Arguments. Module CritSC (A1 A2: Archi) (dp:Dp). Module Wk := Hierarchy.Weaker A1 A2 dp. Import Wk. Hypothesis wk : weaker. Module VA2 := Valid A2n dp. Import VA2. Import VA2.ScAx. Module Covering := Covering A1 A2n dp. Import Covering. Set Implicit Arguments. Definition rel_inter A (r1 r2 : Rln A) := fun x => fun y => r1 x y /\ r2 x y. Definition cycle_sym A (sigma : Rln A) := forall x y, udr sigma x -> udr sigma y -> sigma x y -> sigma y x. Definition cycle_trans_tot A (sigma : Rln A) := forall x y, udr sigma x -> udr sigma y -> tc (sigma) x y. Definition non_empty A (sigma : Rln A) := (exists x, exists y, sigma x y). Definition cycle A (sigma : Rln A) := cycle_sym sigma /\ cycle_trans_tot sigma /\ non_empty sigma. Ltac destruct_cycle H := destruct H as [Hsym [Htot Hnemp]]. Lemma cycle_implies_nac : forall A (sigma:Rln A), cycle sigma -> ~(acyclic sigma). Proof. unfold acyclic; intros A sigma Hcy Hn. destruct_cycle Hcy. destruct Hnemp as [x [y Hxy]]. unfold cycle_sym in Hsym. assert (udr sigma x) as Hudrx. left; exists y; auto. assert (udr sigma y) as Hudry. right; exists x; auto. generalize (Hsym x y Hudrx Hudry Hxy); intro Hyx. assert (tc (sigma) x x) as Hc. apply trc_ind with y; apply trc_step; auto. generalize (Hn x); intro; contradiction. Qed. Definition conflict E := fun e1 => fun e2 => events E e1 /\ events E e2 /\ loc e1 = loc e2 /\ proc_of e1 <> proc_of e2 /\ (writes E e1 \/ writes E e2). Definition sigma_wf E sigma := rel_incl sigma (tc (rel_union (A2n.ppo E) (rel_inter sigma (conflict E)))). Definition crit_cy E sigma := sigma_wf E sigma /\ ~ acyclic sigma /\ acyclic (rel_union (rel_inter sigma (conflict E)) (rel_union (A1.ppo E) (pio_llh E))) /\ (forall x y, sigma x y -> A2n.ppo E x y -> ~(exists z, (z <> y /\ sigma x z /\ A2n.ppo E x z /\ A2n.ppo E z y)) /\ loc x <> loc y) /\ (forall x y, sigma x y -> conflict E x y -> (((reads E x /\ writes E y) \/ (writes E x /\ reads E y) \/ (writes E x /\ writes E y)) /\ ~(exists z, conflict E z x /\ tc sigma x z /\ tc sigma z y)) \/ (reads E x /\ reads E y /\ exists e, writes E e /\ tc sigma x e /\ tc sigma e y /\ ~(exists z, conflict E z x /\ tc sigma x z /\ tc sigma z y))). Definition mhbd E X := fun x => fun y => (A2nWmm.mhb E X x y) /\ proc_of x <> proc_of y. Ltac destruct_valid H := destruct H as [[Hws_tot Hws_cands] [[Hrf_init [Hrf_cands Hrf_uni]] [Hsp [Hth Hvalid]]]]; unfold write_serialization_well_formed in Hws_tot. Definition sigma_wf_or E X sigma := rel_incl sigma (tc (rel_union (mhbd E X) (A2.ppo E))). Definition crit_cy_or E X sigma := sigma_wf_or E X sigma /\ crit_cy E sigma. Axiom exists_crit_cy_or : forall E X x, tc (A2nWmm.ghb E X) x x -> exists sigma, crit_cy_or E X sigma. Module C <: Compete. Parameter competing : Event_struct -> Execution_witness -> Rln Event. Hypothesis compete_in_events : forall E X x y, well_formed_event_structure E -> rfmaps_well_formed E (events E) (rf X) -> competing E X x y -> events E x /\ events E y. Parameter s : Event_struct -> Execution_witness -> Rln Event. Definition covered E X r := forall e1 e2, (competing E X e1 e2) -> (r E X e1 e2 \/ r E X e2 e1). Definition covering s := forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> covered E X s -> acyclic (A2nWmm.ghb E X). Definition cns E X := fun e1 => fun e2 => competing E X e1 e2 /\ ~ (s E X e1 e2 \/ s E X e2 e1). Hypothesis competing_irr : forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> ~ (exists z, competing E X z z). Hypothesis competing_not_po : forall E X x y, well_formed_event_structure E -> A1Wmm.valid_execution E X -> competing E X x y -> ~ (po_iico E y x). Hypothesis covering_s : covering s. Hypothesis wf : forall E X x y, well_formed_event_structure E -> A1Wmm.valid_execution E X -> competing E X x y -> ~ (s E X x y \/ s E X y x) -> (exists Y, A2nWmm.valid_execution E Y /\ competing E Y x y /\ ~ (s E Y x y \/ s E Y y x)). End C. Module Cm <: Compete. Definition competing E X := fun e1 e2 => C.competing E X e1 e2 /\ (exists sigma, crit_cy E sigma /\ sigma e1 e2). Lemma compete_in_events : forall E X x y, well_formed_event_structure E -> rfmaps_well_formed E (events E) (rf X) -> competing E X x y -> events E x /\ events E y. Proof. intros E X x y Hwf Hrfwf [Hc ?]. apply C.compete_in_events with X; auto. Qed. Definition s E X := fun e1 e2 => C.s E X e1 e2. Definition covered E X r := forall e1 e2, (competing E X e1 e2) -> (r E X e1 e2 \/ r E X e2 e1). Definition covering s := forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> covered E X s -> acyclic (A2nWmm.ghb E X). Definition cns E X := fun e1 => fun e2 => competing E X e1 e2 /\ ~ (s E X e1 e2 \/ s E X e2 e1). Lemma competing_irr : forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> ~ (exists z, competing E X z z). Proof. intros E X Hwf Hv1 [z [Hz ?]]. assert (exists z, C.competing E X z z) as Hc. exists z; auto. apply (C.competing_irr Hwf Hv1 Hc). Qed. Lemma competing_not_po : forall E X x y, well_formed_event_structure E -> A1Wmm.valid_execution E X -> competing E X x y -> ~ (po_iico E y x). Proof. intros E X x y Hwf Hv1 [Hc ?]. apply (C.competing_not_po Hwf Hv1 Hc). Qed. Lemma mhbd_in_conflict : forall E X, well_formed_event_structure E -> write_serialization_well_formed (events E) (ws X) /\ rfmaps_well_formed E (events E) (rf X) -> rel_incl (mhbd E X) (conflict E). Proof. intros E X Hwf Hs x y [? ?]. generalize (A2nBasic.mhb_in_hb E X x y H); intro Hhb. split; [|split; [|split; [|split]]]; auto. change (events E x) with (In _ (events E) x); apply A2nBasic.hb_dom_in_evts with X y; auto. change (events E y) with (In _ (events E) y); apply A2nBasic.hb_ran_in_evts with X x; auto. apply A2nBasic.hb_implies_same_loc with E X; auto. apply A2nBasic.hb_implies_writes with X; auto. Qed. Set Implicit Arguments. Lemma nac_incl : forall A (d s s' : Rln A), rel_incl s' s -> ~ acyclic (rel_union d s') -> ~ acyclic (rel_union d s). Proof. unfold not; unfold acyclic; intros A d s1 s1' Hi Hnac Hc. apply Hnac; intros x Hx. assert (tc (rel_union d s1) x x) as Hin. generalize Hx; apply tc_incl; intros e1 e2 H12. inversion H12; [left | right; apply Hi]; auto. generalize (Hc x); intro; contradiction. Qed. Lemma nac_incl2 : forall A (s s' : Rln A), rel_incl s' s -> ~ acyclic s' -> ~ acyclic s. Proof. unfold not; unfold acyclic; intros A s1 s1' Hi Hnac Hc. apply Hnac; intros x Hx. assert (tc s1 x x) as Hin. generalize Hx; apply tc_incl; intros e1 e2 H12. apply Hi; auto. generalize (Hc x); intro; contradiction. Qed. Lemma not_forall_exists_tc : forall A (s : Rln A), ~(forall x, ~ tc s x x) -> exists x, tc s x x. Proof. intros A s1 Hn. generalize (excluded_middle (exists x, tc s1 x x)); intro Hor; inversion Hor; auto. assert (forall x, ~ tc s1 x x) as Hc. intro x. generalize (excluded_middle (tc s1 x x)); intro Hor2; inversion Hor2; auto. assert (exists x, tc s1 x x) as Hc. exists x; auto. contradiction. contradiction. Qed. Unset Implicit Arguments. Hypothesis covering_s : forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> covered E X s -> acyclic (A2nWmm.ghb E X). Lemma wf : forall E X x y, well_formed_event_structure E -> A1Wmm.valid_execution E X -> competing E X x y -> ~ (s E X x y \/ s E X y x) -> (exists Y, A2nWmm.valid_execution E Y /\ competing E Y x y /\ ~ (s E Y x y \/ s E Y y x)). Proof. intros E X x y Hwf Hv1 [Hc [cy [Hmcy Hcy]]] Hns. unfold s in Hns. generalize (C.wf Hwf Hv1 Hc Hns); intros [Y [Hv2 [HcY HnsY]]]. exists Y; split; [|split]; auto. split; auto. exists cy; split; auto. Qed. Module DrfG := DataRaceFree A1 A2 dp. Module DrfMin (HB : DrfG.HappensBefore). Module Drf := DrfG.Drf0 (HB). Hypothesis s_com : forall E X x y, s E X x y -> ~(hb E X y x). Hypothesis s_po : forall E X, acyclic (rel_union (s E X) (po_iico E)). Lemma tc_mhbd_ppo2_in_s_ppo2 : forall E X x y, well_formed_event_structure E -> A1Wmm.valid_execution E X -> Drf.covered E X s -> tc (rel_union (mhbd E X) (A2.ppo E)) x y -> tc (rel_union (s E X) (A2.ppo E)) x y. Proof. intros E X e1 e2 Hwf Hv1 Hcov; apply tc_incl. intros x y Hxy. assert ( write_serialization_well_formed (events E) (ws X) /\ rfmaps_well_formed E (events E) (rf X)) as Hs. split; split; destruct_valid Hv1; auto. inversion Hxy as [Hc | Hppo2]; [left | right]; auto. assert (Drf.competing E X x y) as Hcomp. destruct Hc as [Hmhbdxy ?]; split; [|split; [|split; [|split]]]; auto. assert (mhbd E X x y) as Hmhbd. split; auto. generalize (mhbd_in_conflict Hwf Hs Hmhbd); intro Hcxy. destruct Hcxy; auto. assert (mhbd E X x y) as Hmhbd. split; auto. generalize (mhbd_in_conflict Hwf Hs Hmhbd); intro Hcxy. destruct Hcxy as [? [? ?]]; auto. assert (mhbd E X x y) as Hmhbd. split; auto. generalize (mhbd_in_conflict Hwf Hs Hmhbd); intro Hcxy. destruct Hcxy as [? [? [? ?]]]; auto. assert (mhbd E X x y) as Hmhbd. split; auto. generalize (mhbd_in_conflict Hwf Hs Hmhbd); intro Hcxy. destruct Hcxy as [? [? [? [? ?]]]]; auto. destruct Hs as [? [? [? ?]]]; auto. generalize (Hcov x y Hcomp); intro Hor; inversion Hor; auto. inversion Hxy as [Hmhbd | Hppo]. destruct Hmhbd as [Hmhbdxy ?]. assert (hb E X x y) as Hhb. apply A2nBasic.mhb_in_hb; auto. generalize (s_com E X y x H3); intro; contradiction. assert (exists x, tc (rel_union (s E X) (po_iico E)) x x) as Hcy. exists x; apply trc_ind with y; apply trc_step; [right | left]; auto. apply A2.ppo_valid; auto. destruct Hcy as [e Hcy]. generalize (s_po E X); intro Hac. generalize (Hac e Hcy); intro Ht; inversion Ht. Qed. Lemma tc_cy_in_tc : forall E X cy, rel_incl cy (tc (rel_union (s E X) (A2.ppo E))) -> rel_incl (tc cy) (tc (rel_union (s E X) (A2.ppo E))). Proof. intros E X cy Hi x y Hxy. induction Hxy. apply Hi; auto. apply trc_ind with z; auto. Qed. Lemma min_covered_implies_no_min_cy : forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> Drf.covered E X s -> ~(exists cy, crit_cy_or E X cy). Proof. intros E X Hwf Hv1 Hc [cy [Hicy [? [Hnac ?]]]]. assert (rel_incl cy (tc (rel_union (s E X) (A2.ppo E)))) as Hi. intros x y Hxy; generalize (Hicy x y Hxy); intro Htc. apply tc_mhbd_ppo2_in_s_ppo2; auto. assert (~(acyclic (rel_union (s E X) (po_iico E)))) as Hco. apply nac_incl2 with (rel_union (s E X) (A2.ppo E)). intros e1 e2 H12; inversion H12; [left | right]; auto. apply A2.ppo_valid; auto. unfold acyclic; intros Hex. generalize (not_forall_exists_tc Hnac); intros [e He]. assert (rel_incl (tc cy) (tc (rel_union (s E X) (A2.ppo E)))) as Hitc. apply tc_cy_in_tc; auto. generalize (Hitc e e He); intro Hxx. generalize (Hex e); intro; contradiction. generalize (s_po E X); intro; contradiction. Qed. Lemma covering_s : forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> Drf.covered E X s -> acyclic (A2nWmm.ghb E X). Proof. intros E X Hwf Hv1 Hc z Hz. generalize (exists_crit_cy_or E X Hz); intros [cy Hcy]. assert (exists cy, crit_cy_or E X cy) as Hex. exists cy; auto. generalize (min_covered_implies_no_min_cy E X Hwf Hv1 Hc); intro Hnex. contradiction. Qed. End DrfMin. Module Racy := Racy A1 A2 dp. Module RacyMin (SN:Racy.SafetyNet). Module R := Racy.Barriers (SN). Definition AC X s := forall (x z y:Event), rf_sub X x z /\ s z y -> s x y. Hypothesis s_ghb : forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> acyclic (rel_union (s E X) (A1bWmm.ghb E X)). Hypothesis s_ppo2 : forall E X, well_formed_event_structure E -> acyclic (rel_union (s E X) (A2n.ppo E)). Hypothesis s_ac : forall E X, AC X (s E X). Lemma tc_cy_in_tc : forall E X cy, rel_incl cy (tc (rel_union (mhbd E X) (A2.ppo E))) -> rel_incl (tc cy) (tc (rel_union (mhbd E X) (A2.ppo E))). Proof. intros E X cy Hi x y Hxy. induction Hxy; auto. apply trc_ind with z; auto. Qed. Lemma tc_mhbd_ppo2_in_mhb_ppo2 : forall E X x y, tc (rel_union (mhbd E X) (A2.ppo E)) x y -> tc (rel_union (A2nBasic.AWmm.mhb E X) (A2n.ppo E)) x y. Proof. intros E X x y Hxy; induction Hxy as [x y Hu |]. apply trc_step; inversion Hu as [Hmhbd | Hppo]; [left | right]; auto. destruct Hmhbd; auto. apply trc_ind with z; auto. Qed. Lemma ppo2_in_ghb1 : forall E X x y, well_formed_event_structure E -> R.covered E X s -> A2n.ppo E x y -> rel_union (A1bWmm.ghb E X) (s E X) x y. Proof. intros E X x y Hwf Hfb Hxy. generalize (excluded_middle (A1b.ppo E x y)); intro Hor. inversion Hor as [Hppo1 | Hnppo1]. left; apply A1bBasic.ppo_in_ghb; auto. assert (ppo_sub E x y) as Hppos. split; auto. assert (R.competing E X x y) as Hc. left; auto. right; generalize (Hfb x y Hc); intro Hors; auto. inversion Hors as [|Hsyx]; auto. assert (tc (rel_union (s E X) (A2n.ppo E)) y y) as Hcy. apply trc_ind with x; apply trc_step; [left | right]; auto. generalize (s_ppo2 E X Hwf); unfold acyclic; intro Hac; generalize (Hac y Hcy); intro Ht; inversion Ht. Qed. Lemma rf_sub_seq_ppo2_in_ab1 : forall E X x z y, well_formed_event_structure E -> R.covered E X s -> rf_sub X x z -> A2n.ppo E z y -> s E X x y. Proof. intros E X x z y Hwf Hfb Hxz Hzy. assert (R.competing E X z y) as Hc. right; split; auto. exists x; auto. generalize (Hfb z y Hc); intro Hor. inversion Hor. assert (rf_sub X x z /\ s E X z y) as Hand. split; auto. apply (s_ac E X x z y Hand). assert (tc (rel_union (s E X) (A2n.ppo E)) y y) as Hcy. apply trc_ind with z; apply trc_step; [left | right]; auto. generalize (s_ppo2 E X Hwf); unfold acyclic; intro Hac; generalize (Hac y Hcy); intro Ht; inversion Ht. Qed. Lemma seq_implies_ghb1_int : forall E X x y, weaker -> well_formed_event_structure E -> R.covered E X s -> tc (rel_seq (rel_union (rel_union (A1bWmm.mhb' E X) (rf_sub X)) (rel_union (rel_seq (ws X) (rf_sub X)) (rel_seq (fr E X) (rf_sub X)))) (tc (A2n.ppo E))) x y -> tc (rel_union (A1bWmm.ghb E X) (s E X)) x y. Proof. intros E X x y Hwk Hwf Hfb Hxy. induction Hxy. destruct H as [z [Hxz Hzy]]. inversion Hxz as [Hu | Hs]. inversion Hu as [Hmhb'1 | Hrf_sub]. apply trc_ind with z. rewrite (ghb1b_eq E X). apply tc_incl with (rel_union (rel_union (ws X) (fr E X)) (rel_union (rel_union (mrf1 X) (A1.ppo E)) (A1b.abc E X))). intros e1 e2 H12; left; auto. apply (mhb'1_eq Hmhb'1). apply tc_incl with (A2n.ppo E); auto. intros e1 e2 H12; apply ppo2_in_ghb1; auto. generalize (tc_dec Hzy); intros [z' [Hzz' Hor]]. inversion Hor as [Htc | Heq]. apply trc_ind with z'. inversion Hu as [Hmhb | Hrfs]. apply trc_ind with z. rewrite (ghb1b_eq E X). apply tc_incl with (rel_union (rel_union (ws X) (fr E X)) (rel_union (rel_union (mrf1 X) (A1.ppo E)) (A1b.abc E X))). intros e1 e2 H12; left; auto. apply (mhb'1_eq Hmhb). apply tc_incl with (A2n.ppo E); auto. intros e1 e2 H12; apply ppo2_in_ghb1; auto. apply trc_step; auto. apply trc_step; right; apply (rf_sub_seq_ppo2_in_ab1 E X x z z' Hwf Hfb Hrf_sub Hzz'). apply tc_incl with (A2n.ppo E); auto. intros e1 e2 H12; apply ppo2_in_ghb1; auto. rewrite <- Heq; apply trc_step; right; apply (rf_sub_seq_ppo2_in_ab1 E X x z z' Hwf Hfb Hrf_sub Hzz'). inversion Hs as [Hsws | Hsfr]. destruct Hsws as [e [Hxe Hez]]. generalize (tc_dec Hzy); intros [z' [Hzz' Hor]]. inversion Hor as [Htc | Heq]. apply trc_ind with z'. apply trc_ind with e; apply trc_step. rewrite (ghb1b_eq E X). left; left; left; auto. right. apply rf_sub_seq_ppo2_in_ab1 with z; auto. apply tc_incl with (A2n.ppo E); auto. intros e1 e2 H12; apply ppo2_in_ghb1; auto. apply trc_ind with e; apply trc_step. rewrite (ghb1b_eq E X). left; left; left; auto. right. apply rf_sub_seq_ppo2_in_ab1 with z; auto. rewrite <- Heq; auto. destruct Hsfr as [e [Hxe Hez]]. generalize (tc_dec Hzy); intros [z' [Hzz' Hor]]. inversion Hor as [Htc | Heq]. apply trc_ind with z'. apply trc_ind with e. apply trc_step. rewrite (ghb1b_eq E X). left; left; right; auto. apply trc_step; right; apply rf_sub_seq_ppo2_in_ab1 with z; auto. apply tc_incl with (A2n.ppo E); auto. intros e1 e2 H12; apply ppo2_in_ghb1; auto. rewrite <- Heq; apply trc_ind with e. apply trc_step. rewrite (ghb1b_eq E X). left; left; right; auto. apply trc_step; right; apply rf_sub_seq_ppo2_in_ab1 with z; auto. apply trc_ind with z; auto. Qed. Lemma seq_implies_ghb1 : forall E X x y, weaker -> well_formed_event_structure E -> R.covered E X s -> tc (rel_seq (maybe (rel_union (rel_union (A1bWmm.mhb' E X) (rf_sub X)) (rel_union (rel_seq (ws X) (rf_sub X)) (rel_seq (fr E X) (rf_sub X))))) (tc (A2n.ppo E))) x y -> tc (rel_union (A1bWmm.ghb E X) (s E X)) x y. Proof. intros E X x y Hwk Hwf Hfb Hxy. induction Hxy. destruct H as [z [Hor Hzy]]. inversion Hor as [Hxz | Heq]. apply seq_implies_ghb1_int; auto. apply trc_step; exists z; auto. subst; generalize Hzy; apply tc_incl. intros e1 e2 H12; apply ppo2_in_ghb1; auto. apply trc_ind with z; auto. Qed. Lemma min_covered_implies_no_min_cy : forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> R.covered E X s -> ~(exists cy, crit_cy_or E X cy). Proof. intros E X Hwf Hv1 Hc [cy [Hicy [? [Hnac ?]]]]. assert ( write_serialization_well_formed (events E) (ws X) /\ rfmaps_well_formed E (events E) (rf X)) as Hs. destruct_valid Hv1; split; split; auto. generalize (not_forall_exists_tc Hnac); intros [x Hx]. generalize (tc_cy_in_tc E X cy Hicy x x Hx); intros Hx'. generalize (tc_mhbd_ppo2_in_mhb_ppo2 E X x x Hx'); intro Htc. change (A2.ppo E) with (A2n.ppo E) in Htc. change (A2nWmm.mhb E X) with (A2nBasic.AWmm.mhb E X) in Htc. assert (exists y, tc (rel_seq (maybe (A2nWmm.mhb' E X)) (tc (A2.ppo E))) y y) as Hcyc. eapply (A2nBasic.mhb_union_ppo_cycle_implies_mhb'_seq_ppo_cycle2 X Hwf Hs Htc); auto; apply Htc. destruct Hcyc as [y Hcyc]. generalize (mhb'_ppo2_is_u_seq wk Hwf Hcyc); intro Hcy'. assert (rfmaps_well_formed E (events E) (rf X)) as Hrfwf. destruct Hs; auto. generalize (seq_implies_ghb1 E X y y wk Hwf Hc Hcy'); rewrite union_triv; intro Hcycle. generalize (s_ghb E X Hwf Hv1 y); intro. contradiction. Qed. Lemma covering_s : forall E X, well_formed_event_structure E -> A1Wmm.valid_execution E X -> R.covered E X s -> acyclic (A2nWmm.ghb E X). Proof. intros E X Hwf Hv1 Hc z Hz. generalize (exists_crit_cy_or E X Hz); intros [cy Hcy]. assert (exists cy, crit_cy_or E X cy) as Hex. exists cy; auto. generalize (min_covered_implies_no_min_cy E X Hwf Hv1 Hc); intro Hnex. contradiction. Qed. End RacyMin. End Cm. End CritSC.