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