proposition: Lemma gen_vertex_lmc_ramif: forall g gen index new_v, gen_has_index g gen index -> generation_rep g gen |-- vertex_rep (nth_sh g gen) g (gen, index) * (vertex_rep (nth_sh g gen) (lgraph_mark_copied g (gen, index) new_v) (gen, index) -* generation_rep (lgraph_mark_copied g (gen, index) 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 H0. destruct H0 as [f ?]. exists f. split. 1: assumption. intros. unfold nth_sh, nth_gen. simpl. rewrite lmc_vertex_rep_not_eq. 1: reflexivity. assert (NoDup l). { subst l. apply FinFun.Injective_map_NoDup. 2: apply nat_inc_list_NoDup. red. intros. inversion H2. reflexivity. } apply (Permutation_NoDup H0), NoDup_cons_2 in H2. intro. subst. contradiction. 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