proposition: Lemma CK4F_remove_edges (G : graph2) (E : {set edge G}) : CK4F G -> input != output :> G -> lens G -> components (@sinterval G input output) != set0 \/ edge_set IO :\: E != set0 -> E \subset edge_set IO -> CK4F (point (remove_edges E) input output).
proof: Proof. move => CK4F_G Hio lens_G Ps E_sub_IO. split; last by case: CK4F_G => _; apply: iso_K4_free; exact: sskeleton_remove_io. case: CK4F_G => G_conn _. apply: remove_edges_connected G_conn. suff io_conn : connect (@sk_rel _ _ (remove_edges E)) input output. { move=> e /(subsetP E_sub_IO). rewrite !inE. case/andP=> /orP[]/eqP-> /orP[]/eqP-> //. rewrite connect_symI //. exact: sk_rel_sym. } move: Ps. set sI := sinterval _ _. case. - case/set0Pn=> /= C C_comp. case/and3P: (partition_components sI) => /eqP compU compI comp0. have C_sub : C \subset sI by rewrite -compU; exact: bigcup_sup. case: (@sinterval_components G C _ _ C_comp) => -[u u_C iu][v v_C ov]. have [uNio vNio] : u \notin IO /\ v \notin IO. { have [u_sI v_sI] := (subsetP C_sub u u_C, subsetP C_sub v v_C). rewrite !in_set2. split; [move: u_sI | move: v_sI]; apply: contraTN => /orP[]/eqP->; by rewrite (@sinterval_bounds G). } have /connect1 iu_conn := remove_edges_cross (E_sub_IO) iu uNio. apply: connect_trans iu_conn _. have := remove_edges_cross (E_sub_IO) ov vNio. rewrite sk_rel_sym. move/connect1. apply: connect_trans. apply: remove_edges_restrict (E_sub_IO) _. have := @connected_in_components G sI C C_comp u v u_C v_C. apply: connect_mono. apply: restrict_mono => z /= Hz. have {Hz} Hz : z \in sI by rewrite -compU; apply/bigcupP; exists C. rewrite !inE negb_or. apply/andP. by split; apply: contraTneq Hz => ->; rewrite /sI (@sinterval_bounds G). - case/set0Pn => e /setDP [E1 E2]. apply: connect1. rewrite /sk_rel/= Hio /=. rewrite lens_io_set // in E1. case/setUP : E1 => E1. + apply: adjacentI. instantiate (1 := Sub e E2). by rewrite !inE /= in E1 *. + rewrite adjacent_sym. apply: adjacentI. instantiate (1 := Sub e E2). by rewrite !inE /= in E1 *. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)