fact: Fixpoint match_count (st : spec_gtree) bs (et : colseq) {struct et} := let sub_st s w := st (s :: w) in match et with | [::] => if st [::] then 1 else 0 | Color0 :: _ => 0 | Color1 :: et' => match_count (sub_st Gskip) bs et' | Color2 :: et' => let sub_pop := match bs with | Bstack0 => 0 | Bpush0 bs' => match_count (sub_st Gpop0) bs' et' | Bpush1 bs' => match_count (sub_st Gpop1) bs' et' end in match_count (sub_st Gpush) (Bpush0 bs) et' + sub_pop | Color3 :: et' => let sub_pop := match bs with | Bstack0 => 0 | Bpush0 bs' => match_count (sub_st Gpop1) bs' et' | Bpush1 bs' => match_count (sub_st Gpop0) bs' et' end in match_count (sub_st Gpush) (Bpush1 bs) et' + sub_pop end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)