proposition: Lemma graph_right_local_facts: forall sh x (g1 g2: Graph) l l' r, vvalid g1 x -> vgamma g1 x = (true, l, r) -> vvalid g2 x -> vgamma g2 x = (true, l', r) -> edge_spanning_tree g1 (x, L) g2 -> vertices_at sh (reachable g1 x) g2 |-- valid_pointer (pointer_val_val r).
proof: Proof. intros. eapply derives_trans; [apply (@graph_ramify_aux1_right pSGG_VST (sSGG_VST sh) g1 g2 x l r); auto | ]. assert (weak_valid g2 r) by (apply (gamma_right_weak_valid g2 x true l' r); auto). destruct H4. - simpl in H4. subst r. simpl pointer_val_val. apply sepcon_valid_pointer1. unfold pred. simpl reachable_vertices_at. entailer!. - apply sepcon_valid_pointer1. apply graph_local_facts; auto. 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