proposition: Lemma mark_list_preserve_marked: 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, (forall x, In x l -> ~ g |= x ~o~> n satisfying (negateP m1)) -> (m1 n <-> m2 n).
proof: Proof. apply (ind_RV_DEC (fun m1 l m2 => forall n, (forall x, In x l -> ~ g |= x ~o~> n satisfying (negateP m1)) -> (m1 n <-> m2 n))). + intros. apply H. + intros. rewrite <- H. - destruct H0 as [_ ?]. apply H0, H2. left; auto. - intros. intro. apply (mark_reverse_unmarked m v m') in H4; [| auto | apply R_DEC; left; auto]. apply (H2 x); auto. right; auto. 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