I would not scoff at AVL trees. They are easy to prove correctness for, and admit a short implementation at ~100 lines. They're as short as AA trees, but AA tre

I would not scoff at AVL trees. They are easy to prove correctness for, and admit a short implementation at ~100 lines. They're as short as AA trees, but AA trees are harder to prove with more cases. https://www.nayuki.io/res/aa-tree-set/BasicAvlTreeSet.java https://www.nayuki.io/res/aa-tree-set/BasicAvlTreeSet.java , https://www.nayuki.io/page/aa-tree-set https://www.nayuki.io/page/aa-tree-set B-trees require a much longer implementation than AVL trees. https://www.nayuki.io/page/btree-set https://www.nayuki.io/page/btree-set