Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Work Bounds for Strongly Joina...

Email Gateway (Sep 24 2026 at 13:57):

From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: Work Bounds for Strongly Joinable Balanced Binary Search Trees

Work Bounds for Strongly Joinable Balanced Binary Search Trees
Marco Haucke

This entry formalises the complexity analysis of set operations on strongly
joinable trees as defined by Blelloch, Ferizovic and Sun. It is proved that
union, intersection, and difference run in time O(m * log (n/m + 1)) for input
sets of size n and m where m <= n.

https://isa-afp.org/entries/Joinable_BST_Work_Bounds.html

Enjoy!

smime.p7s

Last updated: Oct 08 2026 at 21:07 UTC