Title: Treaps
Authors: Max Haslbeck, Manuel Eberl and Tobias Nipkow
Submission date: 2018-02-06

A Treap is a binary tree whose nodes contain pairs consisting of some payload and an associated priority. It must have the search-tree property w.r.t. the payloads and the heap property w.r.t. the priorities. Treaps are an interesting data structure that is related to binary search trees (BSTs) in the following way: if one forgets all the priorities of a treap, the resulting BST is exactly the same as if one had inserted the elements into an empty BST in order of ascending priority. This means that a treap behaves like a BST where we can pretend the elements were inserted in a different order from the one in which they were actually inserted.

In particular, by choosing these priorities at random upon insertion of an element, we can pretend that we inserted the elements in random order, so that the shape of the resulting tree is that of a random BST no matter in what order we insert the elements. This is the main result of this formalisation.

  author  = {Max Haslbeck and Manuel Eberl and Tobias Nipkow},
  title   = {Treaps},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2018,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Comparison_Sort_Lower_Bound, Random_BSTs