proposition: Lemma frames_shell_rep_isolate: forall sh frs k, 0 <= k < Zlength frs -> frames_shell_rep sh frs |-- frame_shell_rep sh (Znth k frs) (frames_p (sublist (k+1) (Zlength frs) frs)) * (frame_shell_rep sh (Znth k frs) (frames_p (sublist (k+1) (Zlength frs) frs)) -* frames_shell_rep sh frs).
proof: Proof. induction frs; simpl; intros. list_solve. destruct (zeq k 0). - subst k. change (a::frs) with ([a]++frs). autorewrite with sublist. cancel. apply wand_sepcon_adjoint. cancel. - change (a::frs) with ([a]++frs). replace (Znth k ([a]++frs)) with (Znth (k-1) frs) by list_solve. autorewrite with sublist. specialize (IHfrs (k-1)). replace (k-1+1) with k in IHfrs by lia. sep_apply IHfrs; clear IHfrs. list_solve. cancel. apply -> wand_sepcon_adjoint. cancel. apply wand_sepcon_adjoint. cancel. Qed.
imports: VST.veric.rmaps CertiGraph.lib.List_ext CertiGraph.graph.graph_model Coq.Program.Basics CertiGraph.graph.graph_gen CertiGraph.CertiGC.GCGraph VST.msl.wand_frame CertiGraph.CertiGC.env_graph_gc CertiGraph.CertiGC.spatial_gcgraph CertiGraph.msl_ext.iter_sepcon CertiGraph.CertiGC.gc_spec CertiGraph.msl_ext.ramification_lemmas CertiGraph.CertiGC.forward_lemmas