proposition: Lemma generation_rep_vertex_rep: forall g gen index, gen_has_index g gen index -> generation_rep g gen |-- vertex_rep (nth_sh g gen) g (gen, index) * TT.
proof: Proof. intros. unfold generation_rep. remember (number_of_vertices (nth_gen g gen)) as num. assert (nth index (map (fun x : nat => (gen, x)) (nat_inc_list num)) (gen, O) = (gen, index)). { change (gen, O) with ((fun x: nat => (gen, x)) O). rewrite map_nth. red in H. rewrite nat_inc_list_nth by lia. reflexivity. } assert (In (gen, index) (map (fun x : nat => (gen, x)) (nat_inc_list num))). { rewrite <- H0. apply nth_In. rewrite map_length, nat_inc_list_length. red in H. subst num. assumption. } apply (iter_sepcon_in_true (vertex_rep _ g) _ _ H1). 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