proposition: Lemma graph_gen_left_null_ramify_weak: forall (g: Graph) (x : addr) d (l r : addr), vvalid g x -> vgamma g x = (d, l, r) -> (reachable_vertices_at x g : pred) |-- vertex_at x (d, l, r) * (vertex_at x (d, null, r) -* (reachable_vertices_at x (Graph_gen_left_null g x) * TT)).
proof: Proof. intros. pose proof (graph_gen_left_null_ramify g x d l r H H0). apply log_normalize.sepcon_weaken with (vertex_at x (d, null, r) -* vertices_at (reachable g x) (Graph_gen_left_null g x)); auto. apply wand_derives; auto. unfold reachable_vertices_at. cut ((vertices_at (reachable g x) (Graph_gen_left_null g x) : pred) |-- vertices_at (reachable (Graph_gen_left_null g x) x) (Graph_gen_left_null g x) * TT). auto. unfold vertices_at. apply iter_sepcon.pred_sepcon_prop_true_weak. - apply Graph_reachable_dec, weak_valid_vvalid_dec. right. unfold Graph_gen_left_null. simpl. apply H. - intro y. unfold Graph_gen_left_null. simpl. apply is_partial_graph_reachable, pregraph_gen_dst_is_partial_graph. apply invalid_null. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext Coq.Lists.List CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind CertiGraph.graph.spanning_tree CertiGraph.graph.BinGraph CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.GraphBin_Mark