From 4f9585b8617ecb65fb97408b831ff45ef25ad0c3 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Tue, 13 Aug 2024 00:11:11 +0200 Subject: heapPopOnlyRemovesRoot is finally done --- TODO | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'TODO') diff --git a/TODO b/TODO index b5e7d4f..b4916df 100644 --- a/TODO +++ b/TODO @@ -8,12 +8,11 @@ This is a rough outline of upcoming tasks: [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. + - Done by showing how indices relate between both trees. [ ] 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. +[x] Prove that heapPop leaves all values in the tree, except the root. [x] 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. -- cgit v1.2.3