fact: Fixpoint graph_to_tree (limit: nat) (root: Vertex): nat * Tree := match limit with | O => (O, EPT) | S n => let vertices_list := nodup veq_dec (filter not_null_bool (map (dst G) (edge_func G root))) in let (total, sub_trees) := to_tree_list n vertices_list (0, nil) in (1 + total, T root sub_trees) end with to_tree_list (limit: nat) (l: list Vertex) (result: nat * list Tree) : nat * list Tree := match limit with | O => result | S n => match l with | nil => result | x :: tl => let (current, tr) := graph_to_tree n x in if eq_nat_dec current O then result else to_tree_list (n - current) tl (fst result + current + 1, tr :: snd result) end end.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List