proposition: Lemma mark1_mark_list_mark: forall root l (g g': Graph), vvalid g root -> (WeakMarkGraph.unmarked g) root -> step_list g root l -> relation_list (mark1 root :: mark_list l :: nil) g g' -> mark root g g'.
proof: Proof. intros. destruct_relation_list g0 in H2. eapply (mark_list_eq root) in H2. destruct H2; simpl in H2. split. + eapply WeakMarkGraph.mark1_componded_mark_list_mark; eauto. split_relation_list (g :: g0 :: g0 :: g' :: nil); auto; apply WeakMarkGraph.eq_do_nothing; auto. + destruct H3 as [? _]. rewrite H3; auto. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.msl_application.Graph Coq.Logic.Classical