proposition: Lemma gen_dst_uf_root: forall (g: Graph) x y z root, vvalid g x -> ~ reachable g root x -> uf_root (pregraph_gen_dst g (out_edge x) y) z root -> reachable g z x \/ uf_root g z root.
proof: Proof. intros. assert (vvalid g z) by (destruct H1; apply reachable_head_valid in H1; simpl in H1; auto). assert (forall w, {reachable g z w} + {~ reachable g z w}). { apply (@reachable_decidable_prime _ _ _ _ g is_null); auto; [exact (P_Math g (sound_gg g)) | apply LocalFiniteGraph_FiniteGraph | apply FiniteGraph_EnumCovered]; exact (P_Finite g (sound_gg g)). } destruct (X x); [left; auto | right]. destruct H1. pose proof (P_Lst g (sound_gg g)). pose proof (vvalid_src_evalid g _ _ H). destruct H5 as [? _]. split. - rewrite not_reachable_gen_dst_equiv in H1; auto. rewrite H5; auto. - intro w. intros. apply H3. rewrite not_reachable_gen_dst_equiv; auto. rewrite H5; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext CertiGraph.lib.EnumEnsembles CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable