proposition: Lemma linked_correctly'_shuffle: forall contents lookup lookup' offset, linked_correctly' contents lookup offset -> Permutation lookup lookup' -> (forall i, 0 <= i < Zlength contents -> Znth (heap_item_key (Znth i contents)) lookup = Znth (heap_item_key (Znth i contents)) lookup') -> linked_correctly' contents lookup' offset.
proof: Proof. intros. destruct H as [Hz H]. split. eapply Permutation_NoDup; eauto. repeat intro. unfold loc. rewrite <- H1; trivial. apply Permutation_Zlength in H0. rewrite <- H0. apply H; 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