proposition: Lemma SpaceAdjMatGraph_unfold: forall sh (f : E -> E) g ptr (addresses0 : list val) i, let contents := (graph_to_mat g f) in 0 <= i < size -> SpaceAdjMatGraph sh f g ptr = sepcon (iter_sepcon (list_rep sh ptr contents) (sublist 0 i (nat_inc_list (Z.to_nat size)))) (sepcon (list_rep sh ptr contents i) (iter_sepcon (list_rep sh ptr contents) (sublist (i + 1) (Zlength contents) (nat_inc_list (Z.to_nat size))))).
proof: Proof. intros. unfold SpaceAdjMatGraph. apply SpaceAdjMatGraph_unfold'; trivial. subst contents. rewrite graph_to_mat_Zlength; trivial. lia. Qed.
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathAdjMatGraph