BigInt
lang
BigIntArrayHeap
spec
Bisimulation
List
BlackTree
RedBlackTree
BooleanDecorations
lang
BoundedArray
spec
BoundedArrayLemmas
spec
balance
Leaf
Node
TreeNode
because
ProofOps
bigIntToRat
Rational
bisim
ArrayHeapListHeapBisim
LinkedListArrayListBisimulation
LinkedListMapArrayListBisimulation
bisim_deleteMin
Heap_List_BisimulationSpec
bisim_findMin
Heap_List_BisimulationSpec
bisim_insert
Heap_List_BisimulationSpec
bisim_merge
Heap_List_BisimulationSpec
bisim_size
Heap_List_BisimulationSpec
bisimulate
List
boolean2ProofOps
proof
build
LeftistHeap
by
proof