proposition: Lemma graph_rep_reset: forall (g: LGraph) (gen: nat), graph_has_gen g gen -> graph_rep g = graph_rep (reset_graph gen g) * generation_rep g gen.
proof: Proof. intros. unfold graph_rep. simpl. rewrite reset_nth_gen_info_length, remove_ve_glabel_unchanged. remember (length (g_gen (glabel g))). pose proof H as HS. red in H. rewrite <- Heqn in H. destruct (nat_inc_list_Permutation_cons _ _ H) as [l ?]. rewrite !(iter_sepcon_permutation _ H0). simpl. assert (iter_sepcon l (generation_rep (reset_graph gen g)) = iter_sepcon l (generation_rep g)). { apply iter_sepcon_func_strong. intros. rewrite generation_rep_reset_diff. 1: reflexivity. pose proof (nat_inc_list_NoDup n). apply (Permutation_NoDup H0) in H2. apply NoDup_cons_2 in H2. intro. subst. contradiction. } rewrite H1. clear H1. rewrite generation_rep_reset_same by assumption. rewrite emp_sepcon, sepcon_comm. reflexivity. 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