fact: Fixpoint cpadj cm (cp : cprog) {struct cp} := match cp, cm with | CpR n :: cp', Cfmask mr mk => let: Cfmask mr' mk' := cpadj (Cfmask (rotr n mr) mk) cp' in Cfmask (rot n mr') mk' | CpY :: cp', Cfmask [:: b0, b1, b2 & mr] mk => if cpadj (Cfmask [:: b0, b2 & mr] mk) cp' is Cfmask [:: a0, a2 & mr'] mk' then Cfmask [:: a0 || b1, b0 || b2, a2 || b1 & mr'] mk' else cm | CpH :: cp', Cfmask [:: b0, b1 & mr] (b1' :: mk) => if cpadj (Cfmask [:: b0, b1' & mr] mk) cp' is Cfmask [:: a0, a1 & mr'] mk' then Cfmask [:: a0 || b1, [|| b0, b1' | head b0 mr] & if mr' is a2 :: mr'' then (a2 || b1) :: mr'' else mr'] ((a1 || b1) :: mk') else cm | [::], Cfmask [:: b0; b1] [::] => Cfmask [:: b1; b0] [::] | _, _ => cm end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)