fact: Fixpoint cfquiz_rec (qs : rqseq) (cp : cprog) {struct cp} : quiz := match cp, qs with | [::], [:: rq1, rq2 & _] => let: RingQuestion k1 a1 q1 := rq1 in let: RingQuestion k2 a2 q2 := rq2 in if ~~ (k1 && k2) then noquiz else let qa1 := large_qarity a1.-1 in let qa2 := small_qarity a2.-1 in if (qa1 != a1.+1 :> nat) || bad_small_arity qa2 then noquiz else Quiz (QaskR qa1 q2) (QaskR qa2 q1) | s :: cp', [:: rq1, rq2, rq3 & qs'] => match s with | CpR n => cfquiz_rec (rotr n qs) cp' | CpY => cfquiz_rec (cfquiz_Y rq1 rq2 (rqs_Y rq1 rq3 qs')) cp' | CpH => cfquiz_rec (cfquiz_H rq1 rq2 (rqs_H rq1 rq3 qs')) cp' | _ => noquiz end | _, _ => noquiz end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)