fact: Definition term_of_rec' (t : graph2 -> term sym) (G : graph2) := if [pick x | (input \notin @component_of G x) && (output \notin @component_of G x)] is Some x then top · (term_of (component1 x) · top) ∥ t (induced2 (~: component_of x)) else if output \in @component_of G input then term_of G else term_of (@component1 G input) · (top · term_of (@component1 G output)).
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)