proposition: Lemma linked_heap_array_split: forall L1 L2 ptr L3 ptr', linked_heap_array (L1 ++ L2) ptr L3 ptr' = (linked_heap_array L1 ptr L3 ptr' * (!! linked_correctly' L2 L3 (Zlength L1) && heap_array L2 (field_address0 (tarray t_item (Zlength (L1 ++ L2))) [ArraySubsc (Zlength L1)] ptr)))%logic.
proof: Proof. unfold linked_heap_array. intros. rewrite heap_array_split. rewrite sepcon_assoc. rewrite (sepcon_comm (heap_array L2 _)). rewrite <- sepcon_assoc. rewrite sepcon_andp_prop'. rewrite sepcon_andp_prop. rewrite <- andp_assoc. rewrite <- prop_and. rewrite linked_correctly_app_eq. trivial. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel