TODO


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

This is a rough outline of upcoming tasks:

[ ] Prove that an index exists such that after CompleteTree.heapPush the pushed element can be obtained by
    CompleteTree.get
[ ] Prove that CompleteTree.heapPush leaves all elements that were already in the heap in the heap.
[x] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same tree
[x] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same element
[x] Prove that CompleteTree.heapRemoveLastWithIndex only removes one element and leaves the rest unchanged
    [x] This automatically serves as a proof for CompleteTree.heapRemoveLast, once it is shown that they
      yield the same tree
    - Done by showing that each element of the input tree is in the output tree, except for the one at the
      returned index.
[ ] Prove that if CompleteTree.indexOf returns some, CompleteTree.get with that result fulfills the predicate.
[x] Prove that CompleteTree.heapUpdateRoot indeed exchanges the value at the root.
    - Done by showing that the new tree contains all elements except the root, and the updated value.
[ ] Prove that heapPop leaves all values in the tree, except the root.
[ ] Prove that heapPop returns the root
[ ] Prove that CompleteTree.heapUpdateAt returns the element at the given index
[ ] Prove that CompleteTree.heapUpdateAt indeed updates the value at the given index.
    - Use the same approach as heapUpdateRoot
[ ] Prove that CompleteTree.heapRemoveAt returns the element at the given index
[ ] Prove that CompleteTree.heapRemoveAt leaves all values in the tree except at the input index.


[ ] Write the performance part of this file.