fact: Fixpoint ctree_pick_rev_rec (et : colseq) e t' t {struct t} : colseq := match t with | CtreeLeaf _ => if ctree_mem t' (etrace (belast e et)) then e :: et else [::] | CtreeNode t1 t2 t3 => if ctree_pick_rev_rec (Color1 :: et) (e +c Color1) t' t1 is e' :: et' then e' :: et' else if ctree_pick_rev_rec (Color2 :: et) (e +c Color2) t' t2 is e' :: et' then e' :: et' else ctree_pick_rev_rec (Color3 :: et) (e +c Color3) t' t3 | _ => [::] end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)