diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-08 19:11:28 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-08 19:11:28 +0200 |
| commit | 9c8021d0cd90fe6f0ed9a9c15679b80b099f4229 (patch) | |
| tree | 4b3c0e285d57d937111c04292e59e5bd5f9a9e71 | |
| parent | eeb3cbd36d5e8ff3e4e2b4a242f7dd9af521fdfe (diff) | |
Minor
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index a505c91..99ce68a 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -816,10 +816,16 @@ case isFalse h₃ => subst he6 simp at he5 subst rr2 + subst oldValue + have : pp2+1+1 < o + (pp2 + 1 + 1) := by omega + have : ⟨j2 + 1 - o, by omega⟩ > (CompleteTree.Internal.heapRemoveLastWithIndex r).snd.snd := sorry + --have htest := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt r ⟨j2 + 1 - o, by omega⟩ this + --simp at htest sorry case isTrue h₃ => --removed left sorry +--termination_by n protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)): let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap |