proposition: Lemma lacv_generation_rep_not_eq: forall g v to n, n <> to -> graph_has_gen g to -> no_dangling_dst g -> copy_compatible g -> generation_rep (lgraph_add_copied_v g v to) n = generation_rep g n.
proof: Proof. intros. unfold generation_rep. rewrite lacv_nth_gen by assumption. apply iter_sepcon_func_strong. intros. apply list_in_map_inv in H3. destruct H3 as [m [? ?]]. unfold nth_sh. rewrite lacv_nth_gen by assumption. remember (generation_sh (nth_gen g n)) as sh. unfold vertex_rep. subst x. assert (graph_has_v g (n, m)). { rewrite nat_inc_list_In_iff in H4. destruct (Nat.lt_ge_cases n (length (g_gen (glabel g)))). - split; simpl; assumption. - exfalso. unfold nth_gen in H4. rewrite nth_overflow in H4 by assumption. simpl in H4. lia. } f_equal. - apply lacv_vertex_address_old; assumption. - apply lacv_make_header_old. intro S; inversion S. contradiction. - apply lacv_make_fields_vals_old; assumption. 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