proposition: Lemma term_of_rec_eq (f g : graph2 -> term sym) (G : graph2) : CK4F G -> (forall H : graph2, CK4F H -> measure H < measure G -> f H = g H) -> term_of_rec f G = term_of_rec g G.
proof: Proof. move=> CK4F_G Efg. rewrite /term_of_rec. case: (boolP (@input _ _ G == output)) => Hio. - case: pickP => [e Eio|Es]; last first. + case: pickP => //= C HC. rewrite !Efg //. * exact: CK4F_remove_component. * move: HC. rewrite -[set1 input]setUid {2}(eqP Hio). exact: measure_remove_component. * exact: CK4F_redirect. * exact: measure_redirect. + congr tm_par. rewrite Efg //. * apply CK4F_remove_loops => //. by rewrite sub1set. * apply: measure_remove_edges. exact: set10. - case: (boolP (lens G)) => [deg_G|ndeg_G]. + case: picksP => [e Eio|/eqP Es]; last first. * case: pickP => [C HC|//]. congr tm_par. -- apply: Efg. exact: CK4F_lens. exact: measure_lens. -- apply: Efg. exact: CK4F_lens_rest. exact: measure_lens_rest. * case: (boolP (_ && _)) => Ps //. rewrite Efg //. -- apply: CK4F_remove_edges => //. ++ rewrite negb_and in Ps. exact/orP. ++ by rewrite sub1set. -- apply: measure_remove_edges. exact: set10. + exact: simple_check_point_wf. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)