Require Import Peano_dec List Permutation Vbase Relations ExtraRelations.
Require Import extralib actions c11.
Set Implicit Arguments.
Definition restr_rel X (cond: X -> Prop) (rel: relation X) (a b: X) :=
rel a b /\ cond a /\ cond b.
Record opsem :=
{ Tid : nat ;
Res : option nat ;
Acts: list actid ;
Lab : actid -> act ;
Sb : actid -> actid -> Prop ;
Dsb : actid -> actid -> Prop ;
Asw : actid -> actid -> Prop }.
Record witness :=
{ Rf: actid -> option actid ;
Mo: actid -> actid -> Prop ;
Sc: actid -> actid -> Prop }.
Definition pre_execution mt mt2 mtsc o w :=
Semiconsistent mt mt2 mtsc (Acts o) (Lab o) (Sb o) (Dsb o) (Asw o) (Rf w) (Mo w) (Sc w).
Definition defined_pre_exec mt2 o w :=
<< DPE_MS: mem_safe mt2 (Acts o) (Lab o) (Sb o) (Asw o) (Rf w) (Mo w) >> /\
<< DPE_IR: initialized_reads (Acts o) (Lab o) (Rf w) >> /\
<< DPE_RF: race_free mt2 (Lab o) (Sb o) (Asw o) (Rf w) (Mo w) >>.
Definition pre_executable_opsem mt mt2 mtsc o :=
exists w, pre_execution mt mt2 mtsc o w.
Definition Sbw o x y := Sb o x y \/ Asw o x y.
Lemma pre_executable_sb_irrefl:
forall mt mt2 mtsc o,
pre_executable_opsem mt mt2 mtsc o ->
irreflexive (Sb o).
Proof.
unfold pre_executable_opsem, pre_execution, Semiconsistent.
red; ins; desf; eauto with hb.
Qed.
Definition pref_opsem o1 o2 :=
<< Pref_Tid : Tid o1 = Tid o2 >> /\
<< Pref_Res : Res o1 = None \/
Res o1 = Res o2 /\ Acts o2 <> nil /\
forall a (IN : In a (Acts o2)) (EQ: thread (Lab o2 a) = Tid o2), In a (Acts o1) >> /\
<< Pref_Nemp : Acts o1 <> nil >> /\
<< Pref_ND : NoDup (Acts o1) >> /\
<< Pref_Acts : forall a, In a (Acts o1) -> In a (Acts o2) >> /\
<< Pref_LabIn : forall a, In a (Acts o1) -> Lab o1 a = Lab o2 a >> /\
<< Pref_LabOut: forall a, ~ In a (Acts o1) -> Lab o1 a = Askip 0 >> /\
<< Pref_Sb : Sb o1 <--> restr_rel (fun x => In x (Acts o1)) (Sb o2) >> /\
<< Pref_Dsb : Dsb o1 <--> restr_rel (fun x => In x (Acts o1)) (Dsb o2) >> /\
<< Pref_Asw : Asw o1 <--> restr_rel (fun x => In x (Acts o1)) (Asw o2) >> /\
<< Pref_UCSb : upward_closed (Sb o2) (fun x => In x (Acts o1)) >> /\
<< Pref_UCAsw : upward_closed (Asw o2) (fun x => In x (Acts o1)) >>.
Lemma Pref_ExecutionFinite:
forall o1 o2
(PREF: pref_opsem o1 o2)
(EF: ExecutionFinite (Acts o2) (Lab o2) (Sb o2) (Asw o2)),
ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1).
Proof.
unfold pref_opsem, ExecutionFinite; ins; desc; clear Pref_Res; split; red.
ins; destruct (in_dec eq_nat_dec a (Acts o1)); eauto.
by exfalso; eauto.
by ins; desf; [eapply Pref_Sb in H|eapply Pref_Asw in H]; red in H; desf.
Qed.
Definition alt_read (a1 a2: act) :=
(exists tid typ l v1 v2, a1 = Aload tid typ l v1 /\ a2 = Aload tid typ l v2) \/
(exists tid typ l v1 v2 v3, a1 = Aload tid RATrlx l v1 /\ a2 = Armw tid typ l v2 v3).
Definition alt_read_final_one o1 o2 :=
exists a,
<< AFRO_Tid : Tid o1 = Tid o2 >> /\
<< AFRO_Res : Res o1 = if thread (Lab o1 a) == Tid o1 then None else Res o2 >> /\
<< AFRO_ND : NoDup (Acts o1) >> /\
<< AFRO_Acts: forall (a: actid), In a (Acts o1) <-> In a (Acts o2) >> /\
<< AFRO_Max : max_elt (Sbw o1) a >> /\
<< AFRO_Rd : alt_read (Lab o1 a) (Lab o2 a) >> /\
<< AFRO_Lab : forall b, b <> a -> Lab o1 b = Lab o2 b >> /\
<< AFRO_Sb : Sb o1 <--> Sb o2 >> /\
<< AFRO_Dsb : Dsb o1 <--> Dsb o2 >> /\
<< AFRO_Asw : Asw o1 <--> Asw o2 >>.
Lemma alt_read_thread_eq a1 a2 : alt_read a1 a2 -> thread a2 = thread a2.
Proof. unfold alt_read; ins; desf. Qed.
Opsems should be finite.
We require the sb order to be acyclic. This may be enforced by a hypothesis
on the existence of an execution.
Opsemsets are closed by prefix.
Opsemsets are closed by changing the value read by a sb-final read
instruction.
Definition AFR_closed :=
upward_closed alt_read_final_one oss.
Definition oss_defined mt mt2 mtsc :=
forall o (OSS: oss o)
w (PEX: pre_execution mt mt2 mtsc o w),
defined_pre_exec mt2 o w.
Definition DefinedOSS mt mt2 mtsc :=
<< DOSS_ND: forall o (OSS: oss o), NoDup (Acts o) >> /\
<< DOSS_EF: oss_ef >> /\
<< DOSS_ACYC: oss_sbw_acyc >> /\
<< DOSS_Pref: Pref_closed >> /\
<< DOSS_AFR: AFR_closed >> /\
<< DOSS_Def: oss_defined mt mt2 mtsc >>.
upward_closed alt_read_final_one oss.
Definition oss_defined mt mt2 mtsc :=
forall o (OSS: oss o)
w (PEX: pre_execution mt mt2 mtsc o w),
defined_pre_exec mt2 o w.
Definition DefinedOSS mt mt2 mtsc :=
<< DOSS_ND: forall o (OSS: oss o), NoDup (Acts o) >> /\
<< DOSS_EF: oss_ef >> /\
<< DOSS_ACYC: oss_sbw_acyc >> /\
<< DOSS_Pref: Pref_closed >> /\
<< DOSS_AFR: AFR_closed >> /\
<< DOSS_Def: oss_defined mt mt2 mtsc >>.
Receptivity gives an alternative view of the prefix-closed/AFR-closed
condition, by supposing that the program provides a behavior for any
value read by any read instruction. This translates to the existence
of an alternative opsems, which is equal to the original opsem except
for what sb-follows the modified read instruction.
Both notions are equivalent.
Definition is_any_read a tid typ l :=
(exists v, a = Aload tid typ l v) \/
(exists typ' v1 v2, a = Armw tid typ' l v1 v2) /\ typ = RATrlx.
Definition AR_receptivity :=
forall o (OSS: oss o)
a tid typ l (LRead: is_any_read (Lab o a) tid typ l) vor,
exists or,
<< Rec_OSSR: oss or >> /\
<< Rec_Tid : Tid or = Tid o >> /\
<< Pref_Res : (Res or = None /\
exists b, In b (Acts o) /\ clos_refl_trans _ (Sbw o) a b /\
thread (Lab o b) = Tid o) \/
Res or = Res o /\
forall b, In b (Acts or) ->
~ clos_refl_trans _ (Sbw o) a b ->
thread (Lab or b) = Tid o ->
In b (Acts o) >> /\
<< Rec_AR: Lab or a = Aload tid typ l vor >> /\
<< Rec_In: forall b, In b (Acts o) -> ~ clos_trans _ (Sbw o) a b -> In b (Acts or) >> /\
<< Rec_Lab: forall b, In b (Acts o) -> ~ clos_trans _ (Sbw o) a b -> a <> b -> Lab or b = Lab o b >> /\
<< Rec_Sb: (restr_rel (fun x => In x (Acts o) /\ ~ clos_trans _ (Sbw o) a x) (Sb o))
<--> (restr_rel (fun x => ~ clos_trans _ (Sbw o) a x) (Sb or)) >> /\
<< Rec_Dsb: (restr_rel (fun x => In x (Acts o) /\ ~ clos_trans _ (Sbw o) a x) (Dsb o))
<--> (restr_rel (fun x => ~ clos_trans _ (Sbw o) a x) (Dsb or)) >> /\
<< Rec_Asw: (restr_rel (fun x => In x (Acts o) /\ ~ clos_trans _ (Sbw o) a x) (Asw o))
<--> (restr_rel (fun x => ~ clos_trans _ (Sbw o) a x) (Asw or)) >>.
Require Import Classical.
Lemma Receptivity_implies_AFR:
forall (EF: oss_ef) (DSB: oss_dsb) (PREF: Pref_closed) (Recept: AR_receptivity), AFR_closed.
Proof.
unfold Pref_closed, AR_receptivity, AFR_closed; ins; des.
unfold upward_closed; intros x y afr ossy.
unfold alt_read_final_one in *; des.
assert (hmax: max_elt (Sbw y) a).
unfold max_elt in *; ins; eapply AFRO_Max.
by unfold Sbw, same_relation in *; desf; eauto.
unfold alt_read, is_any_read in *; des.
exploit Recept; try eassumption; clear Recept.
by eauto.
ins; desc.
eapply PREF; [|eexact Rec_OSSR].
split; unnw; [congruence|].
split; [|clear AFRO_Res Pref_Res]; repeat (apply conj; ins); desf; eauto.
exfalso; rewrite clos_refl_transE, t_step_rt in *; desf; eauto.
by rewrite AFRO_Rd, AFRO_Rd0 in *; ins; congruence.
right; split; ins; [congruence|].
split; ins; desf.
by intro X; exploit (proj1 (EF _ Rec_OSSR) a); rewrite ?X; ins; congruence.
destruct (eqP a0 a); desf; [
rewrite AFRO_Rd, Rec_AR in *; ins; congruence |].
apply AFRO_Acts, Pref_Res0; eauto; try congruence.
by intro; rewrite clos_refl_transE, t_step_rt in *; desf; eauto.
by intro X; exploit (proj1 (EF _ ossy) a); ins;
rewrite <- ?AFRO_Acts, ?X in *; ins; congruence.
ins; eapply Rec_In.
exploit AFRO_Acts; by intuition.
red; ins; eapply max_elt_clos_trans; eauto.
ins; destruct (eqP a a0); subst.
rewrite Rec_AR; by eauto.
destruct (AFRO_Acts a0). rewrite Rec_Lab; by eauto using max_elt_clos_trans.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
ins; destruct (eqP a a0); subst.
exfalso; eapply H, AFRO_Acts, CLOlab; congruence.
destruct (classic (Lab x a0 = Askip 0)).
by eauto.
by exfalso; eapply H, AFRO_Acts, CLOlab; rewrite <- AFRO_Lab; eauto.
split; try done.
assert (SBY: Sb y x0 y0) by (eapply AFRO_Sb; done).
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply or_introl, CLOsb in SBY; desf.
unfold Sbw in *; destruct AFRO_Sb; eapply Rec_Sb; unfold restr_rel;
by repeat split; eauto using max_elt_clos_trans.
exploit (EF y); unnw; ins; unfold ExecutionFinite in *; desf.
by destruct AFRO_Sb; rewrite !AFRO_Acts; eauto; eapply CLOsb; eauto.
unfold restr_rel, inclusion; ins; desf.
eapply AFRO_Sb. eapply Rec_Sb. unfold restr_rel.
destruct (AFRO_Acts x0); destruct (AFRO_Acts y0).
repeat split; by eauto using max_elt_clos_trans.
split; try done.
assert (SBY: Dsb y x0 y0) by (by eapply AFRO_Dsb).
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
exploit (DSB y); intuition; unfold ConsistentDSB in *; desf.
assert (In x0 (Acts y) /\ In y0 (Acts y)).
eapply x2 in SBY; clear - SBY CLOsb.
induction SBY; desf; eauto.
by desc; destruct AFRO_Dsb; eapply Rec_Dsb; repeat split; eauto using max_elt_clos_trans.
assert (SBY: Dsb y x0 y0) by (by eapply AFRO_Dsb).
exploit (EF y); unnw; ins; unfold ExecutionFinite in *; desf.
exploit (DSB y); ins; unfold ConsistentDSB in *; desf.
destruct AFRO_Sb; rewrite !AFRO_Acts; eapply x2 in SBY; clear - SBY CLOsb H0 H1.
by induction SBY; desf; eauto.
unfold restr_rel, inclusion; ins; desf.
eapply AFRO_Dsb, Rec_Dsb; unfold restr_rel.
destruct (AFRO_Acts x0); destruct (AFRO_Acts y0).
repeat split; by eauto using max_elt_clos_trans.
split; try done.
assert (SBY: Asw y x0 y0).
by eapply AFRO_Asw.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply or_intror, CLOsb in SBY; desf.
destruct AFRO_Asw; eapply Rec_Asw; unfold restr_rel.
by repeat split; eauto using max_elt_clos_trans.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply AFRO_Acts.
destruct AFRO_Asw; exploit (CLOsb x0 y0); by intuition.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply AFRO_Acts.
destruct AFRO_Asw; exploit (CLOsb x0 y0); by intuition.
unfold restr_rel, inclusion; ins; desf.
eapply AFRO_Asw; eapply Rec_Asw; unfold restr_rel.
destruct (AFRO_Acts x0); destruct (AFRO_Acts y0).
repeat split; by eauto using max_elt_clos_trans.
unfold upward_closed; ins.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply AFRO_Acts; exploit (CLOsb x0 y0); intuition.
left; eapply Rec_Sb.
repeat split; by eauto using max_elt_clos_trans.
unfold upward_closed; ins.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply AFRO_Acts; exploit (CLOsb x0 y0); intuition.
right; eapply Rec_Asw.
repeat split; by eauto using max_elt_clos_trans.
exploit Recept; try eassumption; clear Recept.
by right; eauto.
ins; desc.
eapply PREF; [|eexact Rec_OSSR].
split; unnw; [congruence|].
split; [|clear AFRO_Res Pref_Res]; repeat (apply conj; ins); desf; eauto.
exfalso; rewrite clos_refl_transE, t_step_rt in *; desf; eauto.
by rewrite AFRO_Rd, AFRO_Rd0 in *; ins; congruence.
right; split; ins; [congruence|].
split; ins; desf.
by intro X; exploit (proj1 (EF _ Rec_OSSR) a); rewrite ?X; ins; congruence.
destruct (eqP a0 a); desf; [
rewrite AFRO_Rd, Rec_AR in *; ins; congruence |].
apply AFRO_Acts, Pref_Res0; eauto; try congruence.
by intro; rewrite clos_refl_transE, t_step_rt in *; desf; eauto.
by intro X; exploit (proj1 (EF _ ossy) a); ins;
rewrite <- ?AFRO_Acts, ?X in *; ins; congruence.
ins; eapply Rec_In.
exploit AFRO_Acts; by intuition.
red; ins; eapply max_elt_clos_trans; eauto.
ins; destruct (eqP a a0); subst.
rewrite Rec_AR; by eauto.
destruct (AFRO_Acts a0). rewrite Rec_Lab; by eauto using max_elt_clos_trans.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
ins; destruct (eqP a a0); subst.
exfalso; eapply H, AFRO_Acts, CLOlab; congruence.
destruct (classic (Lab x a0 = Askip 0)).
by eauto.
by exfalso; eapply H, AFRO_Acts, CLOlab; rewrite <- AFRO_Lab; eauto.
split; try done.
assert (SBY: Sb y x0 y0) by (eapply AFRO_Sb; done).
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply or_introl, CLOsb in SBY; desf.
unfold Sbw in *; destruct AFRO_Sb; eapply Rec_Sb; unfold restr_rel;
by repeat split; eauto using max_elt_clos_trans.
exploit (EF y); unnw; ins; unfold ExecutionFinite in *; desf.
by destruct AFRO_Sb; rewrite !AFRO_Acts; eauto; eapply CLOsb; eauto.
unfold restr_rel, inclusion; ins; desf.
eapply AFRO_Sb. eapply Rec_Sb. unfold restr_rel.
destruct (AFRO_Acts x0); destruct (AFRO_Acts y0).
repeat split; by eauto using max_elt_clos_trans.
split; try done.
assert (SBY: Dsb y x0 y0) by (by eapply AFRO_Dsb).
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
exploit (DSB y); intuition; unfold ConsistentDSB in *; desf.
assert (In x0 (Acts y) /\ In y0 (Acts y)).
eapply x2 in SBY; clear - SBY CLOsb.
induction SBY; desf; eauto.
by desc; destruct AFRO_Dsb; eapply Rec_Dsb; repeat split; eauto using max_elt_clos_trans.
assert (SBY: Dsb y x0 y0) by (by eapply AFRO_Dsb).
exploit (EF y); unnw; ins; unfold ExecutionFinite in *; desf.
exploit (DSB y); ins; unfold ConsistentDSB in *; desf.
destruct AFRO_Sb; rewrite !AFRO_Acts; eapply x2 in SBY; clear - SBY CLOsb H0 H1.
by induction SBY; desf; eauto.
unfold restr_rel, inclusion; ins; desf.
eapply AFRO_Dsb, Rec_Dsb; unfold restr_rel.
destruct (AFRO_Acts x0); destruct (AFRO_Acts y0).
repeat split; by eauto using max_elt_clos_trans.
split; try done.
assert (SBY: Asw y x0 y0).
by eapply AFRO_Asw.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply or_intror, CLOsb in SBY; desf.
destruct AFRO_Asw; eapply Rec_Asw; unfold restr_rel.
by repeat split; eauto using max_elt_clos_trans.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply AFRO_Acts.
destruct AFRO_Asw; exploit (CLOsb x0 y0); by intuition.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply AFRO_Acts.
destruct AFRO_Asw; exploit (CLOsb x0 y0); by intuition.
unfold restr_rel, inclusion; ins; desf.
eapply AFRO_Asw; eapply Rec_Asw; unfold restr_rel.
destruct (AFRO_Acts x0); destruct (AFRO_Acts y0).
repeat split; by eauto using max_elt_clos_trans.
unfold upward_closed; ins.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply AFRO_Acts; exploit (CLOsb x0 y0); intuition.
left; eapply Rec_Sb.
repeat split; by eauto using max_elt_clos_trans.
unfold upward_closed; ins.
exploit (EF y); intuition; unfold ExecutionFinite in *; desf.
eapply AFRO_Acts; exploit (CLOsb x0 y0); intuition.
right; eapply Rec_Asw.
repeat split; by eauto using max_elt_clos_trans.
Qed.
Lemma filter_Prop:
forall X (eq_X_dec: forall (x y: X), {x=y}+{x<>y}) (l: list X) (ND: NoDup l) (P: X -> Prop),
exists l', NoDup l' /\ forall x, In x l' <-> In x l /\ P x.
Proof.
ins; induction l.
by exists nil,; ins; intuition.
inv ND; intuition; desf; destruct (classic (P a)).
by exists (a :: l'),; [constructor|]; ins; rewrite H0; intuition; desf.
by exists l',; ins; rewrite H0; intuition; desf.
Qed.
Require Import ClassicalDescription.
Lemma AFR_implies_Receptivity:
forall (ND: forall o (OSS: oss o), NoDup (Acts o))
(EF: oss_ef) (ACYC: oss_sbw_acyc)
(PREF: Pref_closed) (AFR: AFR_closed), AR_receptivity.
Proof.
unfold Pref_closed, AR_receptivity, AFR_closed; ins; des.
destruct (filter_Prop eq_nat_dec (ND _ OSS) (fun x => ~ clos_trans _ (Sbw o) a x))
as (acts_pref & acts_pref_ND & acts_pref_In).
set (lab_pref := fun x => if in_dec eq_nat_dec x acts_pref
then Lab o x
else Askip 0).
set (sb_pref := restr_rel (fun x => In x acts_pref) (Sb o)).
set (dsb_pref := restr_rel (fun x => In x acts_pref) (Dsb o)).
set (asw_pref := restr_rel (fun x => In x acts_pref) (Asw o)).
set (op_pref := {| Tid := Tid o ;
Res := if
excluded_middle_informative (
exists a', In a' (Acts o) /\ thread (Lab o a') = Tid o /\ clos_trans actid (Sbw o) a a') then None else Res o ;
Acts := acts_pref;
Lab := lab_pref ;
Sb := sb_pref ;
Dsb := dsb_pref ;
Asw := asw_pref |}).
exists {| Tid := Tid o ; Res := if Tid o == tid then None else Res op_pref ;
Acts := acts_pref;
Lab := fun x => if x == a
then Aload tid typ l vor
else lab_pref x;
Sb := sb_pref;
Dsb := dsb_pref ;
Asw := asw_pref |}; ins.
repeat (split; rewrite ?eqxx; ins); unnw;
try (by ins; unfold dsb_pref, asw_pref, sb_pref, restr_rel in *; desf;
eapply acts_pref_In; eauto).
eapply AFR with op_pref.
exists a; unnw; repeat (split; ins); rewrite ?eqxx; ins;
try (by unfold sb_pref, dsb_pref, asw_pref, restr_rel in *; intuition).
by desf; desf; ins; congruence.
unfold max_elt, sb_pref, asw_pref, restr_rel; ins; des.
by unfold Sbw in *; ins; des;
eapply acts_pref_In in REL1; desf; eauto using t_step.
unfold lab_pref; desf; desf.
by unfold is_any_read, alt_read in *; desf; eauto 8; rewrite LRead; eauto 10.
destruct n. eapply acts_pref_In. split.
exploit EF; eauto.
by unfold ExecutionFinite; ins; desf; eapply CLOlab;
unfold is_any_read in *; desf; rewrite LRead.
intro; eapply ACYC; by eauto.
by desf; desf.
eapply PREF; eauto.
unfold pref_opsem; repeat split; unnw; ins;
try (by unfold sb_pref, dsb_pref, asw_pref, restr_rel in *; intuition).
desf; vauto; right; split; [|split]; ins; rewrite ?acts_pref_In; try split; ins.
by red in LRead; desf; intro X; exploit (proj1 (EF _ OSS) a); rewrite ?X; ins; congruence.
by intro; destruct n; eauto.
by red in LRead; desf; intro X; exploit (proj1 (EF _ OSS) a);
rewrite <- ?AFRO_Acts, ?X in *; ins; try congruence;
eapply acts_pref_In; split; eauto; red; eapply ACYC; eauto.
ins; by eapply acts_pref_In.
unfold lab_pref; ins; by desf.
ins; unfold lab_pref; by desf.
unfold upward_closed.
ins.
eapply acts_pref_In in POST. desf.
eapply acts_pref_In. split.
exploit EF; eauto.
unfold ExecutionFinite; ins; desf.
eapply (CLOsb x y); by eauto.
by unfold Sbw in *; eauto 6 using clos_trans.
unfold upward_closed.
ins.
eapply acts_pref_In in POST. desf.
eapply acts_pref_In. split.
exploit EF; eauto.
unfold ExecutionFinite; ins; desf.
eapply (CLOsb x y); by eauto.
by unfold Sbw in *; eauto 6 using clos_trans.
desf; desf.
by left; split; [|exists a]; ins; unfold is_any_read in *; desf; rewrite LRead;
ins; repeat split; eauto using rt_refl;
apply EF; eauto; congruence.
by left; split; [|exists a']; ins; rewrite clos_refl_transE; repeat split; eauto.
by subst lab_pref; right; split; ins; desf; ins; desf;
rewrite acts_pref_In in *; desf.
ins; unfold lab_pref; desf.
exploit EF; eauto.
unfold ExecutionFinite; ins; desf.
apply NNPP; intro.
by destruct n; eapply acts_pref_In; desf.
Qed.
End OpsemSets.
This page has been generated by coqdoc