proposition: Lemma split2_data_at_Tarray_space_type: forall (sh: share) (n n1: Z) (v: list (val * (val * (val*val)))) (p: val), 0 <= n1 <= n -> n = Zlength v -> data_at sh (tarray space_type n) v p = data_at sh (tarray space_type n1) (sublist 0 n1 v) p * data_at sh (tarray space_type (n - n1)) (sublist n1 n v) (field_address0 (tarray space_type n) [ArraySubsc n1] p).
proof: Proof. intros. pose proof (split2_data_at_Tarray sh space_type n n1) as HS. apply HS with (v' := v); auto. - rewrite Z.le_lteq. right; auto. - rewrite sublist_same; auto. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec)