proposition: Lemma mark_mark1_mark: forall m1 root l m2 m3 (R_DEC: forall x, In x l -> ReachDecidable g x (negateP m2)) (V_DEC: forall x, In x l -> Decidable (vvalid g x)), vvalid g root -> (negateP m1) root -> step_list g root l -> mark1 m1 root m2 -> mark_list m2 l m3 -> mark m1 root m3.
proof: Proof. intros. split; intros. + apply (mark1_unmarked _ _ _ _ H2) in H4. destruct H4. - subst n. destruct H2 as [_ [? _]]. eapply mark_list_marked; eauto. - destruct H4 as [z [? ?]]. unfold edge in H4; rewrite <- (H1 z) in H4. destruct H4 as [_ [_ ?]]. eapply mark_list_get_marked; eauto. + assert (m1 n <-> m2 n). { destruct H2 as [? [? ?]]. apply H6. intro. apply H4. subst. apply reachable_by_refl; auto. } rewrite H5. assert (forall x, In x l -> ~ g |= x ~o~> n satisfying (negateP m2)). { intros. intro. destruct (V_DEC x H6). + apply (mark1_reverse_unmark m1 root) in H7; auto. apply H4. apply H1 in H6. apply edge_reachable_by with x; auto. unfold edge; auto. + apply reachable_by_head_valid in H7; tauto. } eapply mark_list_preserve_marked; eauto. 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