# Weight-Balanced Trees

 Title: Weight-Balanced Trees Authors: Tobias Nipkow and Stefan Dirix Submission date: 2018-03-13 Abstract: This theory provides a verified implementation of weight-balanced trees following the work of Hirai and Yamamoto who proved that all parameters in a certain range are valid, i.e. guarantee that insertion and deletion preserve weight-balance. Instead of a general theorem we provide parameterized proofs of preservation of the invariant that work for many (all?) valid parameters. BibTeX: @article{Weight_Balanced_Trees-AFP, author = {Tobias Nipkow and Stefan Dirix}, title = {Weight-Balanced Trees}, journal = {Archive of Formal Proofs}, month = mar, year = 2018, note = {\url{https://isa-afp.org/entries/Weight_Balanced_Trees.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.