proposition: Lemma split_cp (G : graph2) (u : skeleton G) : connected [set: skeleton G] -> u \in @cp G input output :\: IO -> edge_set (@bag G IO input) == set0 -> edge_set (@bag G IO output) == set0 -> G ≃2 @igraph _ _ G input u · (@bgraph _ _ G IO u · @igraph _ _ G u output).
proof: Proof. move => conn_G proper_u Ei0 Eo0. symmetry. have Dio: input != output :> G. { apply: contraTneq proper_u => <-. by rewrite setUid cpxx setDv inE. } have [? ? ?] : [/\ input \in @CP G IO, output \in @CP G IO & u \in @CP G IO]. { split; rewrite CP_set2 ?(@mem_cpl G) //; by [rewrite cp_sym (@mem_cpl G)|set_tac]. } rewrite-> dot2A. rewrite /= {1}/igraph /bgraph /induced. setoid_rewrite-> merge_subgraph_dot=>//. 2: by rewrite disjoint_sym interval_edges_sym interval_bag_edges_disj. 2: move => x A B; rewrite interval_sym in A; exact: (@bag_interval_cap G) B A. move: (union_bij_proofL _ _) => Pi. move: (union_bij_proofR _ _) => Po. move: (consistentU _ _) => con1. rewrite /igraph. setoid_rewrite merge_subgraph_dot=>//. apply iso2_subgraph_forT=>//. - move => x. have: x \in @interval G input output. { move: (sinterval_bag_cover conn_G Dio). rewrite (eqP (edgeless_bag _ _ _)) // (eqP (edgeless_bag _ _ _)) //. rewrite setUC setUA [[set _;_]]setUC -/(@interval G _ _) => <- //. } rewrite (interval_cp_cover conn_G proper_u) /interval. by set_tac. - move => e. have: e \in interval_edges input output. { move: (interval_bag_edge_cover conn_G Dio). by rewrite (eqP Ei0) (eqP Eo0) set0U setU0 => <-. } by rewrite (interval_cp_edge_cover conn_G proper_u). - apply: disjointsU. apply: interval_edges_disj_cp. by set_tac. apply: interval_bag_edges_disj => //. - move => x. case/setUP. apply: (@interval_interval_cap G). by set_tac. exact: (@bag_interval_cap G). Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(bij set_tac digraph sgraph minor checkpoint) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(skeleton bounded equiv extraction_def)