proposition: Lemma comp_dom2_redirect (G : graph2) (C : {set G}) : connected [set: skeleton G] -> input == output :> G -> edge_set G IO == set0 -> C \in @components G [set~ input] -> component C ≃2 dom (redirect C).
proof: Proof. move => G_conn Eio no_loops HC. rewrite /redirect. case: pickP => [x /andP [inC adj_x] |]. have E : input |: (output |: C) = input |: (x |: C). { by rewrite (eqP Eio) [x |: C]setU1_mem // setUA setUid. } - apply: subgraph_for_iso => //; by rewrite ?E //= (eqP Eio). - case: (sig2W (comp_exit G_conn Eio HC)) => z Z1. rewrite sg_sym /=/sk_rel => /andP[_ B] /(_ z). by rewrite Z1 B. 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)