proposition: Lemma graph_local_facts: forall sh x (g: Graph), vvalid g x -> @derives mpred Nveric (graph sh x g) (valid_pointer (pointer_val_val x)).
proof: Proof. intros. eapply derives_trans; [apply (@va_reachable_root_stable_ramify pSGG_VST _ _ _ (sSGG_VST sh) g x (vgamma g x)); auto |]. simpl vertex_at. unfold trinode. simpl. entailer!. Qed.
imports: CertiGraph.dispose.env_dispose_bin CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.spanning_tree CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.GraphBin_Mark CertiGraph.data_structure.spatial_graph_dispose_bin CertiGraph.data_structure.spatial_graph_unaligned_bin_VST CertiGraph.floyd_ext.share VST.msl.wand_frame VST.floyd.reassoc_seq VST.floyd.field_at_wand