fact: Fixpoint cfctr (mr mc : bitseq) (cp : cprog) {struct cp} : option cprog := match cp, mr, mc with | CpR i :: cp', _, _ => let mr' := rotr i mr in if cfctr mr' mc cp' is Some cpc then Some (CpR (count negb (take i mr')) :: cpc) else None | [:: CpY], [:: b1, b2, b3 & _], _ => if nsp b1 b2 b3 then None else Some (if b1 || (b2 || b3) then [::] else [:: CpY]) | CpY :: cp', [:: b1, b2 & mr'], b3 :: mc' => if nsp b1 b2 b3 then None else if cfctr (b3 :: mr') mc' cp' is Some cpc then Some (if b1 || b2 then cpc else (if b3 then CpU else CpY) :: cpc) else None | CpH :: cp', [:: b1, b2 & mr'], [:: b3, b4, b5 & mc'] => if nsp b3 b1 b4 || nsp b3 b2 b5 then None else if [&& b1, b2 & all id mr'] then None else if cfctr [:: b4, b5 & mr'] mc' cp' is Some cpc then Some (if b3 then cpc else if b1 then if b2 then CpA :: cpc else if b5 then cpc else CpK :: cpc else if b2 then (if b4 then cpc else CpK :: cpc) else if b4 then (if b5 then CpU :: cpc else CpY :: cpc) else if b5 then CpY :: cpc else CpH :: cpc) else None | _, _, _ => None end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)