proposition: Lemma sizeOfEnum_step_list: forall root l (X: Enumerable Vertex (reachable_through_set G (nodup veq_dec (filter not_null_bool l)))) s lim, vvalid G root -> is_tree G root -> step_list G root l -> NoDup s -> (forall x, In x s <-> reachable G root x) -> 2 * (length s) - 1 <= S lim -> 2 * sizeOfEnum X <= lim.
proof: Proof. intros. destruct X as [l' [? ?]]. unfold sizeOfEnum. simpl in *. unfold Ensembles.In in i. assert (Permutation (root :: l') s). { apply NoDup_Permutation; auto. + constructor; auto. intro. rewrite i in H5. destruct H5 as [v [? ?]]. rewrite nodup_In in H5. apply (in_step_list_edge root) in H5; auto. eapply is_tree_not_to_root; eauto. + intros. simpl. rewrite i. rewrite H3. rewrite <- reachable_through_set_nonull_nodup. symmetry. apply reachable_ind.reachable_ind'; auto. } apply Permutation_length in H5. simpl in H5. clear -H5 H4. intuition. Qed.
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