proposition: Lemma harray_split: forall L1 L2 ptr, harray (L1 ++ L2) ptr = ((harray L1 ptr) * (harray L2 (field_address0 (tarray t_item (Zlength (L1 ++ L2))) [ArraySubsc (Zlength L1)] ptr)))%logic.
proof: Proof. intros. unfold harray. rewrite map_app. erewrite split2_data_at_Tarray_app. 2: rewrite Zlength_map; reflexivity. 2: rewrite Zlength_app, Zlength_map; lia. rewrite Zlength_app. replace (Zlength L1 + Zlength L2 - Zlength L1) with (Zlength L2) by lia. trivial. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel RelationClasses