proposition: Lemma gen_vertex_lgd_ramif: forall g gen index new_v v n e, gen_has_index g gen index -> 0 <= n < Zlength (make_fields g v) -> Znth n (make_fields g v) = inr e -> v = (gen, index) -> generation_rep g gen |-- vertex_rep (nth_sh g gen) g (gen, index) * (vertex_rep (nth_sh g gen) (labeledgraph_gen_dst g e new_v) (gen, index) -* generation_rep (labeledgraph_gen_dst g e new_v) gen).
proof: Proof. intros. unfold generation_rep. unfold nth_gen. simpl. apply iter_sepcon_ramif_pred_1. change (nth gen (g_gen (glabel g)) null_info) with (nth_gen g gen). remember (map (fun x : nat => (gen, x)) (nat_inc_list (number_of_vertices (nth_gen g gen)))). assert (In (gen, index) l) by (subst l; apply in_map; rewrite nat_inc_list_In_iff; assumption). apply In_Permutation_cons in H3. destruct H3 as [f ?]. exists f. split. 1: assumption. intros. unfold nth_sh, nth_gen. simpl. remember (generation_sh (nth gen (g_gen (glabel g)) null_info)) as sh. rewrite (lgd_vertex_rep_eq_in_diff_vert sh g new_v v x e n); try reflexivity; try assumption. assert (NoDup l). { subst l. apply FinFun.Injective_map_NoDup. 2: apply nat_inc_list_NoDup. red. intros. inversion H5. reflexivity. } apply (Permutation_NoDup H3), NoDup_cons_2 in H5. intro. rewrite H2 in H6. rewrite H6 in H4. intuition. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List