proposition: Lemma graph_vgen_ramify: forall (g: UFGraph) x r1 r2 pa, vvalid g x -> vgamma g x = (r1, pa) -> (vertices_at (vvalid g) g: pred) |-- vertex_at x (r1, pa) * (vertex_at x (r2, pa) -* vertices_at (vvalid g) (Graph_vgen g x r2)).
proof: Proof. intros. assert (vgamma (Graph_vgen g x r2) x = (r2, pa)). { simpl in *. inversion H0. unfold vgamma, UnionFindGraph.vgamma. simpl. f_equal. unfold update_vlabel. destruct (equiv_dec x x); auto. compute in c. exfalso; auto. } apply vertices_at_ramif_1; auto. eexists. split; [|split]. - apply Ensemble_join_Intersection_Complement. + unfold Included, In; intro y. intros. subst. auto. + intros; destruct_eq_dec x x0; auto. - apply Ensemble_join_Intersection_Complement. + unfold Included, In; intro y. intros. subst. 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 H2. destruct H2. unfold Complement, In in H3. unfold vgamma, UnionFindGraph.vgamma. simpl. unfold update_vlabel. f_equal. destruct (equiv_dec x x0); auto. hnf in e. exfalso; auto. Qed.
imports: Coq.Logic.Classical Coq.Lists.List Coq.Sets.Ensembles VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.Relation_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList