proposition: Theorem term_of_iso (G : graph2) : CK4F G -> G ≃2 graph_of_term (term_of G).
proof: Proof. elim/(size_ind (@term_of_measure sym)) : G => G IH CK4F_G. rewrite term_of_eq // /term_of_rec. case: ifP => [C1|/negbT C1]. - case: picksP => [e e_io|/eqP C2]; last first. + case: pickP => [C HC|/(_ _) HC] /=. * setoid_rewrite (@split_component _ C) at 1 =>//. rewrite -?(eqP C1) ?setUid. have G_conn : connected [set: skeleton G] by case: CK4F_G. setoid_rewrite <-IH=>//. setoid_rewrite comp_dom2_redirect=>//. -- exact: measure_redirect. -- exact: CK4F_redirect. -- move: HC. rewrite -[set1 input]setUid {2}(eqP C1). exact: measure_remove_component. -- exact: CK4F_remove_component. -- by rewrite -?(eqP C1) ?setUid. * have : @components G [set~ input] == set0. { rewrite -subset0. apply/subsetP => C. by rewrite HC. } exact: componentless_one. + rewrite -> (split_io_loop e_io C1) at 1. simpl. rewrite <- IH => //. * apply: measure_remove_edges. exact: set10. * apply: CK4F_remove_loops => //. by rewrite sub1set. - case: ifP => [C2|/negbT C2]. + have EC := lens_sinterval (proj1 CK4F_G) C2. case: picksP => [e e_io|/eqP C3]; last first. * case: pickP => [C HC|]. -- rewrite EC in HC. setoid_rewrite (split_component _ HC) at 1=> //=. apply: par_iso2. ++ apply IH; rewrite -EC in HC. exact: measure_lens. exact: CK4F_lens. ++ apply IH; rewrite -EC in HC. exact: measure_lens_rest. exact: CK4F_lens_rest. -- have := split_K4_nontrivial C1 C2 _ CK4F_G. rewrite edge_set_adj // => /(_ isT)/ltnW. move=>H H'. exfalso. move: H H'. case/card_gt0P => C HC /(_ C). by rewrite HC. * rewrite EC. case: (boolP (_ && _)) => C4 /=. -- case/andP : C4 => C4 E4. rewrite -> (split_io_edge_lens e_io C2) at 1. have -> : [set e] = edge_set IO. { apply/eqP. by rewrite eqEsubset sub1set e_io -setD_eq0. } by rewrite -> componentless_top, par2top. -- setoid_rewrite (split_io_edge_lens e_io C2) at 1. apply: par_iso2 => //. rewrite negb_and -EC in C4. move/orP in C4. apply: IH. ++ apply: measure_remove_edges. exact: set10. ++ apply: CK4F_remove_edges => //=. by rewrite sub1set. + rewrite /simple_check_point_term. case: ifP => [A|/negbT A]. * rewrite /=. setoid_rewrite <-IH; first last. apply rec_bag => //; apply: CP_extensive; by rewrite !inE eqxx. apply rec_bag => //; apply: CP_extensive; by rewrite !inE eqxx. apply: CK4F_igraph => //; last rewrite cp_sym; exact: mem_cpl. apply: measure_igraph => //; by case: CK4F_G. apply rec_bag => //; apply: CP_extensive; by rewrite !inE eqxx. apply rec_bag => //; apply: CP_extensive; by rewrite !inE eqxx. case: CK4F_G => G_conn _. setoid_rewrite <-dot2A. exact: split_pip. * move: A. rewrite negb_or !negbK. case/andP => A B. rewrite /lens !negb_and A B (negbTE C1) /= in C2. case: pickP => [z Hz|C]; last first. { case:notF. apply: contraNT C2 => _. rewrite -setD_eq0. apply/eqP. apply/setP => x. by rewrite C inE. } rewrite /=. setoid_rewrite (split_cp (proj1 CK4F_G) Hz) at 1 => //. setoid_rewrite dot2A. repeat apply: dot_iso2. -- apply IH=> //. exact: measure_split_cpL. exact: CK4F_split_cpL. -- suff ? : z \in @CP G IO. { apply IH => //; by apply rec_bag. } case/setDP : Hz => Hz _. apply/bigcupP; exists (input,output) => //. by rewrite !inE !eqxx. -- apply IH=> //. exact: measure_split_cpR. exact: CK4F_split_cpR. 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)