proposition: Lemma iso_disconnected_io (G : graph2) : (forall x : G, (x \in @component_of G input) || (x \in @component_of G output)) -> output \notin @component_of G input -> G ≃2 @component1 G input · (top · @component1 G output).
proof: Proof. move => no_comp dis_io. symmetry. rewrite -> dot2A. rewrite -> iso2_GTG. rewrite {1}/component1. rewrite /=. move: (in_component_of _) => I1. move: (in_component_of _) => I2. have E : @component_of G output = ~: @component_of G input. { apply/setP => z. rewrite inE. apply/idP/idP. - move => Z1. apply: contraNN dis_io => Z2. by rewrite -(same_component Z2) (same_component Z1). - move/(_ z) : no_comp. by case: (z \in _). } rewrite E in I2 *. move: (@component_of_components G input) => comp_i. Iso2 (iso_component comp_i). Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)