proposition: Lemma Kempe_completeP ctu ctr gtr gtu : Kempe_valid ctu ctr gtr gtu -> Kempe_complete 1 ctu ctr gtr gtu -> forall et, size et = h.+1 -> reflect (Kempe_coclosure P (ctrace et)) (~~ ctree_mem ctu (etrace et)).
proof: Proof. move=> valid_gt [ctu0 closed_et0] et0 sz_et0. apply: (iffP idP) => [|clPet0]; first exact: (Kempe_validP valid_gt). have{valid_gt} [[ctu_ok Dctu] _ Dgtr Dgtu closedP] := valid_gt. have{ctu0} [|[ctr0 /(_ _)/idP-gtr0]] := ctu0. by rewrite ltnS leqn0 => /eqP/(ctree_size_proper ctu_ok)->. have ctu0 et: sub_gt gtu et = 0 -> ~ ctree_mem ctu et. by rewrite /ctree_mem Dctu => ->; rewrite /gtree_sub match_count_0 ?if_same. have gtu132 et: sub_gt gtu et = 0 -> sub_gt gtu (permt Eperm132 et) = 0. apply: contra_eq => /match_countP[w]; rewrite matchpg_flip => gtu_w et_w. by apply/match_countP; exists w. have ctu132 et: ctree_mem ctu (permt Eperm132 (etrace et)) -> ctree_mem ctu (etrace et). - rewrite {2}/ctree_mem Dctu even_etrace {1}/gtree_sub match_count_0 //=. by apply: contraNneq => /gtu132/ctu0/idP. have Pctue et: ctree_mem ctu (etrace et) = ctree_mem ctu et || ctree_mem ctu (permt Eperm132 et). - have /orb_idl := ctu132 et; rewrite /etrace /etrace_perm. by case: ifP => _; rewrite ?permt_id ?etrace_id // orbC. pose tr_ctu cet := exists2 et, cet = ctrace et & ctree_mem ctu (etrace et). move Dcet0: (ctrace et0) => cet0 in clPet0; apply/negP=> ctu_et0. have [cet [et -> ct_et2] | | et Pet []] := clPet0 tr_ctu; try by exists et0. set et2 := etrace et in ct_et2; split=> [g|]. exists (permt g et); first by rewrite ctrace_permt. have [g2 <-]: exists g2, permt g2 et2 = permt g et. have [g2 Dg2] := compose_permt g (etrace_perm et) et2. exists g2; rewrite Dg2 /et2 /etrace /etrace_perm. by case: ifP; rewrite ?permt_id ?etrace_id. apply: contraLR ct_et2; rewrite !Pctue {2}/permt -map_comp => ct'et2. have [||gt'et] := closed_et0 et; rewrite ?ctr0 //. right; exists (inv_eperm g2 Color1); apply/negP; case/norP: ct'et2. by case: g2 => // _; congr (~~ ctree_mem _ _ = _); apply: eq_map => [] []. by apply/norP; split; apply/negP; apply: ctu0 => //; apply: gtu132. have /match_countP[w gt_w wMet2]: sub_gt gtu et2 != 0 by apply/eqP=> /ctu0. have /andP[sz_w bal_w] := Dgtu _ gt_w. exists (cgram 0 false w); first by rewrite matchpg_etrace -matchg_pg in wMet2. move=> cet1 cet1Mw; have [et1 Det1]: exists et1, cet1 = ctrace et1. have:= balanced_sumt0 bal_w cet1Mw. case/lastP: cet1 cet1Mw => [|et1 e _]; first by case w. rewrite -{1}cats1 /sumt foldr_cat /= addc0 => sum_et1_0. exists et1; congr rcons; rewrite -[e]add0c -{}sum_et1_0. by elim: et1 e => /= [|e1 et1 IHet] e; rewrite ?addcc // -addcA IHet. exists et1 => //; rewrite Det1 matchg_pg // in cet1Mw. rewrite /ctree_mem Dctu even_etrace addn_eq0; apply/nandP; right. by apply/match_countP; exists w; rewrite ?matchpg_etrace. move=> cet Dcet ct_cet. case: (closed_et0 cet); rewrite ?ctr0 -?Dcet //; first by left. move=> gt'_cet; case/negP: ct_cet; rewrite Dctu even_etrace. have ->: sub_gt gtu (etrace cet) = 0. by rewrite /etrace /etrace_perm; case: ifP => _; rewrite (permt_id, gtu132). by rewrite addn0; apply/match_countP=> -[w1 /idPn[]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring cfmap) fourcolor(cfcolor dyck ctree initctree gtree initgtree) fourcolor(gtreerestrict ctreerestrict)