diff --git a/theories/common/ident.v b/theories/common/ident.v
index f290cb7b..7e0ab05c 100644
--- a/theories/common/ident.v
+++ b/theories/common/ident.v
@@ -177,6 +177,19 @@ Proof. by rewrite nfreshE size_rev size_traject. Qed.
 Lemma nfresh_last n : last \i0 (nfresh n) = \i0.
 Proof. by rewrite nfreshE trajectS rev_cons -cats1 last_cat. Qed.
 
+Lemma behead_nfresh n :
+  n != 0 ->
+  behead (nfresh n) = nfresh n.-1.
+Proof. by case: n. Qed.
+
+Lemma nfresh2 n e1 e2 s : 
+  [:: e1, e2 & s] = nfresh n -> e1 = fresh e2.
+Proof. by case: n=> //= [[/= |/= ?]][->->].  Qed.
+
+Lemma nfresh1 n e1 : 
+  [:: e1] = nfresh n -> nfresh n = [:: \i0].
+Proof. by case: n=> //= [[]]. Qed.
+
 End NfreshSpec.
 
 Lemma nfresh_le x n : x \in nfresh n.+1 -> x <= fresh_seq (nfresh n).
diff --git a/theories/concur/porf_eventstruct.v b/theories/concur/porf_eventstruct.v
index 6ccedbee..a41284a4 100644
--- a/theories/concur/porf_eventstruct.v
+++ b/theories/concur/porf_eventstruct.v
@@ -301,6 +301,11 @@ Definition edescr_map {E1 E2 : Type} : (E1 -> E2) -> edescr E1 -> edescr E2 :=
     let: mk_edescr l e_po e_rf := ed in
     mk_edescr l (f e_po) (f e_rf).
 
+Lemma edescr_mapE {E1 E2} (f : E1 -> E2) ed : 
+  edescr_map f ed = mk_edescr (lab_prj ed) (f (fpo_prj ed)) (f (frf_prj ed)).
+Proof. by case: ed. Qed.
+
+
 (* TODO: prove functor and monad laws? *)
 
 Lemma edescr_map_id {E : Type} : 
