proposition: Lemma graph_gen_left_null_ramify: 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) -* vertices_at (reachable g x) (Graph_gen_left_null g x)).
proof: Proof. intros. replace (@vertex_at _ _ _ _ _ SGP x (d, l, r)) with (graph_vcell g x). 2: { unfold graph_vcell; simpl. simpl in H0; rewrite H0; auto. } replace (@vertex_at _ _ _ _ _ SGP x (d, null, r)) with (graph_vcell (Graph_gen_left_null g x) x). 2: { unfold graph_vcell; simpl. unfold updateEdgeFunc. destruct_eq_dec (x, L) (x, L). 2: exfalso; auto. destruct_eq_dec (x, L) (x, R). inversion H2. simpl in H0; inversion H0; auto. } apply vertices_at_ramif_1; auto. eexists; split; [| split]. + apply Ensemble_join_Intersection_Complement. - unfold Included, Ensembles.In; intros; subst; apply reachable_by_refl; auto. - intros; destruct_eq_dec x x0; auto. + apply Ensemble_join_Intersection_Complement. - unfold Included, Ensembles.In; intros; subst; apply reachable_by_refl; auto. - intros; destruct_eq_dec x x0; auto. + rewrite vertices_identical_spec. simpl; intros. change (lg_gg g) with (g: LGraph). rewrite Intersection_spec in H1. destruct H1; unfold Complement, Ensembles.In in H2. simpl. unfold updateEdgeFunc. destruct_eq_dec (x, L) (x0, L). - inversion H3. exfalso; auto. - destruct_eq_dec (x, L) (x0, R). inversion H4. auto. 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