proposition: Proposition confluence F: forall G H, steps F G -> steps F H -> exists F', steps G F' /\ steps H F'.
proof: Proof. induction F as [F_ IH] using (well_founded_induction_type (Wf_nat.well_founded_ltof _ measure)). move=> G H S. move: G H S IH => _ H [F G FG|F__ F0 G' G FF0 FG GG] IH FH. - exists H; split=>//. by rewrite -(inhabits FG: _ ≃2p _). - move: H FH IH FF0=> _ [F H FH|F F1 H' H FF1 FH HH] IH FF0. exists G; split=>//. rewrite -(inhabits FH: _ ≃2p _). eauto using cons_step. destruct (local_confluence FG FH) as [M[GM HM]]. by rewrite -(inhabits FF0: _ ≃2p _). destruct (fun D => IH G' D _ _ GG GM) as [L[GL ML]]. rewrite /Wf_nat.ltof -(iso_stagnates (inhabits FF0)). apply /ltP. by apply step_decreases. have HL: steps H' L by transitivity M. destruct (fun D => IH H' D _ _ HL HH) as [R[LR HR]]. rewrite /Wf_nat.ltof -(iso_stagnates (inhabits FF1)). apply /ltP. by apply step_decreases. exists R. split=>//. by transitivity L. 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)