proposition: Lemma local_confluence_aux (G : pre_graph) (isG : is_graph G) Gl Gr : ostep G Gl -> ostep G Gr -> exists Gl' Gr', (osteps Gl Gl' /\ osteps Gr Gr') /\ (Gl' ≡G Gr').
proof: Proof. Proof with eauto with typeclass_instances. move => S1 S2. wlog : Gl Gr S1 S2 / step_order S1 <= step_order S2. { move => W. case/orb_sum: (leq_total (step_order S1) (step_order S2)) => SS. - exact: W SS. - case: (W _ _ _ _ SS) => H' [G'] [[stpG stpH] E]. do 2 eexists; split; first split. 1-2:eassumption. by symmetry. } destruct S1 as [z Vz Iz zIO| x z e u Iz zIO arc_e xDz | x y z e1 e2 u v Iz e1De2 zIO xDz yDz arc_e1 arc_e2| x e u arc_e | x y e1 e2 u v e1De2 arc_e1 arc_e2]; destruct S2 as [z' Vz' Iz' zIO'| x' z' e' u' Iz' zIO' arc_e' xDz'| x' y' z' e1' e2' u' v' Iz' e1De2' zIO' xDz' yDz' arc_e1' arc_e2'| x' e' u' arc_e' | x' y' e1' e2' u' v' e1De2' arc_e1' arc_e2']; rewrite //=; move => CASE_TAG. - case: (altP (z =P z')) => [?|D]. + subst z'. do 2 exists ((G \ z)%O). split => //. + exists (G \ z \ z')%O. exists (G \ z' \ z)%O. rewrite {2}remove_vertexC. split => //. split; apply ostep_step,ostep_v0 => //=. 2,4: by rewrite edges_at_del Iz Iz' fsetD0. all: by rewrite !inE ?D 1?eq_sym ?D. - have D : z != z'. { apply: contra_eq_neq Iz => ->. by rewrite Iz' fset01. } e2split. + eapply ostep_step,ostep_v1. 3: eapply oarc_remove_vertex,arc_e'. all: try done. * by rewrite edges_at_del Iz Iz' fsetD0. * by rewrite Iz inE. + eapply ostep_step,(ostep_v0 (z := z)). 3:done. * by rewrite !inE D /=. * by rewrite edges_at_del edges_at_test Iz fset0D. + by rewrite remove_vertexC remove_vertex_add_test. - have D : z != z'. { apply: contra_eq_neq Iz' => <-. by rewrite Iz eq_sym fset1U0. } have [? ?] : x' != z /\ y' != z. { split. - apply: contra_eq_neq Iz => <-. apply/fset0Pn; exists e1'. exact: oarc_edge_atL arc_e1'. - apply: contra_eq_neq Iz => <-. apply/fset0Pn; exists e2'. exact: oarc_edge_atR arc_e2'. } e2split. + eapply ostep_step,ostep_v2. 6-7: apply: oarc_remove_vertex. 7: apply arc_e1'. 8: apply: arc_e2'. all: try done. all: by rewrite ?edges_at_del ?Iz ?Iz' ?fsetD0 ?inE. + eapply ostep_step,(ostep_v0 (z := z)). 3:done. by rewrite !inE D. rewrite @edges_at_add_edge' //=. * by rewrite edges_at_del Iz fset0D. * by rewrite Iz' maxn_fsetD. + by rewrite -remove_vertex_add_edge 1?eq_sym 1?remove_vertexC //= Iz' maxn_fsetD. - have zDx : z != x'. { apply: contra_eq_neq Iz => ->. apply/fset0Pn. exists e'. exact: oarc_edge_atL arc_e'. } e2split. + eapply ostep_step,ostep_e0. apply: oarc_remove_vertex arc_e'. by rewrite Iz inE. + eapply ostep_step,(@ostep_v0 _ z) => //. by rewrite edges_at_test edges_at_remove_edges Iz fset0D. + by rewrite /= -remove_vertex_add_test -remove_vertex_edges. - have[zDx zDy] : z != x' /\ z != y'. { split;apply: contra_eq_neq Iz => ->;apply/fset0Pn;exists e1'. exact: oarc_edge_atL arc_e1'. exact: oarc_edge_atR arc_e1'. } e2split. + eapply ostep_step,ostep_e2. exact: e1De2'. all: apply oarc_remove_vertex; eauto. all: by rewrite Iz inE. + eapply ostep_step,(@ostep_v0 _ z) => //. rewrite edges_at_add_edge' 1?eq_sym ?maxn_fsetD //. by rewrite edges_at_remove_edges Iz fset0D. + by rewrite remove_vertex_edges remove_vertex_add_edge ?maxn_fsetD. - case: (altP (z =P z')) => [E|D]; last case: (altP (e =P e')) => [E|E]. + subst z'. have ? : e' = e by apply: oarc_uniqeR arc_e'. subst e'. have ? : x = x' by apply: oarc_injL arc_e arc_e'. subst x'. apply: close_same_step. suff -> : [dom (u·elem_of (lv G z))] ≡ [dom (u'·elem_of (lv G z))] by []. move => ? ?. by rewrite eqv_testE (oarc_eqv _ arc_e arc_e'). + subst e'. case: (same_oarc arc_e arc_e') => [[? ? U]|[? ? U]]; subst z' x'; first by rewrite eqxx in D. e2split. * eapply ostep_step, (@ostep_v0 _ x) => //. rewrite !inE eq_sym D. exact: oarc_vsetL arc_e. by rewrite edges_at_del !edges_at_test Iz Iz' fsetDv. * eapply ostep_step, (@ostep_v0 _ z) => //. rewrite !inE D. exact: oarc_vsetR arc_e. by rewrite edges_at_del !edges_at_test Iz Iz' fsetDv. * by rewrite remove_vertexC [in X in _ ≡G X]remove_vertexC !add_testK remove_vertexC. + gen have H,Hz : z z' x x' e e' u u' Iz Iz' arc_e' arc_e E {xDz xDz' zIO zIO' D} / z != x'. { apply: contraTneq E => ?. subst x'. rewrite negbK eq_sym -in_fset1 -Iz. apply: oarc_edge_atL arc_e'. } have {H} Hz' : z' != x by apply: H arc_e arc_e' _ ; rewrite // eq_sym. do 2 eexists. split. split. * eapply ostep_step, ostep_v1. 3: eapply oarc_remove_vertex. 4: apply arc_e'. all: try done. by rewrite edges_at_del /= !edges_at_test Iz' Iz mem_fsetD1 // inE. by rewrite edges_at_test Iz inE eq_sym. * eapply ostep_step, ostep_v1. 3: eapply oarc_remove_vertex. 4: apply arc_e. all: try done. by rewrite edges_at_del /= !edges_at_test Iz' Iz mem_fsetD1 // inE eq_sym. by rewrite edges_at_test Iz' inE. * by rewrite !remove_vertex_add_test remove_vertexC add_testC /= !updateE. - have zDz' : z != z' by apply: degree_one_two Iz Iz'. case: (boolP (z \in [fset x';y'])) => [z_xy'|xD']. + wlog: x' y' xDz' yDz' u' v' e1' e2' arc_e1' arc_e2' Iz' e1De2' {z_xy'} / z = y' => [W|?]. { move: z_xy'. rewrite !inE. case/orb_sum => /eqP E ; last exact: W. rewrite -> oarc_cnv in arc_e1',arc_e2'. move/(_ y' x' yDz' xDz' _ _ _ _ arc_e2' arc_e1') in W. rewrite fsetUC eq_sym in W. case: W => // Gl [Gr] [[S1 S2] WG]. exists Gl. exists Gr. do 2 (split => //). rewrite-> maxnC, flip_step ; eauto with vset. by rewrite !cnvdot cnvtst dotA. } subst y'. have ? : e2' = e by apply: oarc_uniqeR arc_e2'. subst e2'. have ? : x = z' by apply: oarc_injL arc_e arc_e2'. subst x. have Dz : x' != z. { apply: contra_neq e1De2' => ?. subst. exact: oarc_uniqeL arc_e1'. } e2split. * eapply ostep_step, ostep_v1. 3: { apply: oarc_remove_vertex arc_e1'. by rewrite Iz inE. } all: try done. rewrite edges_at_del !edges_at_test Iz Iz'. by rewrite fsetDUl fsetDv fsetU0 mem_fsetD1 // inE eq_sym. * eapply ostep_step, ostep_v1. 3: exact: oarc_added_edge. all: try done. rewrite edges_at_add_edge ?edges_at_del Iz Iz'. rewrite [_ `\` _](_ : _ = fset0) ?fsetU0 //. apply/eqP. by rewrite fsetD_eq0 fsub1set in_fset2 eqxx. * rewrite /= updateE. set a := lv G z. set b := lv G z'. rewrite -remove_vertex_add_test remove_vertexC add_testK. rewrite -remove_vertex_add_test add_edgeKr /= ?Iz' ?maxn_fsetD //. apply: add_test_morphism => //=. rewrite eqv_testE (oarc_eqv _ arc_e2' arc_e) //. exact: critical_pair3. + move: xD'. rewrite in_fset2 negb_or => /andP [zDx zDy]. have E1 : e1' != e. { rewrite -in_fset1 -Iz. apply/negP => H. move:(edges_at_oarc H arc_e1'). case => ?;subst; by rewrite eqxx in zDx zDz'. } have E2 : e2' != e. { rewrite -in_fset1 -Iz. apply/negP => H. move:(edges_at_oarc H arc_e2'). case => ?;subst; by rewrite eqxx in zDy zDz'. } have Z : z' != x. { apply: contraTneq (oarc_edge_atL arc_e) => <-. by rewrite Iz' in_fset2 negb_or ![e == _]eq_sym E1. } have ? : e \notin [fset e1';e2'] by rewrite in_fset2 negb_or ![e == _]eq_sym E1. e2split. * eapply ostep_step, ostep_v2. 6: { apply: oarc_remove_vertex. 2: apply: arc_e1'. by rewrite edges_at_test Iz inE. } 6: { apply: oarc_remove_vertex. 2: apply: arc_e2'. by rewrite edges_at_test Iz inE. } all: try done. by rewrite edges_at_del !edges_at_test Iz Iz' mem_fsetD1. * eapply ostep_step, ostep_v1. 3: { apply: oarc_add_edge. 2:apply: oarc_remove_vertex arc_e. apply: fset2_maxn_neq => //. by rewrite Iz'. } all: try done. rewrite edges_at_add_edge' ?[_ == z]eq_sym //= ?edges_at_del ?Iz Iz' ?maxn_fsetD //. by rewrite -fsetDDl !mem_fsetD1 ?inE. * set e12 := maxn _ _. set a := lv G z. set b := lv G z'. set a' := lv _ z. set b' := lv _ z'. have <- : a = a' by []. have <- : b = b'. rewrite /b /b' /= updateE //. rewrite remove_vertexC -remove_vertex_add_test add_edge_test. rewrite -remove_vertex_add_edge //. by rewrite /= inE negb_and negbK Iz' !inE /e12; case: (leqP e1' e2'); rewrite eqxx. - have De : e != e'. { apply: contra_neq xDz => ?; subst e'. exact: oarc_loop arc_e arc_e'. } have Dx' : x' != z. { apply: contra_neq De => ?; subst x'. symmetry. exact: oarc_uniqeL arc_e'. } e2split. * eapply ostep_step, ostep_e0. apply: oarc_remove_vertex arc_e'. by rewrite Iz !inE eq_sym. * eapply ostep_step, ostep_v1. 3: { apply: oarc_remove_edges arc_e. by rewrite inE. } all: try done. by rewrite edges_at_test edges_at_remove_edges Iz mem_fsetD1 // inE eq_sym. * rewrite /= updateE 1?eq_sym //. rewrite remove_vertex_edges -remove_edges_add_test. by rewrite remove_vertex_add_test add_testC. - gen have D,zDx : e1' e2' x' y' u' v' arc_e1' arc_e2' e1De2' / x' != z. { apply: contra_neq e1De2' => ?. subst x'. wlog suff : e1' e2' u' v' arc_e1' arc_e2' / e1' = e. { move => S. by rewrite (S _ _ _ _ arc_e1' arc_e2') (S _ _ _ _ arc_e2' arc_e1'). } apply/eqP. rewrite -in_fset1 -Iz. apply: oarc_edge_atL arc_e1'. } have {D} zDy : y' != z. { rewrite -> oarc_cnv in arc_e1',arc_e2'. apply: D arc_e2' arc_e1' _. by rewrite eq_sym. } have E1 : e1' != e. { rewrite -in_fset1 -Iz. apply/negP => H. move:(edges_at_oarc H arc_e1'). case => ?;subst; by rewrite eqxx in zDx zDy. } have E2 : e2' != e. { rewrite -in_fset1 -Iz. apply/negP => H. move:(edges_at_oarc H arc_e2'). case => ?;subst; by rewrite eqxx in zDx zDy. } have ? : e \notin [fset e1';e2'] by rewrite in_fset2 negb_or ![e == _]eq_sym E1. e2split. * eapply ostep_step, ostep_e2. -- exact: e1De2'. -- apply: oarc_remove_vertex arc_e1'. by rewrite Iz inE. -- apply: oarc_remove_vertex arc_e2'. by rewrite Iz inE. * eapply ostep_step, ostep_v1. 3: { apply: oarc_add_edge. 2: apply: oarc_remove_edges arc_e => //. exact: fset2_maxn_neq. } all: try done. rewrite edges_at_add_edge' //= ?maxn_fsetD //. by rewrite edges_at_remove_edges -fsetDDl !mem_fsetD1 // Iz in_fset1. * rewrite /= add_edge_test remove_edges_add_test -remove_vertex_add_edge -?remove_vertex_edges // 1?eq_sym //. by rewrite maxn_fsetD. - move: (fset2_cases e1De2 e1De2') => [[E|D]|[e He]]. + wlog [? ?] : x' y' e1' e2' u' v' e1De2' Iz' arc_e1' arc_e2' xDz' yDz' {E} / e1 = e1' /\ e2 = e2'. { move => W. case: (fset2_inv e1De2 E) => [[? ?]|[? ?]]; first exact: W. move/(_ y' x' e2' e1' v'° u'°) in W. rewrite fsetUC eq_sym in W. case: W => //. 1-2: by rewrite <- oarc_cnv. move => Gl [Gr] [[S1 S2] E']. e2split;[exact: S1| |exact: E']. rewrite-> maxnC, flip_step; eauto with vset. by rewrite !cnvdot cnvtst dotA. } subst e1' e2'. case: (altP (z =P z')) => [?|D]. { subst z'. eapply close_same_step. 1-2: apply add_edge_graph'; eauto with vset typeclass_instances. move: (oarc_injL arc_e1 arc_e1') (oarc_injR arc_e2 arc_e2') => ? ?. subst x' y'. by rewrite (oarc_eqv _ arc_e1' arc_e1) ?(oarc_eqv _ arc_e2' arc_e2) // eq_sym. } { case: (same_oarc arc_e1 arc_e1') => [[? ? U]|[? ? U]]; first by subst;rewrite eqxx in D. subst x x'. case: (same_oarc arc_e2 arc_e2') => [[? ? U']|[? ? U']]; first by subst;rewrite eqxx in D. subst y y'. have ?: (maxn e1 e2 |` [fset e1; e2] `\` [fset e1; e2]) `\ maxn e1 e2 = fset0. { apply/fsetP => e; rewrite !inE; case: leqP => _. all: case (altP (e =P e1)) => [?|?]; subst; rewrite ?(negbTE e1De2) //=. all: by case: (altP (e =P e2)). } e2split. * apply: ostepL. apply: ostep_e0. apply: oarc_added_edge. apply: ostep_step. apply: (@ostep_v0 _ z'). all: try done. rewrite /= in_fsetD inE eq_sym D. exact: oarc_vsetL arc_e1. rewrite /= edges_at_test edges_at_remove_edges edges_at_add_edge. by rewrite edges_at_del Iz Iz'. * apply: ostepL. apply: ostep_e0. apply: oarc_added_edge. apply: ostep_step. apply: (@ostep_v0 _ z). all: try done. rewrite /= in_fsetD inE D. exact: oarc_vsetR arc_e1. rewrite /= edges_at_test edges_at_remove_edges edges_at_add_edge. by rewrite edges_at_del Iz Iz'. * rewrite !add_testK !add_edge_remove_edgesK. 2-3: by rewrite in_fset1. by rewrite -!remove_vertex_edges remove_vertexC. } + move: (fdisjointP D) => D1. rewrite fdisjoint_sym in D. move: (fdisjointP D) => D2. have ?: x != z'. { apply: contraTneq (oarc_edge_atL arc_e1) => ->. by rewrite Iz' D1 // in_fset2 eqxx. } have ?: y != z'. { apply: contraTneq (oarc_edge_atR arc_e2) => ->. by rewrite Iz' D1 // in_fset2 eqxx. } have ?: x' != z. { apply: contraTneq (oarc_edge_atL arc_e1') => ->. by rewrite Iz D2 // in_fset2 eqxx. } have ?: y' != z. { apply: contraTneq (oarc_edge_atR arc_e2') => ->. by rewrite Iz D2 // in_fset2 eqxx. } e2split. * eapply ostep_step,ostep_v2. 7: { apply: oarc_add_edge. 2:apply: oarc_remove_vertex arc_e2'. apply: fset2_maxn_neq. by rewrite D2 // in_fset2 eqxx. by rewrite Iz D2 // !inE eqxx. } 6: { apply: oarc_add_edge. 2:apply: oarc_remove_vertex arc_e1'. apply: fset2_maxn_neq. by rewrite D2 // in_fset2 eqxx. by rewrite Iz D2 // !inE eqxx. } all: try done. rewrite edges_at_add_edge' //= ?Iz ?maxn_fsetD // edges_at_del Iz Iz'. by apply/fsetDidPl. * eapply ostep_step,ostep_v2. 7: { apply: oarc_add_edge. 2: apply: oarc_remove_vertex arc_e2. apply: fset2_maxn_neq. by rewrite D1 // in_fset2 eqxx. by rewrite Iz' D1 // in_fset2 eqxx. } 6: { apply: oarc_add_edge. 2: apply: oarc_remove_vertex arc_e1. apply: fset2_maxn_neq. by rewrite D1 // in_fset2 eqxx. by rewrite Iz' D1 // !inE eqxx. } all: try done. rewrite edges_at_add_edge' //= ?Iz' ?maxn_fsetD // edges_at_del Iz Iz'. apply/fsetDidPl. by rewrite fdisjoint_sym. * rewrite /=. rewrite -!remove_vertex_add_edge /= ?Iz ?Iz' 1?eq_sym ?maxn_fsetD //. rewrite remove_vertexC add_edge_edge //. by case: leqP => _; rewrite fset2_maxn_neq // D1 // !inE eqxx. + wlog ? : e1 e2 x y u v arc_e1 arc_e2 Iz e1De2 zIO xDz yDz He / e = e2 ; [move => W|subst e]. { have: e \in [fset e1;e2]. { move/fsetP : He => /(_ e). rewrite in_fset1 eqxx. by case/fsetIP. } rewrite inE. case/orb_sum => /fset1P => E; last exact: W. rewrite -> oarc_cnv in arc_e1,arc_e2. move/(_ _ _ _ _ _ _ arc_e2 arc_e1) in W. rewrite fsetUC eq_sym in W. case: W => // Gl [Gr] [[S1 S2] WG]. exists Gl. exists Gr. do 2 (split => //). rewrite-> maxnC, flip_step; eauto with vset. by rewrite !cnvdot cnvtst dotA. } wlog ? : e1' e2' x' y' u' v' arc_e1' arc_e2' Iz' e1De2' xDz' yDz' He / e2 = e1' ; [move => W|subst e1']. { have: e2 \in [fset e1';e2']. { move/fsetP : He => /(_ e2). rewrite in_fset1 eqxx. by case/fsetIP. } rewrite inE. case/orb_sum => /fset1P => E; first exact: W. rewrite -> oarc_cnv in arc_e1',arc_e2'. move/(_ _ _ _ _ _ _ arc_e2' arc_e1') in W. rewrite fsetUC eq_sym in W. case: W => // Gl [Gr] [[S1 S2] WG]. exists Gl. exists Gr. do 2 (split => //). rewrite-> maxnC, flip_step; eauto with vset. by rewrite !cnvdot cnvtst dotA. } have {He} E1 : e1 != e2'. { apply: contraNneq e1De2 => E. by rewrite -in_fset1 -He !inE E !eqxx. } have {arc_e2} [? ? C] : [/\ z = x' , y = z' & v ≡ u' ];[| subst x' y]. { case: (same_oarc arc_e2 arc_e1') => [//|[A B C]]; subst. move: (oarc_edge_atR arc_e1). by rewrite Iz' !inE (negbTE e1De2) (negbTE E1). } e2split. * eapply ostep_step,ostep_v2. 6: apply: oarc_added_edge. 6: apply: oarc_add_edge. 7: apply: oarc_remove_vertex arc_e2'. all: try done. -- exact: edges_replace. -- by case: (leqP e1 e2). -- apply: contraTneq (oarc_edge_atL arc_e1) => ->. by rewrite Iz' !inE negb_or e1De2. -- apply: fset2_maxn_neq. by rewrite in_fset2 ![e2' == _]eq_sym negb_or E1. -- by rewrite Iz !inE negb_or eq_sym E1 eq_sym. * eapply ostep_step,ostep_v2. 7: apply: oarc_added_edge. 6: apply: oarc_add_edge. 7: apply: oarc_remove_vertex arc_e1. all: try done. -- rewrite edges_atC fsetUC maxnC. apply: edges_replace; by rewrite // 1?fsetUC 1?eq_sym. -- by case: (leqP e2 e2'). -- apply: contraTneq (oarc_edge_atR arc_e2') => ->. by rewrite Iz !inE negb_or eq_sym E1 eq_sym. -- apply: fset2_maxn_neq. by rewrite in_fset2 negb_or e1De2. -- by rewrite Iz' !inE negb_or e1De2. * rewrite !add_edgeKr ?add_edgeKl /= ?Iz ?Iz' ?maxn_fsetD //. by rewrite remove_vertexC maxnA !dotA C. - have He : e' \notin edges_at G z. { rewrite Iz in_fset2 negb_or. apply/andP; split. - apply: contra_neq xDz => ?; subst e'. exact: oarc_loop arc_e1 arc_e'. - apply: contra_neq yDz => ?; subst e'. symmetry. exact: oarc_loop arc_e2 arc_e'. } have xDz' : z != x' by apply: contraTneq (oarc_edge_atL arc_e') => <-. have He' : e' != maxn e1 e2. apply: fset2_maxn_neq. by rewrite -Iz. e2split. * eapply ostep_step,ostep_e0. apply: oarc_add_edge He' _. exact: oarc_remove_vertex arc_e'. * eapply ostep_step,ostep_v2. 6: { apply: oarc_remove_edges arc_e1. rewrite inE. apply: contraNneq He => <-. by rewrite Iz !inE eqxx. } 6: { apply: oarc_remove_edges arc_e2. rewrite inE. apply: contraNneq He => <-. by rewrite Iz !inE eqxx. } all: try done. by rewrite edges_at_test edges_at_remove_edges -Iz mem_fsetD1. * rewrite /= !updateE //. rewrite add_edge_remove_edges ?inE 1?eq_sym //. by rewrite -remove_vertex_add_test remove_edges_vertex add_test_edge. - case: (boolP (z \in [fset x'; y'])) => Hz. + wlog ? : x' y' e1' e2' u' v' e1De2' arc_e1' arc_e2' {Hz} / z = y'. { move => W. move: Hz. rewrite in_fset2. case/orb_sum => /eqP ?; last exact: W. subst x'. rewrite -> oarc_cnv in arc_e2', arc_e1'. case: (W _ _ _ _ _ _ _ arc_e2' arc_e1'); rewrite 1?eq_sym //. move => Gl' [Gr'] [[Sl Sr] E]. e2split; [exact: Sl| |exact: E]. rewrite-> fsetUC, maxnC, flip_step; eauto with vset. by rewrite cnvpar parC. } subst y'. wlog ? : e1 e2 u v x y e1De2 arc_e1 arc_e2 xDz yDz Iz / e1' = e1. { move => W. move:(oarc_edge_atR arc_e1'). rewrite Iz in_fset2. case/orb_sum => /eqP ? ; first exact: W. subst e1'. rewrite -> oarc_cnv in arc_e2, arc_e1. case: (W _ _ _ _ _ _ _ arc_e2 arc_e1); rewrite // 1?eq_sym 1?fsetUC //. move => Gl [Gr] [[Sl Sr] E]. e2split; [ | exact: Sr|exact: E]. rewrite->maxnC, flip_step; eauto with vset. by rewrite !cnvdot cnvtst dotA. } subst e1'. have /eqP ? : e2' == e2; [|subst e2']. { move:(oarc_edge_atR arc_e2'). by rewrite Iz in_fset2 eq_sym (negbTE e1De2'). } have ? := oarc_injL arc_e1 arc_e1'. subst x'. rewrite -> oarc_cnv in arc_e2. have ? := (oarc_injL arc_e2 arc_e2'); subst y. have Eu : u ≡ u' by apply: oarc_eqv arc_e1 arc_e1'. have Ev : v° ≡ v' by apply: oarc_eqv arc_e2 arc_e2'. move => {arc_e1 arc_e1' arc_e2 arc_e2' yDz e1De2'}. e2split. * eapply ostep_step,ostep_e0. apply: oarc_added_edge. * eapply ostep_step,ostep_v1. 3: apply: oarc_added_edge. all: try done. by rewrite edges_at_add_edge ?edges_at_remove_edges -Iz ?fsetDv ?fsetU0 //= Iz maxn_fsetD. * rewrite /= !updateE. rewrite -remove_vertex_add_test add_edgeKr /= ?maxn_fsetD //. rewrite add_edge_remove_edgesK ?inE ?eqxx // remove_vertex_edges. rewrite !remove_edges_vertexK ?fsubUset ?fsub1set ?Iz ?in_fset2 ?eqxx //. apply: add_test_morphism => //=. by rewrite eqv_testE -Eu -Ev critical_pair1. by case: (leqP e1 e2); rewrite eqxx. + rewrite in_fset2 negb_or ![z == _]eq_sym in Hz. case/andP : Hz => xDz' yDz'. gen have H,H1 : e1' u' {e1De2'} arc_e1' / e1' \notin edges_at G z. { apply/negP => H. case: (edges_at_oarc H arc_e1') => ?; subst; by rewrite ?eqxx in xDz' yDz'. } move: (H _ _ arc_e2') => H2 {H}. have He1 : e1 \notin [fset e1'; e2']. { apply/negP. by case/fset2P => ?; subst; rewrite Iz !in_fset2 !eqxx in H1 H2. } have He2 : e2 \notin [fset e1'; e2']. { apply/negP. by case/fset2P => ?; subst; rewrite Iz !in_fset2 !eqxx ?orbT in H1 H2. } set e := maxn e1 e2. set e' := maxn e1' e2'. have ? : e' != e. { rewrite /e /e' eq_sym. case: (leqP e1 e2) => _; exact: fset2_maxn_neq. } e2split. * eapply ostep_step,ostep_e2. 3:{ apply: oarc_add_edge. 2:exact: oarc_remove_vertex arc_e2'. apply: fset2_maxn_neq. by rewrite -Iz. } 2:{ apply: oarc_add_edge. 2:exact: oarc_remove_vertex arc_e1'. apply: fset2_maxn_neq. by rewrite -Iz. } done. * eapply ostep_step,ostep_v2. 7: { apply: oarc_add_edge. 2:exact: oarc_remove_edges arc_e2. exact: fset2_maxn_neq. } 6: { apply: oarc_add_edge. 2: exact: oarc_remove_edges arc_e1. exact: fset2_maxn_neq. } all: try done. rewrite edges_at_add_edge' //= ?maxn_fsetD // edges_at_remove_edges. by rewrite -fsetDDl !mem_fsetD1. * rewrite /=. rewrite -remove_vertex_add_edge ?[z == _]eq_sym //= ?maxn_fsetD //. rewrite remove_edges_vertex add_edge_edge //. rewrite add_edge_remove_edges //. exact: mem_maxn. - case: (altP (e =P e')) => [?|xDx']; first subst e'. + have ? : x' = x by case: (same_oarc arc_e arc_e') => [[? ? ?]|[? ? ?]]; subst. subst. exact: close_same_step. + e2split. * eapply ostep_step,ostep_e0. apply: oarc_remove_edges arc_e'. by rewrite inE eq_sym. * eapply ostep_step,ostep_e0. apply: oarc_remove_edges arc_e. by rewrite inE. * rewrite /=. by rewrite -!remove_edges_add_test add_testC !remove_edges_edges fsetUC. - case: (boolP (e \in [fset e1'; e2'])) => He. + wlog ? : e1' e2' u' v' x' y' arc_e1' arc_e2' e1De2' {He} / e = e1'. { move => W. move: He. rewrite in_fset2. case/orb_sum => /eqP E; first exact: W. case: (W _ _ _ _ _ _ arc_e2' arc_e1' _ E); rewrite 1?eq_sym //. move => Gl [Gr] [[Sl Sr] Elr]. e2split; [exact: Sl | | exact: Elr]. by rewrite fsetUC maxnC parC. } subst e1'. move: (oarc_loop arc_e1' arc_e) => ?. subst y'. have ? : x' = x by case: (same_oarc arc_e arc_e1') => [] [? ? ?]; congruence. subst x'. e2split. * eapply ostep_step,ostep_e0. apply: oarc_remove_edges arc_e2'. by rewrite inE eq_sym. * eapply ostep_step,ostep_e0. apply: oarc_added_edge. * rewrite /= !updateE. rewrite -remove_edges_add_test remove_edges_edges add_edge_remove_edgesK ?inE ?eqxx //. rewrite remove_edges_edges [[fset _ ; _ ; _]]fsetUC [maxn _ _ |` _]mem_fset1U ?maxn_fset2 //. rewrite add_test_merge. apply: add_test_morphism => //. rewrite eqv_testE /= (oarcxx_le arc_e1') (oarcxx_le arc_e2'). by rewrite critical_pair2. + set e' := maxn _ _. have eDe' : e != e' by rewrite fset2_maxn_neq . e2split. * eapply ostep_step,ostep_e2; [exact: e1De2'| |]. -- apply: oarc_remove_edges arc_e1'. apply: contraNN He. by rewrite !inE eq_sym => ->. -- apply: oarc_remove_edges arc_e2'. apply: contraNN He. by rewrite !inE eq_sym => ->. * eapply ostep_step,ostep_e0. apply: oarc_add_edge eDe' _. exact: oarc_remove_edges arc_e. * rewrite /= -/e' updateE //. rewrite -remove_edges_add_test add_edge_remove_edges ?remove_edges_edges ?inE 1?eq_sym //. by rewrite fsetUC -add_test_edge. - case: (fset2_cases e1De2 e1De2') => [[E|D]|[e He]]. + wlog [? ?] : e1' e2' u' v' e1De2' arc_e1' arc_e2' {E} / e1 = e1' /\ e2 = e2'. { move => W. case: (fset2_inv e1De2 E) => [|[? ?]]; first exact: W. subst e2' e1'. rewrite [[fset e2;e1]]fsetUC [maxn e2 e1]maxnC. case: (W _ _ _ _ _ arc_e2' arc_e1') => // Gl [Gr] [[Sl Sr] EG]. e2split; [exact: Sl| |exact: EG]. by rewrite parC. } subst e1' e2'. wlog [? ? Hu] : x' y' u' v' {arc_e1'} arc_e2' / [/\ x = x', y = y' & u ≡ u']. { move => W. case: (same_oarc arc_e1 arc_e1') => [|[? ? Hu]]; first exact: W. subst x' y'. rewrite -> oarc_cnv in arc_e2'. case: (W _ _ u'° _ arc_e2') => //. move => Gl [Gr] [[Sl Sr] EG]. e2split; [exact: Sl| |exact: EG]. rewrite-> flip_step; eauto with vset. by rewrite cnvpar. } subst x' y'. have [Hv|[? Hv]]: ((v ≡ v') \/ (x = y /\ v ≡ v'°)). { case: (same_oarc arc_e2 arc_e2'); firstorder. } * apply close_same_step. 1-2: apply: add_edge_graph'; eauto with vset. by rewrite Hu Hv. * subst y. e2split. -- eapply ostep_step,ostep_e0. apply: oarc_added_edge. -- eapply ostep_step,ostep_e0. apply: oarc_added_edge. -- rewrite /= !updateE !add_edge_remove_edgesK ?in_fset1 ?eqxx //. apply: add_test_morphism => //. rewrite eqv_testE Hu Hv. by rewrite parA par_tst_cnv parA. + move: (fdisjointP D) => D1. rewrite fdisjoint_sym in D. move: (fdisjointP D) => {D} D2. e2split. * apply ostep_step,ostep_e2. -- exact: e1De2'. -- apply: oarc_add_edge. ++ apply: fset2_maxn_neq. by rewrite D2 // in_fset2 eqxx. ++ apply: oarc_remove_edges arc_e1'. by rewrite D2 // !inE eqxx. -- apply: oarc_add_edge. ++ apply: fset2_maxn_neq. by rewrite D2 // in_fset2 eqxx. ++ apply: oarc_remove_edges arc_e2'. by rewrite D2 // !inE eqxx. * apply ostep_step,ostep_e2. -- exact: e1De2. -- apply: oarc_add_edge. ++ apply: fset2_maxn_neq. by rewrite D1 // in_fset2 eqxx. ++ apply: oarc_remove_edges arc_e1. by rewrite D1 // !inE eqxx. -- apply: oarc_add_edge. ++ apply: fset2_maxn_neq. by rewrite D1 // !inE eqxx. ++ apply: oarc_remove_edges arc_e2. by rewrite D1 // !inE eqxx. * rewrite !add_edge_remove_edges ?D1 ?D2 ?maxn_fset2 //. rewrite !remove_edges_edges fsetUC add_edge_edge //. case: leqP => _; by rewrite fset2_maxn_neq // ?D1 ?D2 // !inE eqxx. + wlog ? : e1 e2 x y u v arc_e1 arc_e2 e1De2 He / e = e2 ; [move => W|subst e]. { have: e \in [fset e1;e2]. { move/fsetP : He => /(_ e). rewrite in_fset1 eqxx. by case/fsetIP. } rewrite inE. case/orb_sum => /fset1P => E; last exact: W. rewrite -> oarc_cnv in arc_e1,arc_e2. move/(_ _ _ _ _ _ _ arc_e2 arc_e1) in W. rewrite fsetUC eq_sym in W. case: W => // Gl [Gr] [[S1 S2] WG]. exists Gl. exists Gr. do 2 (split => //). rewrite-> maxnC, flip_step; eauto with vset. by rewrite !cnvpar parC. } wlog ? : e1' e2' x' y' u' v' arc_e1' arc_e2' e1De2' He / e2 = e1' ; [move => W|subst e1']. { have: e2 \in [fset e1';e2']. { move/fsetP : He => /(_ e2). rewrite in_fset1 eqxx. by case/fsetIP. } rewrite inE. case/orb_sum => /fset1P => E; first exact: W. rewrite -> oarc_cnv in arc_e1',arc_e2'. move/(_ _ _ _ _ _ _ arc_e2' arc_e1') in W. rewrite eq_sym [[fset e2';_]]fsetUC in W. case: W => // Gl [Gr] [[S1 S2] WG]. exists Gl. exists Gr. do 2 (split => //). rewrite-> maxnC, flip_step; eauto with vset. by rewrite !cnvpar parC. } have {He} E1 : e1 != e2'. { apply: contraNneq e1De2 => E. by rewrite -in_fset1 -He !inE E !eqxx. } wlog [? ? Hu] : x' y' u' v' {arc_e1'} arc_e2' / [/\ x' = x, y' = y & u' ≡ v]. { move => W. case: (same_oarc arc_e1' arc_e2) => [|[? ? E]]; first exact: W. rewrite -> oarc_cnv in arc_e2'. subst x' y'. case: (W _ _ u'° _ arc_e2'). split => //. by rewrite E cnvI. move => Gl [Gr] [[Sl Sr] EG]. e2split; [exact: Sl| |exact: EG]. rewrite->flip_step; eauto with vset. by rewrite !cnvpar. } subst. have He2' : e2' \notin [fset e1; e2] by rewrite !inE negb_or ![e2' == _]eq_sym E1 e1De2'. have He1 : e1 \notin [fset e2; e2'] by rewrite !inE negb_or e1De2. e2split. * eapply ostep_step,ostep_e2. 2: exact: oarc_added_edge. 2: { apply: oarc_add_edge. 2:exact: oarc_remove_edges arc_e2'. exact: fset2_maxn_neq. } by case: leqP. * eapply ostep_step,ostep_e2. 3: exact: oarc_added_edge. 2: { apply: oarc_add_edge. 2: exact: oarc_remove_edges arc_e1. exact: fset2_maxn_neq. } by case: leqP. * rewrite maxnA. set f := maxn (maxn _ _) _. rewrite !add_edge_remove_edgesK ?inE ?eqxx // !remove_edges_edges. apply: add_edge_morphism' => //; last by rewrite Hu parA. pose A := [fset e1;e2;e2']. rewrite [_ `|` _](_ : _ = A) 1?[[fset e2; e2'] `|` _](_ : _ = A) //. rewrite [_ `|` [fset maxn _ _]]fsetUC. all: rewrite fsetUC -!fsetUA. all: rewrite [maxn _ _ |` _]mem_fset1U. all: try by case: leqP; rewrite !inE eqxx. by rewrite fsetUA. by rewrite fsetUC. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)