From e47e4b79142bcee5bcdc4647dc71c7ce3954cf0b Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 25 Aug 2024 22:48:10 +0200 Subject: indexOfNoneImpPredFalse --- TODO | 1 + 1 file changed, 1 insertion(+) (limited to 'TODO') diff --git a/TODO b/TODO index 45b469d..5ad9eb6 100644 --- a/TODO +++ b/TODO @@ -9,6 +9,7 @@ This is a rough outline of upcoming tasks: [x] This automatically serves as a proof for CompleteTree.heapRemoveLast, once it is shown that they yield the same tree - Done by showing how indices relate between both trees. +[x] Prove that if CompleteTree.indexOf returns none, no index exists for which the predicate is true. [ ] 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. -- cgit v1.2.3