proposition: Lemma mark_exists: forall m x, vvalid g x -> ReachDecidable g x (negateP m) -> {m': NodePred V | mark m x m'}.
proof: Proof. intros. destruct ((node_pred_dec (negateP m)) x). + exists (existT (fun P => forall x, {P x} + {~ P x}) (fun y => g |= x ~o~> y satisfying (negateP m) \/ (m) y) (fun y => sumbool_dec_or (X y) (node_pred_dec (m) y))). split. - intros; subst; hnf. auto. - split; intros; subst; simpl in *; tauto. + exists (m). split; intros. - destruct H0 as [path ?]. apply (reachable_by_path_In g _ _ _ _ x) in H0. hnf in H0. tauto. destruct H0 as [[? _] _]. destruct path; simpl in H0; inversion H0. hnf; left; auto. - reflexivity. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2