@@ -366,7 +371,6 @@ Context {disp : unit} (E : identType disp) (L : labType).
 Local Notation edescr := (edescr E L).
 
 Structure porf_eventstruct := Pack {
-  dom    : seq E;
   fed    : { fsfun for fun e =>
                {| lab_prj := \eps;
                   fpo_prj := e;
@@ -374,6 +378,7 @@ Structure porf_eventstruct := Pack {
                |} : edescr
            };
 
+  dom    := nfresh (#|` finsupp fed|.-1);
   lab e  := lab_prj (fed e);
   fpo e  := fpo_prj (fed e);
   frf e  := frf_prj (fed e);
@@ -413,20 +418,17 @@ Section PORFEventStructEq.
 Context {disp} {E : identType disp} {L : labType}.
 
 Definition eq_es (es es' : porf_eventstruct E L) : bool :=
-  [&& dom es == dom es' & fed es == fed es'].
+  fed es == fed es'.
 
 Lemma eqesP : Equality.axiom eq_es.
 Proof.
   move=> x y; apply: (iffP idP)=> [|->]; last by rewrite /eq_es ?eq_refl.
-  case: x=> dom1 fed1 lab1 fpo1 frf1 df1 ds1 di1. 
-  rewrite {}/lab1 {}/fpo1 {}/frf1=> li1 pc1 f1 g1 rc1 rc1' rc1''.
-  case: y=> dom2 fed2 lab2 fpo2 frf2 df2 ds2 di2.
-  rewrite {}/lab2 {}/fpo2 {}/frf2=> li2 pc2 f2 g2 rc2 rc2' rc2''.
-  case/andP=> /= /eqP E1 /eqP E2. 
+  case: x=> /= fed1 df1 ds1 di1 li1 pc1 f1 g1 rc1 rc1' rc1''.
+  case: y=> /= fed2 df2 ds2 di2 li2 pc2 f2 g2 rc2 rc2' rc2''.
+  move=> /eqP /= E1. 
   move: df1 ds1 di1 li1 pc1 f1 g1 rc1 rc1' rc1''. 
   move: df2 ds2 di2 li2 pc2 f2 g2 rc2 rc2' rc2''. 
-  move: E1 E2; do 2 (case: _ /). 
-  move=> *; congr Pack; exact/eq_irrelevance.
+  case: _ / E1; move=> *; congr Pack; exact/eq_irrelevance.
 Qed.
 
 End PORFEventStructEq. 
@@ -443,18 +445,17 @@ Local Notation edescr := (edescr E L).
 
 Lemma inh_exec_eventstructure : porf_eventstruct E L.
 Proof.
-  pose dom0 := ([:: \i0] : seq E).
-  pose fed0 := [fsfun [fsfun] with ident0 |-> mk_edescr \init \i0 \i0] :
+  pose fed0 := [fsfun [fsfun] with \i0 |-> mk_edescr \init \i0 \i0] :
     {fsfun for fun e => mk_edescr \eps e e : edescr}.
-  have S: finsupp fed0 =i [:: \i0] => [?|].
+  have S: finsupp fed0 = [fset \i0].
   - rewrite /fed0 finsupp_with /= /eq_op /= /eq_op /= /eq_op /=.
-    by rewrite (negbTE init_eps) finsupp0 ?inE orbF.
+    by rewrite (negbTE init_eps) /= finsupp0 fsetU0.
   have F: fed0 \i0 = mk_edescr \init \i0 \i0 by rewrite ?fsfun_with.
   have [: a1 a2 a3 a4 a5 a6 a7 a8 a9 a10] @evstr : 
-  porf_eventstruct E L := Pack dom0 fed0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10;
-  rewrite /dom0 ?inE ?eq_refl //.
-  - by apply/eqP/fsetP=> ?; rewrite S seq_fsetE.
-  all: apply/forallP=> [[/= x]]; rewrite S ?inE=> /eqP-> /[! F]/= //.
+  porf_eventstruct E L := Pack fed0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10.
+  - by apply/eqP/fsetP=> ?; rewrite ?inE seq_fsetE S cardfs1 /= ?inE.
+  all: rewrite ?S ?cardfs1 /nfresh /= /fresh_seq /= ?inE ?eq_refl //.
+  all: apply/forallP=> [[/= x]]; rewrite ?inE=> /eqP-> /[! F]/= //.
   all: by rewrite ?eq_refl ?synch.
 Defined.
 
@@ -611,7 +612,8 @@ Lemma fpo_dom e :
   e \in dom -> fpo e \in dom.
 Proof.
   rewrite -fed_supp_mem.
-  case: es=> /=; rewrite /porf_eventstruct.fpo /==>> ???? /forallP H ????? L'.
+  case: es=> /=; 
+  rewrite /porf_eventstruct.fpo /porf_eventstruct.dom /==>> ???? /forallP H ????? L'.
   exact/(H [` L']).
 Qed.
 
@@ -665,7 +667,8 @@ Lemma frf_dom e :
   e \in dom -> frf e \in dom.
 Proof.
   rewrite -fed_supp_mem.
-  case: es=> /=; rewrite /porf_eventstruct.frf /==>> ????? /forallP H ???? L'.
+  case: es=> /=; 
+  rewrite /porf_eventstruct.frf /porf_eventstruct.dom /==>> ????? /forallP H ???? L'.
   exact/(H [` L']).
 Qed.
 
@@ -1070,6 +1073,17 @@ Implicit Type es : (@porf_eventstruct disp E L).
 Inductive prime_porf_eventstruct := 
   PrimeES es of (rf_ncf_dom es && dup_free es).
 
+Lemma prime_inh : 
+  rf_ncf_dom (inh : (@porf_eventstruct disp E L)) && 
+  dup_free (inh : (@porf_eventstruct disp E L)).
+Proof.
+  have I : forall (x : E), x \in dom inh -> x = \i0=> [>|].
+  - rewrite -fed_supp_mem /= finsupp_with /= {1}/eq_op /= {1}/eq_op /=.
+    by rewrite {1}/eq_op /= (negbTE init_eps) /= finsupp0 ?inE orbF =>/eqP->.
+  apply/andP; split; last by apply/dup_freeP=> ?? /I->/I->.
+  - apply/allP=> /= x ?; by rewrite ?inE /frf (I L x) // ?fsfun_with /= eqxx.
+Qed.
+
 Arguments PrimeES {_}.
 
 Coercion porf_eventstruct_of (pes : prime_porf_eventstruct) :=
@@ -1080,6 +1094,15 @@ Canonical prime_subType := [subType for porf_eventstruct_of].
 Lemma prime_inj : injective (porf_eventstruct_of).
 Proof. exact: val_inj. Qed.
 
+Definition prime_eqMixin := Eval hnf in [eqMixin of prime_porf_eventstruct by <:].
+Canonical prime_eqType := Eval hnf in EqType prime_porf_eventstruct prime_eqMixin.
+
 End PrimePORFEventStruct.
 
-Notation "e '|-' a # b" := (cf e a b) (at level 10).
\ No newline at end of file
+Notation "e '|-' a # b" := (cf e a b) (at level 10).
+
+Canonical pes_inhMixin {disp E V} := 
+  @Inhabitant.Mixin (@prime_porf_eventstruct disp E V) _ 
+    (PrimeES _ (prime_inh E V)).
+Canonical pes_inhType {disp E V} := 
+  Eval hnf in Inhabitant (@prime_porf_eventstruct disp E V) pes_inhMixin.
\ No newline at end of file
diff --git a/theories/concur/transitionsystem.v b/theories/concur/transitionsystem.v
index 918ee8b6..f5714225 100644
--- a/theories/concur/transitionsystem.v
+++ b/theories/concur/transitionsystem.v
@@ -2,7 +2,7 @@ From RelationAlgebra Require Import lattice monoid rel kat_tac kleene.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice seq path.
 From mathcomp Require Import order finmap fintype ssrnat finfun.
 From eventstruct Require Import utils porf_eventstruct ident.
-From eventstruct Require Import rewriting_system inhtype.
+From eventstruct Require Import rewriting_system inhtype ssrnatlia.
 
 (******************************************************************************)
 (* Here we want to make function that by event and event structure creates a  *)
@@ -110,9 +110,6 @@ Proof. by move/add_po_in_dom/(fresh_seq_lt (dom_sorted _)): al. Qed.
 Lemma rf_fresh_id : write < fresh_id.
 Proof. by move/add_rf_in_dom/(fresh_seq_lt (dom_sorted _)): al. Qed.
 
-Definition contain := 
-  has (fun e => (flab e == lb) && (ffrf e == write) && (ffpo e == pred)) dom.
-
 Definition add_fed :=
   [ fsfun ffed with fresh_id |->
                     {| lab_prj := lb; fpo_prj := pred; frf_prj := write |} ].
@@ -139,31 +136,42 @@ Lemma add_frfE e :
   add_frf e = if e == fresh_id then write else frf es e.
 Proof. by rewrite /add_frf /add_fed /= fsfun_withE; case: ifP. Qed.
 
-Fact add_fed_finsupp : finsupp add_fed == (seq_fset tt (fresh_id :: dom)).
+Lemma add_fed_supp : finsupp add_fed = (seq_fset tt (fresh_id :: dom)).
 Proof.
-  apply/fset_eqP=> x; rewrite ?inE seq_fsetE finsupp_with.
+  apply/fsetP=> x; rewrite ?inE seq_fsetE finsupp_with.
   case: ifP; rewrite ?inE fed_supp //.
   move: po_fresh_id=> /[swap]/eqP[?->]; by rewrite ltxx.
 Qed.
 
+Lemma dom_nfresh : fresh_id :: dom = (nfresh #|` finsupp add_fed|.-1).
+Proof.
+  rewrite /dom add_fed_supp size_seq_fset undup_id /dom -nfreshS.
+  - by rewrite nfresh_size.
+  exact/(sorted_uniq (rev_trans (lt_trans)) ltxx (nfresh_sorted _)).
+Qed.
+
+
+Fact add_fed_finsupp : finsupp add_fed == seq_fset tt (nfresh #|` finsupp add_fed|.-1).
+Proof. by rewrite {1}add_fed_supp dom_nfresh. Qed.
+
 Lemma add_fed0 : 
   add_fed ident0 = {| lab_prj := \init; fpo_prj := ident0; frf_prj := ident0 |}.
 Proof. rewrite add_fedE lt_eqF=> //; [ exact/fed0| exact/i0_fresh_seq ]. Qed.
 
 Fact add_fpo_dom :
-  [forall e : finsupp add_fed, add_fpo (val e) \in fresh_id :: dom].
+  [forall e : finsupp add_fed, add_fpo (val e) \in (nfresh #|` finsupp add_fed|.-1)].
 Proof.
   apply/forallP=> [[/= x]].
-  rewrite (eqP add_fed_finsupp) ?inE seq_fsetE ?inE /add_fpo fsfun_withE.
+  rewrite -dom_nfresh add_fed_supp ?inE seq_fsetE ?inE /add_fpo fsfun_withE.
   case: (x =P fresh_id) => /=; first by rewrite (add_po_in_dom al).
   by move=> ? /fpo_dom->.
 Qed.
 
 Fact add_frf_dom :
-  [forall e : finsupp add_fed, add_frf (val e) \in fresh_id :: dom].
+  [forall e : finsupp add_fed, add_frf (val e) \in  (nfresh #|` finsupp add_fed|.-1)].
 Proof.
   apply/forallP=> [[/= x]].
-  rewrite (eqP add_fed_finsupp) ?inE seq_fsetE ?inE /add_frf fsfun_withE.
+  rewrite -dom_nfresh add_fed_supp ?inE seq_fsetE ?inE /add_frf fsfun_withE.
   case: (x =P fresh_id)=> /=; first by rewrite (add_rf_in_dom al).
   by move=> ? /frf_dom->.
 Qed.
@@ -172,7 +180,7 @@ Fact add_fpo_le :
   [forall e : finsupp add_fed, (val e != \i0) ==> (add_fpo (val e) < val e)].
 Proof.
   apply/forallP=> [[/=]] e. 
-  rewrite (eqP add_fed_finsupp) ?inE seq_fsetE ?inE.
+  rewrite add_fed_supp ?inE seq_fsetE ?inE.
   rewrite add_fpoE; case: ifP=> /= [/eqP-> _|?].
   - by rewrite po_fresh_id implybT.
   by move/fpo_n0/implyP. 
@@ -182,7 +190,7 @@ Fact add_frf_le :
   [forall e : finsupp add_fed, (val e != \i0) ==> (add_frf (val e) < val e)].
 Proof.
   apply/forallP=> [[/=]] e. 
-  rewrite (eqP add_fed_finsupp) ?inE seq_fsetE ?inE.
+  rewrite add_fed_supp ?inE seq_fsetE ?inE.
   rewrite add_frfE; case: ifP=> /= [/eqP-> _|?].
   - by rewrite rf_fresh_id implybT.
   by move/frf_n0/implyP. 
@@ -194,7 +202,7 @@ Fact add_frf_sync :
   [forall e : finsupp add_fed, add_lab (add_frf (val e)) (rf)>> add_lab (val e)].
 Proof.
   apply/forallP=> [[/=]] e. 
-  rewrite (eqP add_fed_finsupp) ?inE seq_fsetE ?inE.
+  rewrite add_fed_supp ?inE seq_fsetE ?inE.
   rewrite !add_labE !add_frfE.
   case: (e =P fresh_id)=> /= [|? /frf_dom /(fresh_seq_lt dom_sorted)/lt_eqF->].
   - by rewrite (lt_eqF rf_fresh_id) (add_rf_consist al).
@@ -205,7 +213,7 @@ Fact add_fpo_sync :
   [forall e : finsupp add_fed, add_lab (add_fpo (val e)) (po)>> add_lab (val e)].
 Proof.
   apply/forallP=> [[/=]] e. 
-  rewrite (eqP add_fed_finsupp) ?inE seq_fsetE ?inE.
+  rewrite add_fed_supp ?inE seq_fsetE ?inE.
   rewrite !add_labE !add_fpoE.
   case: (e =P fresh_id)=> /= [|? /fpo_dom /(fresh_seq_lt dom_sorted)/lt_eqF->].
   - by rewrite (lt_eqF po_fresh_id) (add_po_consist al).
@@ -213,15 +221,18 @@ Proof.
 Qed.
 
 Lemma nfresh_dom0 : 
-  \i0 \in fresh_id :: dom.
-Proof. by rewrite ?inE dom0. Qed.
+  (\i0 : E) \in nfresh #|` finsupp add_fed|.-1.
+Proof. 
+  rewrite add_fed_supp size_seq_fset undup_id /dom -nfreshS.
+  - by rewrite /dom /= nfresh_size nfreshE mem_rev /= ?inE eqxx.
+  exact/(sorted_uniq (rev_trans (lt_trans)) ltxx (nfresh_sorted _)).
+Qed.
 
 Definition add_event :=
   @Pack _ _ _
-        (fresh_id :: dom)
         add_fed
         add_fed_finsupp
-        (path_fresh_seq dom_sorted)
+        (nfresh_sorted _)
         nfresh_dom0
         add_fed0
         add_fpo_dom
@@ -231,8 +242,6 @@ Definition add_event :=
         add_fpo_sync
         add_frf_sync.
 
-Definition add_new_event := if contain then es else add_event.
-
 Hypothesis rf_ncf_dom_  : rf_ncf_dom es.
 (* Hypothesis rf_ncf_fresh : ~~ (cf add_event fresh_id write). *)
 
@@ -240,6 +249,11 @@ Import Relation_Operators.
 
 (* TODO: remove duplicate lemmas `add_fedE`, `add_labE`, etc *)
 
+Lemma dom_add_event : 
+  porf_eventstruct.dom add_event = fresh_id :: dom.
+Proof. by rewrite {1}/porf_eventstruct.dom -dom_nfresh. Qed.
+
+
 Lemma fed_add_eventE e :
   fed add_event e = if e == fresh_id then mk_edescr lb pred write else fed es e.
 Proof. exact: add_fedE. Qed.
@@ -308,14 +322,14 @@ Lemma rf_ncf_add_event :
 Proof.
   split=> [?|].
   - rewrite /rf_ncf_dom; apply /allP=> e1.
-    rewrite /frf /= fsfun_withE ?inE.
+    rewrite /frf /= dom_add_event fsfun_withE ?inE.
     case: ifP=> /= [/eqP-> _|/negbT N /(allP rf_ncf_dom_)] //; first exact/implyP.
     rewrite -cf_add_eventE //.
     apply/negP=> /eqP Ef.
     have /ica_fresh /eqP /(negP N) //: ica es fresh_id e1.
     by rewrite icaE /= ?inE -Ef eq_refl.
   case: (boolP (write == fresh_id))=> [/eqP<- /cf_irrelf/(_ write)->|?] //.
-  move/allP/(_ fresh_id)=> /=; rewrite frf_add_eventE inE eq_refl /=.
+  move/allP/(_ fresh_id)=> /=; rewrite dom_add_event frf_add_eventE inE eq_refl /=.
   move/(_ erefl)/implyP; exact.
 Qed.
 
@@ -372,9 +386,10 @@ Notation prime_porf_eventstruct := (@prime_porf_eventstruct disp E Lab).
 
 Notation label := Lab.
 
-Implicit Types (x : Loc) (es : porf_eventstruct).
+Implicit Types (x : Loc) (es : porf_eventstruct) (pes : prime_porf_eventstruct).
 
-Definition tr es1 es2 := exists al, es2 = @add_event disp _ Lab es1 al.
+Definition tr : hrel _ _ :=
+  fun es1 es2 => exists al, es2 = @add_event disp _ Lab es1 al.
 
 Notation "es1 '~>' es2" := (tr es1 es2) (at level 0).
 
@@ -535,7 +550,7 @@ End Equivalence.
 
 Notation "e1 ~~ e2" := (eqv e1 e2) (at level 20).
 
-Notation fresh_id1  es := (fresh_seq (dom es)).
+Notation fresh_id1 es := (fresh_seq (dom es)).
 Notation fresh_id2 es := (fresh_seq (fresh_seq (dom es) :: dom es)).
 
 Lemma is_iso_swap es1 es2 f e1 e2 :
@@ -567,9 +582,13 @@ Qed.
 Arguments Add {_ _ _ _} _ _ _.
 Arguments dom_sorted {_ _ _ _}.
 
+Lemma exlab_tr : tr ≡ exlab ltr.
+Proof. by move=> ??; split=> [[l ->]|[?[l ->]]]; do ? exists l. Qed.
+
 Lemma comm_eqv_tr :
-  diamond_commute eqv tr.
+  diamond_commute eqv (exlab ltr).
 Proof.
+  rewrite -exlab_tr.
   move=> es es3 ? /[swap][][[al ap aw apd awd apc awc]]->.
   case=> f /[dup][[_ [g? c]]] I.
   have NI: g (fresh_id1 es3) \notin dom es.
@@ -607,9 +626,10 @@ Lemma add_add (es : porf_eventstruct)
 Proof.
   case: al2=> l p w ap aw ??.
   have [:a1 a2 a3 a4] @al : add_label (add_event al1) := 
-    Add l p w a1 a2 a3 a4; try by rewrite ?inE (ap, aw) orbT.
+    Add l p w a1 a2 a3 a4; try by rewrite dom_add_event ?inE (ap, aw) orbT.
     - by rewrite /= lab_add_eventE (lt_eqF (fresh_seq_lt dom_sorted ap)).
-    - by rewrite /= lab_add_eventE (lt_eqF (fresh_seq_lt dom_sorted aw)).  by exists al; rewrite ?(swap_dom (lexx _)).
+    - by rewrite /= lab_add_eventE (lt_eqF (fresh_seq_lt dom_sorted aw)). 
+    by exists al; rewrite ?(swap_dom (lexx _)).
 Qed.
 
 Lemma swap_add es 
@@ -627,9 +647,9 @@ Proof.
   move=> x /=; rewrite /comp !fed_add_eventE /=.
   have: fresh_id1 es <> fresh_id2 es by move/(@fresh_iter _ _ 1 2).
   move/eqP/negbTE=>F; case: (x =P fresh_id1 es)=> [->|/eqP/[dup] ? /negbTE N1].
-  - rewrite swap1 eq_refl F /= !swap_dom //.
-  rewrite ?inv_eq ?swap1 ?swap2 ?N1; try exact/swap_inv.
-  case: ifP=> //=; first by rewrite !swap_dom=> //.
+  - rewrite ?dom_add_event swap1 eq_refl F /= !swap_dom //.
+  rewrite ?dom_add_event ?inv_eq ?swap1 ?swap2 ?N1; try exact/swap_inv.
+  case: ifP=> //=; first by rewrite !swap_dom=> //=.
   move/negbT=> ?; rewrite -swap_not_eq //.
   case: (boolP (x \in dom es))=> [|I]. 
   - case L: (fed _ x)=> [l p r] I /=; apply/congr2; rewrite swap_dom //.
@@ -639,19 +659,16 @@ Proof.
 Qed.
 
 Lemma comm_ltr l1 l2 :
-  eqv_diamond_commute (ltr l1) (ltr l2) eqv.
+  eqv_rdiamond_commute (ltr l1) (ltr l2) eqv.
 Proof.
   move=> es ?? [al1 -> /[swap][[al2->]]].
   case: (add_add al1 al2)=> al3 /[dup]? <-->.
   case: (add_add al2 al1)=> al4 /[dup]? <-->.
   exists (add_event al3), (add_event al4).
-  split; [by exists al3| by exists al4|].
+  split; [by right; exists al3| by right; exists al4|].
   exists (swap id (fresh_id1 es) (fresh_id2 es)); exact/swap_add.
 Qed.
 
-Lemma exlab_tr : tr ≡ exlab ltr.
-Proof. by move=> ??; split=> [[l ->]|[?[l ->]]]; do ? exists l. Qed.
-
 Arguments isoE {_ _ _ _ _}.
 
 Lemma dom_consist_eqv es1 es2 :
@@ -683,15 +700,15 @@ Proof.
   have W : f w1 = w1 by rewrite /f (swap_dom aw1).
   have [: a1 a2 a3 a4] @al3 : add_label (add_event al2) 
     := Add la1 (f p1) (f w1) a1 a2 a3 a4=> /=.
-  1,2: rewrite ?inE (P, W) (ap1, aw1); lattice.
+  1,2: rewrite ?dom_add_event ?inE (P, W) (ap1, aw1); lattice.
   - by rewrite P lab_add_eventE (lt_eqF (po_fresh_id al1)).
   - by rewrite W lab_add_eventE (lt_eqF (rf_fresh_id al1)).
   have E1: al1 = al3 :> edescr _ _ by rewrite /= W P.
   have E2: al2 = al2' :> edescr _ _ by [].
-  rewrite (isoE (swap_add E1 E2)) swap2 (swap_dom aw) //.
-  rewrite -cf_add_eventE; first exact/rf_ncf_add_event.
+  rewrite ?dom_add_event (isoE (swap_add E1 E2)) swap2 (swap_dom aw) //.
+  rewrite -cf_add_eventE ?dom_add_event; first exact/rf_ncf_add_event.
   - by apply/eqP=> /(@fresh_iter _ _ 1 2).
-  by rewrite (lt_eqF (rf_fresh_id al2')).
+  by move: (lt_eqF (rf_fresh_id al2'))=> /=; rewrite ?dom_add_event=>->.
 Qed.
 
 Lemma dup_free_eqv es1 es2 :
@@ -722,27 +739,208 @@ Proof.
   move/dup_freeP=> I3 [al3] -> Eq.
   have N: al1 <> al3 :> edescr _ _ by rewrite -Eq=> /of_add_label_inj //.
   apply/dup_freeP=> x y /=.
-  move: (I1 x y) (I2 x y)=> /=. rewrite ?add_fedE ?inE /=.
+  move: (I1 x y) (I2 x y)=> /=. rewrite ?dom_add_event ?add_fedE ?inE /=.
   case: ifP=> /= [/eqP->|].
-  - rewrite fresh_id12 /=; case: ifP=> [/eqP->|].
+  - rewrite ?dom_add_event fresh_id12 /=; case: ifP=> [/eqP->|].
     - by rewrite fresh_id12.
     case: ifP=> /= [/eqP->|???/[apply]/[apply]//].
     move=> ????? []; case: (al1) (al3) N=> /= ??????? [/=].
     by move=>> ???? /[swap]->/[swap]->/[swap]->.
   case: ifP=> /= [/eqP->|].
-  - rewrite fresh_id12 /=; case: ifP=> /= // ?????? /esym.
+  - rewrite ?dom_add_event fresh_id12 /=; case: ifP=> /= // ?????? /esym.
     by case: (al1) (al3) N=> /= ??????? [].
   case: ifP=> /= [/eqP->|]; case: ifP=> [/eqP->|] //=.
-  - move=> ? /[dup] EN + ???? D Ef; move: (I3 (fresh_id1 es1) y)=> /=.
-    rewrite ?inE ?add_fedE {-3}EN -Ef ?eqxx D /==> /(_ erefl erefl) L.
+  - rewrite ?dom_add_event=>-> /=.
+    move=> /[dup] EN + ???? D Ef; move: (I3 (fresh_id1 es1) y)=> /=.
+    rewrite ?dom_add_event.
+    rewrite ?inE ?add_fedE {-3}EN -Ef ?eqxx /= D /==> /(_ erefl erefl) L.
     have->: fresh_id1 es1 = y by apply/L; case: (al2) (al3) Eq=> ??????? [].
     by rewrite eqxx.
-  move=> ?? /[dup] EN + ?? D ? Ef; move: (I3 x (fresh_id1 es1))=> /=.
-  rewrite ?inE ?add_fedE {-3}EN Ef ?eqxx D /==> /(_ erefl erefl) L.
-  have->: x = fresh_id1 es1 by apply/L; case: (al2) (al3) Eq=> ??????? [].
-  by rewrite eqxx.
+  - rewrite ?dom_add_event=>-> /=.
+    move=> ? /[dup] EN + ?? D ? Ef; move: (I3 x (fresh_id1 es1))=> /=.
+    rewrite ?dom_add_event.
+    rewrite ?inE ?add_fedE {-3}EN Ef ?eqxx D /==> /(_ erefl erefl) L.
+    have->: x = fresh_id1 es1 by apply/L; case: (al2) (al3) Eq=> ??????? [].
+    by rewrite eqxx.
+  by rewrite ?dom_add_event=>->->.
 Qed. 
 
+Arguments sub_eqv_comm_union {_ _ _ _ _}.
+
+Notation ptr  := (relpreim (@porf_eventstruct_of _ _ Lab) tr).
+Notation peqv := (relpreim (@porf_eventstruct_of _ _ Lab) eqv).
+
+Lemma tr_prime es pes : es ~> pes -> rf_ncf_dom es && dup_free es.
+Proof.
+  case: pes=> /= ? /[swap][[al -> /andP[/allP + /dup_freeP]]].
+  rewrite /rf_ncf_dom dom_add_event=> R D; apply/andP; split.
+  - apply/allP=> x /[dup] xD. 
+    have /R: x \in fresh_id1 es :: dom es by rewrite ?inE xD.
+    rewrite frf_add_eventE; case: ifP=> [| N].
+    - by move/eqP=> -> ? /(negP (fresh_seq_notin dom_sorted)).
+    rewrite -cf_add_eventE // ?N // lt_eqF // (fresh_seq_lt dom_sorted) //.
+    exact/frf_dom.
+  apply/dup_freeP=> ?? D1 D2 *; apply/D; rewrite ?inE ?(D1, D2) //. 
+  by rewrite ?fed_add_eventE ?lt_eqF // (fresh_seq_lt dom_sorted).
+Qed.
+
+Lemma tr_ptr : 
+  ptr^* ≡ (relpreim (@porf_eventstruct_of _ _ Lab) tr^*).
+Proof.
+  apply/(antisym ptr^*)=> [|pes1 pes2]; rewrite /relpreim.
+  - apply/str_ind_l1=> [[??[??/= [?]]]|??[x]]; first exact/(str_refl tr).
+    move=> ??; apply/(str_cons tr); by exists x.
+  move:
+    {-2}(porf_eventstruct_of pes1)
+    {-2}(porf_eventstruct_of pes2)
+    (@erefl _ (porf_eventstruct_of pes1))
+    (@erefl _ (porf_eventstruct_of pes2))=> es1 es2 ++ tr.
+    move: tr pes1 pes2.
+  suff: tr^* ≦ (fun es1 es2 => forall pes1 pes2,
+    es1 = pes1 ->
+    es2 = pes2 -> (relpreim (@porf_eventstruct_of _ _ Lab) tr)^* pes1 pes2).
+  - exact.
+  apply/str_ind_r1=> [??->??-> /prime_inj->|]; first exact/(str_refl ptr).
+  move=> ?? [? IH + ?? + Eq]; rewrite Eq=> /[dup] /tr_prime C ??.
+  apply/(str_snoc ptr); exists (PrimeES _ C)=> //; exact/IH.
+Qed.
+
+Theorem tr_confl : eqv_rconfluent ptr peqv.
+Proof.
+  apply/(@confl_sub _ _ _ (fun es => rf_ncf_dom es && dup_free es)).
+  - move=> ? L; by exists (PrimeES _ L).
+  - by case.
+  - exact/val_inj.
+  have->: forall p, rst p tr ≡ rst p (exlab ltr).
+  - by move=> ???/=; rewrite /rst /= exlab_tr.
+  apply/(sub_eqv_comm_union eqv_trans eqv_symm eqv_refl comm_ltr comm_eqv_tr).
+  - move=> ? es' /= [es]; rewrite /hrel_inj=> [[-> /andP[]]].
+    move/dom_consist_eqv=> C /dup_free_eqv D /[dup]/[dup]? /C ? /D ?.
+    exists es'=> //; split=> //; exact/andP.
+  move=>>/dup_free_add D [/= /[dup] /D{D}D /dom_consist_add C /andP[/andP[]]].
+  move/C=> {C}C /D{D}D /andP[/C{C}C /D{D}D].
+  by case=>/[dup] /C{C}C /D{D}D /= /andP[? /andP[/C{C}C /D{D}D/[dup]/C->/D->]].
+Qed.
+
+Lemma tr_ninh es : es != inh -> exists es', es' ~> es.
+Proof.
+  case: es=> fed dom; case: {1}dom (@erefl _ dom)=> [/= I ??/[dup]|fr l D].
+  - by rewrite -{1}I.
+  move=> lab fpo frf supp /[dup]; rewrite -{1}D /==> P s d i df dp vf vp sf sp.
+  rewrite /eq_op /= /eq_es /==> /[dup] F.
+  have Efr : fr = fresh (head \i0 l).
+  - case: (l) D F=> /= [F|>]; last by move/nfresh2.
+    move/nfresh1: F supp=> F; rewrite /dom F=> /eqP Es /eqP N.
+    exfalso; apply/N/fsfunP=> ?; rewrite fsfun_withE.
+    case: ifP=> [/eqP-> //|{N}N].
+    by rewrite ?fsfun_dflt // (finsupp0, Es) ?seq_fsetE ?inE // N.
+  have f0 : \i0 != fr by rewrite lt_eqF // Efr; move: (i0_fresh_seq l).
+  have npo : {in finsupp fed, forall e, fpo_prj (fed e) != fr}.
+  - move=> x /[dup] L; move: P.
+    case: (boolP (x == \i0))=> [/eqP->|?]; first by rewrite i /=.
+    rewrite (eqP supp) seq_fsetE -D path_sortedE ?inE.
+    - case/andP=> a _ O; have: x <= fr by move/orP: O=> [/eqP->|/(allP a)/ltW].
+      move=> Lf; rewrite lt_eqF //; apply/(lt_le_trans _ Lf).
+      move/forallP: vf=> /(_ [`L])/implyP /=; exact.
+    exact/rev_trans/lt_trans.
+  have nrf : {in finsupp fed, forall e, frf_prj (fed e) != fr}.
+  - move=> x /[dup] L; move: P.
+    case: (boolP (x == \i0))=> [/eqP->|?]; first by rewrite i /=.
+    rewrite (eqP supp) seq_fsetE -D path_sortedE ?inE.
+    - case/andP=> a _ O; have: x <= fr by move/orP: O=> [/eqP->|/(allP a)/ltW].
+      move=> Lf; rewrite lt_eqF //; apply/(lt_le_trans _ Lf).
+      move/forallP: vp=> /(_ [`L])/implyP /=; exact.
+    exact/rev_trans/lt_trans.
+  have n_fr : forall e, e \in l -> e != fr=> [?|].
+  - move: P; rewrite (path_sortedE (rev_trans lt_trans))=> /andP[/allP I+/I*].
+    by rewrite lt_eqF.
+  have Ed: nfresh #|` finsupp [fsfun fed without fr]|.-1 = l.
+    rewrite finsupp_without // cardfsDS ?cardfs1 -?behead_nfresh ?subn1.
+    - by rewrite -/dom -D.
+    - by apply/eqP=> N; move: N D; rewrite /dom=>-> /= [/esym/eqP/(negP f0)].
+    by apply/fsubsetP=> ?; rewrite ?inE (eqP supp) seq_fsetE -D ?inE=>->.
+  have [: a1 a2 a3 a4 a5 a6 a7 a8 a9 a10] @es : porf_eventstruct :=
+    Pack ([fsfun fed without fr]) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10;
+    rewrite ?Ed.
+  - rewrite finsupp_without ?(eqP supp) // -D.
+    apply/eqP/fsetP=> x; rewrite ?inE ?seq_fsetE ?inE.
+    case: (x =P fr)=> //=->; apply/esym/negbTE/negP; move: s=> /=.
+    rewrite -D /= (path_sortedE (rev_trans lt_trans))=> /andP[/allP L ? /L].
+    by rewrite ltxx.
+  - by move: s; rewrite -D /==> /path_sorted.
+  - by move: d f0=> /=; rewrite -D ?inE=> /orP[]// /eqP<- /[! eqxx].
+  - by rewrite fsfun_withE (negbTE f0).
+  - apply/forallP=> [[e /=]]; rewrite (eqP a1) seq_fsetE fsfun_withE=> /[dup].
+    rewrite Ed; move/n_fr/negbTE=>-> L.
+    have I : e \in (finsupp fed) by rewrite (eqP supp) seq_fsetE -D ?inE L. 
+    by move/forallP/(_ [`I]): df; rewrite/=-D ?inE=>/orP[]// /(negP (npo _ I)).
+  - apply/forallP=> [[e /=]]; rewrite (eqP a1) seq_fsetE fsfun_withE=> /[dup].
+    rewrite Ed; move/n_fr/negbTE=>-> L.
+    have I : e \in (finsupp fed) by rewrite (eqP supp) seq_fsetE -D ?inE L. 
+    by move/forallP/(_ [`I]): dp; rewrite/=-D ?inE=>/orP[]// /(negP (nrf _ I)).
+  - apply/forallP=> [[e /=]]; rewrite fsfun_withE finsupp_without // ?inE.
+    case/andP=> /negbTE-> L; exact/(forallP vf [`L]).
+  - apply/forallP=> [[e /=]]; rewrite fsfun_withE finsupp_without // ?inE.
+    case/andP=> /negbTE-> L; exact/(forallP vp [`L]).
+  - apply/forallP=> [[e /=]]; rewrite ?fsfun_withE finsupp_without // ?inE.
+    case/andP=> /negbTE-> /[dup] L /npo/negbTE->; exact/(forallP sf [`L]).
+    - apply/forallP=> [[e /=]]; rewrite ?fsfun_withE finsupp_without // ?inE.
+    case/andP=> /negbTE-> /[dup] L /nrf/negbTE->; exact/(forallP sp [`L]).
+  exists es.
+  have L : fr \in finsupp fed by rewrite (eqP supp) seq_fsetE -D ?inE eqxx.
+  have [: b1 b2 b3 b4] @al : add_label es := 
+    Add (lab fr) (fpo fr) (frf fr) b1 b2 b3 b4.
+  - rewrite -fed_supp_mem /= finsupp_without // ?inE.
+    move: (forallP vf [`L]) (forallP df [`L])=> /=.
+    rewrite ?inE [fr == _](eq_sym) f0 /= (eqP supp) seq_fsetE ?inE.
+    by move/lt_eqF->.
+  - rewrite -fed_supp_mem /= finsupp_without // ?inE.
+    move: (forallP vp [`L]) (forallP dp [`L])=> /=.
+    rewrite ?inE [fr == _](eq_sym) f0 /= (eqP supp) seq_fsetE ?inE.
+    by move/lt_eqF->.
+  - rewrite /porf_eventstruct.lab /= fsfun_withE lt_eqF.
+    - exact/(forallP sf [`L]).
+    apply/(implyP (forallP vf [`L])); by rewrite eq_sym.
+  - rewrite /porf_eventstruct.lab /= fsfun_withE lt_eqF.
+    - exact/(forallP sp [`L]).
+    apply/(implyP (forallP vp [`L])); by rewrite eq_sym.
+  exists al; apply/eqP; rewrite /eq_op /= /eq_es /=.
+  apply/eqP/fsfunP=> ?; rewrite add_fedE /= /fresh_seq /porf_eventstruct.dom.
+  move=> /=; rewrite Ed -Efr fsfun_withE; case: ifP=> [|->] // /eqP->.
+  by rewrite /lab /fpo /frf; case: (fed fr).
+Qed.
+
+Lemma dom_tr es1 es2 : es1 ~> es2 -> size (dom es2) = (size (dom es1)).+1.
+Proof. by case=> ?->; rewrite dom_add_event. Qed.
+
+Lemma dom_eqv es1 es2 : es1 ~~ es2 -> size (dom es1) = size (dom es2).
+Proof. 
+  case=> f /[dup][[_ /bij_inj ?]] /iso_dom Es.
+  rewrite -(size_map f); apply/perm_size/uniq_perm=> //; 
+  by rewrite ?map_inj_uniq ?(sorted_uniq (rev_trans (lt_trans))) // dom_sorted.
+Qed.
+
+Lemma dom_itr_tr : 
+  tr^+ ≦ (fun es1 es2 => (size (dom es1) < size (dom es2))%N).
+Proof. apply/itr_ind_l1=> [?|?? /= []]? /= /dom_tr->; ssrnatlia. Qed.
+
+Lemma dom_itr_ptr : 
+  ptr^+ ≦ (fun pes1 pes2 => (size (dom pes1) < size (dom pes2))%N).
+Proof. apply/itr_ind_l1=> [?|?? /= []]? /= /dom_tr->; ssrnatlia. Qed.
+
+Lemma init_inh (pes : prime_porf_eventstruct) : ptr^* inh pes.
+Proof.
+  rewrite tr_ptr /relpreim; case: pes=> /= pes _.
+  have [n le_size] := ubnP (size (dom pes)).
+  elim: n pes le_size=> // n IHn pes.
+  case: (pes =P inh)=>[-> *|/eqP /tr_ninh[]]; first exact/(str_refl tr).
+  move=> es es_tr s; apply/(str_snoc tr); exists es=> //.
+  apply/IHn; rewrite -(dom_tr es_tr); ssrnatlia.
+Qed.
+
+Lemma irr_ptr: ptr^+ ⊓ eqv ≦ bot.
+Proof. move=> ?? [/dom_itr_ptr ? /dom_eqv]; ssrnatlia. Qed.
+
 End Confluence.
 
 End AddEvent.