proposition: Lemma lgd_gen_rep_eq_in_diff_gen: forall (g : LGraph) (v v' : VType) (x : nat) e n, 0 <= n < Zlength (make_fields g v) -> Znth n (make_fields g v) = inr e -> x <> vgeneration v -> generation_rep g x = generation_rep (labeledgraph_gen_dst g e v') x.
proof: Proof. intros. unfold generation_rep. unfold nth_sh, nth_gen. simpl. remember (nat_inc_list (number_of_vertices (nth x (g_gen (glabel g)) null_info))). apply iter_sepcon_func_strong. intros v1 H2. apply list_in_map_inv in H2. destruct H2 as [x1 [? ?]]. remember (generation_sh (nth x (g_gen (glabel g)) null_info)) as sh. assert (v1 <> v). { intro. unfold vgeneration in H1. rewrite H4 in H2. rewrite H2 in H1. unfold not in H1. simpl in H1. lia. } apply (lgd_vertex_rep_eq_in_diff_vert sh g v' v v1 e n); 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