proposition: Lemma graph_gen_lgd_ramif: forall g v v' e n, 0 <= n < Zlength (make_fields g v) -> Znth n (make_fields g v) = inr e -> graph_has_gen g (vgeneration v) -> graph_rep g |-- generation_rep g (vgeneration v) * (generation_rep (labeledgraph_gen_dst g e v') (vgeneration v) -* graph_rep (labeledgraph_gen_dst g e v')).
proof: Proof. intros. unfold graph_rep. simpl. apply iter_sepcon_ramif_pred_1. red in H1. rewrite <- nat_inc_list_In_iff in H1. apply In_Permutation_cons in H1. destruct H1 as [f ?]. exists f. split. 1: assumption. intros. assert (NoDup (vgeneration v :: f)) by (apply (Permutation_NoDup H1), nat_inc_list_NoDup). apply NoDup_cons_2 in H3. assert (x <> vgeneration v) by (unfold not; intro; subst; contradiction). apply (lgd_gen_rep_eq_in_diff_gen g v v' x 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