proposition: Lemma mark_list_marked_reachable_conflict: forall m1 l m2 (R_DEC: forall x, In x l -> ReachDecidable g x (negateP m1)) (V_DEC: forall x, In x l -> Decidable (vvalid g x)), mark_list m1 l m2 -> forall n, Included (reachable_by g n (negateP m2)) (Complement _ (reachable_by_through_set g l (negateP m1))).
proof: Proof. intros. intro n'; unfold Complement, Ensembles.In; intros. intros [? [? ?]]. pose proof mark_list_get_marked _ _ _ R_DEC V_DEC H x n' H1. apply reachable_by_foot_prop in H0. change ((negateP m2) n') with (~ (m2 n')) in H0. 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