proposition: Lemma exp_mark1: forall (g: Graph) (x: V) (lx: bool), WeakMarkGraph.label_marked lx -> @derives Pred _ (reachable_vertices_at x (labeledgraph_vgen g x lx)) (EX g': Graph, !! (mark1 x g g') && reachable_vertices_at x g').
proof: Proof. intros. apply (exp_right (labeledgraph_vgen g x lx)). apply andp_right; [apply prop_right | auto]. apply WeakMarkGraph.vertex_update_mark1; 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