proposition: Lemma root_update_ramify : forall (g: Graph) (x x0: addr) (lx: addr) (gx gx': addr * addr * addr) F, vgamma g x = gx -> vgamma (Graph_vgen g x lx) x = gx' -> vvalid g x -> @derives pred _ (F * @reachable_vertices_at _ _ _ _ (@SGBA pSGG_Bin) _ _ _ (@SGC_Bin pSGG_Bin _ _ _) _ (@SGP pSGG_Bin _ _ sSGG_Bin) (@SGA pSGG_Bin _ _ sSGG_Bin) x g) (vertex_at x gx * (vertex_at x gx' -* F * (@vertices_at _ _ _ _ (@SGBA pSGG_Bin) _ (@SGP pSGG_Bin _ _ sSGG_Bin) _ (Intersection _ (vvalid (initial_copied_Graph x x0 g)) (fun u : addr => x0 <> u)) (initial_copied_Graph x x0 g) * reachable_vertices_at x (Graph_vgen g x lx)))).
proof: Proof. intros. rewrite !(sepcon_comm F). apply RAMIF_PLAIN.frame. assert (@vertices_at _ _ _ _ (@SGBA pSGG_Bin) _ (@SGP pSGG_Bin _ _ sSGG_Bin) _ (Intersection _ (vvalid (initial_copied_Graph x x0 g)) (fun u : addr => x0 <> u)) (initial_copied_Graph x x0 g) = emp). { erewrite <- vertices_at_False. apply vertices_at_Same_set. rewrite Same_set_spec; intros ?. Transparent initial_copied_Graph. simpl. Opaque initial_copied_Graph. unfold update_vlabel. if_tac; [| congruence]. split; [intros [? ?]; congruence | tauto]. } rewrite H2, emp_sepcon. apply va_reachable_root_update_ramify; auto. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize VST.msl.ramification_lemmas VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon 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 CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.graph_morphism CertiGraph.graph.local_graph_copy CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.Graph_Copy Coq.Logic.Classical