proposition: Lemma heap_rep_ramif_stable_1: forall sh h p gen, Z.of_nat gen < MAX_SPACES -> heap_rep sh h p |-- space_struct_rep sh p h gen * (space_struct_rep sh p h gen -* heap_rep sh h p).
proof: Proof. intros. unfold heap_rep. set (Q := heap_rest_rep _). clearbody Q. remember (map space_tri (spaces h)). assert (Zlength l = MAX_SPACES) by (subst; rewrite Zlength_map; apply spaces_size). destruct (heap_struct_rep_split_single sh l p (Z.of_nat gen)) as [B ?]; try rep_lia; try assumption. rewrite H1, !Nat2Z.id. clear H1. assert (data_at sh space_type (@Znth _ (@Inhabitant_reptype CompSpecs space_type) (Z.of_nat gen) l) (space_address p gen) = space_struct_rep sh p h gen). { intros. unfold space_struct_rep. subst l. rewrite Zlength_map in H0. rewrite Znth_map by rep_lia. rewrite nth_space_Znth. reflexivity. } rewrite !H1. cancel. rewrite sepcon_assoc. apply wand_frame_intro. 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