fact: Fixpoint matchg (lb : bitseq) (et : colseq) (w : chromogram) {struct w} := match w, et, lb with | [::], [::], [::] => true | s :: w', e :: et', _ => match e, s, lb with | Color1, Gskip, _ => matchg lb et' w' | Color2, Gpush, _ => matchg (false :: lb) et' w' | Color2, Gpop0, false :: lb' => matchg lb' et' w' | Color2, Gpop1, true :: lb' => matchg lb' et' w' | Color3, Gpush, _ => matchg (true :: lb) et' w' | Color3, Gpop0, true :: lb' => matchg lb' et' w' | Color3, Gpop1, false :: lb' => matchg lb' et' w' | _, _, _ => false end | _, _, _ => false end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)