Work Bounds for Strongly Joinable Balanced Binary Search Trees

Marco Haucke 📧

September 24, 2026

Abstract

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 $m$ and $n$ where $m \le n$.

License

BSD License

Note

Claude Fable 5.1 (Anthropic) was used to derive the instantiation of the framework for red-black trees (theory StronglyJoinableRBT) and part of the appendix (theory Submodularity), as well as pointwise resolving of SMT steps/apply scripts.

Topics

Related publications

  • Blelloch, G., Ferizovic, D., & Sun, Y. (2022). Joinable Parallel Balanced Binary Trees. ACM Transactions on Parallel Computing, 9(2), 1–41. https://doi.org/10.1145/3512769

Session Joinable_BST_Work_Bounds

Cite

× 
@article{Joinable_BST_Work_Bounds-AFP,
  author  = {Marco Haucke},
  title   = {Work Bounds for Strongly Joinable Balanced Binary Search Trees},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Joinable_BST_Work_Bounds.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download