proposition: Lemma graph_gen_lmc_ramif: forall g v new_v, graph_has_gen g (vgeneration v) -> graph_rep g |-- generation_rep g (vgeneration v) * (generation_rep (lgraph_mark_copied g v new_v) (vgeneration v) -* graph_rep (lgraph_mark_copied g v new_v)).
proof: Proof. intros. unfold graph_rep. simpl. apply iter_sepcon_ramif_pred_1. red in H. rewrite <- nat_inc_list_In_iff in H. apply In_Permutation_cons in H. destruct H as [f ?]. exists f. split. 1: assumption. intros. assert (NoDup (vgeneration v :: f)) by (apply (Permutation_NoDup H), nat_inc_list_NoDup). apply NoDup_cons_2 in H1. rewrite <- lmc_generation_rep_not_eq. 1: reflexivity. 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