fact: Definition term_of_rec (term_of : graph2 -> term sym) (G : graph2) := if input == output :> G then let E := edge_set G IO in if [pick e in E] isn't Some e then if [pick C in @components G [set~ input]] is Some C then dom (term_of (redirect C)) ∥ term_of (induced2 (~: C)) else 1 else tm_ e ∥ term_of (point (remove_edges [set e]) input output) else if lens G then let P := components (@sinterval (skeleton G) input output) in let E := edge_set G IO in if [pick e in E] isn't Some e then if [pick C in P] isn't Some C then 1 else term_of (component C) ∥ term_of (induced2 (~: C)) else if (P == set0) && (E :\ e == set0) then tm_ e else tm_ e ∥ term_of (point (remove_edges [set e]) input output) else @simple_check_point_term term_of G.
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)