HeapADT

spec

HeapNode

LeftistHeap

Heap_List_BisimulationSpec

spec

h

Cons Cons PCons

hasDescendant

AHeap

hasKey

PList

hasKey_contains

PairListLemmas

hasNext

Iterator ListIterator

has_descendant_tran

AHeap

head

List Oracle List PList ArrayList Iterator LinkedList ListADT ListIterator MapArrayList

headOption

List List PList

headReverseLast

ListSpecs ListLemmas

head_bisim

LinkedListArrayListBisimulation LinkedListMapArrayListBisimulation

heap

LeftistHeapOps

holds

BooleanDecorations