From 13bb1e954d5bd3cb9a560d9318a8df751e393ccf Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Fri, 26 Jul 2024 23:15:27 +0200 Subject: Partial implementation of heapRemoveLastWithIndexOnlyRemovesOneElement --- TODO | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'TODO') diff --git a/TODO b/TODO index 382afc6..5f8f446 100644 --- a/TODO +++ b/TODO @@ -5,7 +5,7 @@ This is a rough outline of upcoming tasks: [ ] Prove that CompleteTree.heapUpdateAt returns the element at the given index [ ] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same tree [ ] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same element -[ ] Prove that CompleteTree.heapRemoveLastWithIndex indeed removes the last element +[ ] Prove that CompleteTree.heapRemoveLastWithIndex only removes one element and leaves the rest unchanged - This automatically serves as a proof for CompleteTree.heapRemoveLast, once it is shown that they yield the same tree - A potential approach is to show that any index in the resulting tree can be converted into an index -- cgit v1.2.3