proposition: Proposition local_confluence G G' H H': step G G' -> step H H' -> G ≃2p H -> exists F, steps G' F /\ steps H' F.
proof: Proof. move => GG HH [GH]. apply ostep_of in GG as [U [[sGU] [UG']]]. apply ostep_of in HH as [V [[sHV] [VH']]]. apply oiso_of in GH. destruct (ostep_iso sGU GH) as [W [sHW UW]]. destruct (fun HF => local_confluence HF sHV sHW) as [T [sVT sWT]]. by apply GH. have gT: is_graph T. by eapply osteps_graph, sWT; apply UW. have gU: is_graph U. by apply UW. have gV: is_graph V. by apply VH'. have gW: is_graph W. by apply UW. apply (steps_of gV gT) in sVT. apply (steps_of gW gT) in sWT. exists (pack T); split. - transitivity (pack W)=>//. apply iso_step. etransitivity. apply openK. apply iso_of_oiso. eapply oiso2_trans. apply oiso2_sym. eassumption. assumption. - transitivity (pack V)=>//. apply iso_step. etransitivity. apply openK. apply iso_of_oiso. by apply oiso2_sym. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) GraphTheory(setoid_bigop structures mgraph pttdom mgraph2) GraphTheory(rewriting reduction open_confluence transfer)