proposition: Lemma iso_split_par2 (G : graph2) (C D : {set G}) (Ci : input \in C) (Co : output \in C) (Di : input \in D) (Do : output \in D) : C :&: D \subset IO -> C :|: D = setT -> edge_set C :&: edge_set D = set0 -> edge_set C :|: edge_set D = setT -> G ≃2 point (induced C) (Sub input Ci) (Sub output Co) ∥ point (induced D) (Sub input Di) (Sub output Do).
proof: Proof. move => subIO fullCD disjE fullE. symmetry. apply: iso2_comp. apply: (merge_subgraph_par _ _ _ _) => //=. abstract by rewrite -setI_eq0 disjE //. abstract by move => x inC inD; apply: (subsetP subIO); exact/setIP. by apply: iso2_subgraph_forT => //=; rewrite ?fullCD ?fullE. 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)