proposition: Lemma lookup_oob_eq_Zexchange: forall L1 L2 j k, 0 <= j < Zlength L1 -> 0 <= k < Zlength L1 -> linked_correctly L1 L2 -> lookup_oob_eq (Zexchange L1 j k) L2 (Zexchange L2 (heap_item_key (Znth j L1)) (heap_item_key (Znth k L1))).
proof: Proof. repeat intro. destruct H1 as [Hz H1]. split; repeat rewrite Zlength_Zexchange in *. apply Zexchange_Permutation. intros. rewrite Znth_Zexchange''; auto. destruct (H1 _ H); auto. destruct (H1 _ H0); auto. intro. subst i. eapply H2. apply H0. rewrite Znth_Zexchange'; auto. intro. subst i. eapply H2. apply H. rewrite Znth_Zexchange; auto. 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