fact: Definition ctr_decr := Eval lazy beta zeta in let dlf lf klf := if lf is CtreeLeaf lf' then klf lf' else klf lf in let dlf1 lfk lf1 lf2 lf3 := dlf lf1 (fun lf1' => lfk lf1' lf2 lf3) in let dlf2 lfk lf1 lf2 lf3 := dlf lf2 (fun lf2' => lfk lf1 lf2' lf3) in let dlf3 lfk lf1 lf2 lf3 := dlf lf3 (fun lf3' => lfk lf1 lf2 lf3') in fix ctr_decr (lf1 lf2 lf3 : ctree) (r : ctree_restriction) {struct r} : A := match r with | CtrNil => cont lf1 lf2 lf3 | CtrCons bs t r' => let lfk lf1' lf2' lf3' := ctr_decr lf1' lf2' lf3' r' in match t, bs with | GtreeLeaf0, _ => dlf2 (dlf3 lfk) lf1 lf2 lf3 | GtreeLeaf1, _ => dlf1 lfk lf1 lf2 lf3 | GtreeLeaf2, Bpush0 _ => dlf2 lfk lf1 lf2 lf3 | GtreeLeaf2, Bpush1 _ => dlf3 lfk lf1 lf2 lf3 | GtreeLeaf3, Bpush0 _ => dlf3 lfk lf1 lf2 lf3 | GtreeLeaf3, Bpush1 _ => dlf2 lfk lf1 lf2 lf3 | GtreeLeaf01, _ => dlf1 (dlf2 (dlf3 lfk)) lf1 lf2 lf3 | GtreeLeaf12, Bstack0 => dlf1 lfk lf1 lf2 lf3 | GtreeLeaf12, Bpush0 _ => dlf1 (dlf2 lfk) lf1 lf2 lf3 | GtreeLeaf12, Bpush1 _ => dlf1 (dlf3 lfk) lf1 lf2 lf3 | GtreeLeaf13, Bstack0 => dlf1 lfk lf1 lf2 lf3 | GtreeLeaf13, Bpush0 _ => dlf1 (dlf3 lfk) lf1 lf2 lf3 | GtreeLeaf13, Bpush1 _ => dlf1 (dlf2 lfk) lf1 lf2 lf3 | GtreeLeaf23, Bpush0 _ => dlf2 (dlf3 lfk) lf1 lf2 lf3 | GtreeLeaf23, Bpush1 _ => dlf2 (dlf3 lfk) lf1 lf2 lf3 | _, _ => lfk lf1 lf2 lf3 end end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)