proposition: Lemma measure_split_cpM : measure (@bgraph _ _ G IO z) < measure G.
proof: Proof. apply: (measure_node (v := input)); first apply CK4F_G. rewrite (@bag_cp G) 1?eq_sym //; first apply CK4F_G. - apply: CP_extensive. by rewrite !inE eqxx. - apply/bigcupP. exists (input,output) => //. by rewrite !inE /= !eqxx. 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)