fact: Fixpoint ctrband (cm : bitseq) (cp : cprog) {struct cp} : cfmask := match cp, cm with | CpR n :: cp', _ => let: Cfmask mr mk := ctrband cm cp' in Cfmask (rot n mr) mk | [:: CpY], _ => Cfmask (nseq 3 false) [::] | CpY :: cp', b1 :: cm' => if ctrband cm' cp' is Cfmask [:: a0, a1 & mr] mk then Cfmask [:: b1 || a0, false, b1 || a1 & mr] mk else Cfmask [::] [::] | CpH :: cp', [:: b1, b0, b2 & cm'] => if ctrband cm' cp' is Cfmask [:: a0, a1, a2 & mr] mk then Cfmask [:: b0 || a0, b1, b2 || a2 & mr] ([|| b0, b1, b2 | a1] :: mk) else Cfmask [::] [::] | _, _ => Cfmask [::] [::] end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)