proposition: Theorem term_of_iso' (G : graph2) : K4_free (sskeleton G) -> G ≃2 graph_of_term (term_of' G).
proof: Proof. elim/card_ind : G => G IH K4F_G. rewrite term_of_eq' /term_of_rec'. case: pickP => [x /andP [X1 X2]|H]. - rewrite /=. rewrite <- term_of_iso, <- IH. + apply: iso2_disconnected_component; by rewrite inE. + exact: induced2_compN_small. + apply: subgraph_K4_free K4F_G. exact: sskeleton_subgraph_for. + exact: CK4F_component. - case: ifP; last first. + move/negbT => io. rewrite /=. rewrite <- !term_of_iso; first apply: iso_disconnected_io => //. * move => x. move/(_ x) : H. apply: contraFT. rewrite negb_or. by rewrite !(@component_exchange G x). * exact: CK4F_component. * exact: CK4F_component. + move => E. apply: term_of_iso. split => //. apply: connected_one_component (@component_of_components G input) _. apply/subsetP => x _. move/(_ x) : H. apply: contraFT => H. rewrite !(component_exchange x) H /=. by rewrite (same_component E). 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)