proposition: Lemma mark_unmarked_strong: forall m1 root m2 n1 n2, vvalid g root -> ReachDecidable g root (negateP m1) -> mark m1 root m2 -> g |= n1 ~o~> n2 satisfying (negateP m1) -> Decidable (g |= n1 ~o~> n2 satisfying (negateP m2)).
proof: Proof. intros. pose proof mark_unmarked _ _ _ _ _ H X H0 H1. destruct (node_pred_dec (m2) n2); [| left; tauto]. right. intro. rewrite reachable_by_eq_subgraph_reachable in H3. apply reachable_foot_valid in H3. simpl in H3. destruct H3. rewrite negateP_spec in H4; tauto. 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