Abstract: 
A Treap is a binary tree whose nodes contain pairs
consisting of some payload and an associated priority. It must have
the searchtree 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. 
BibTeX: 
@article{TreapsAFP,
author = {Maximilian Haslbeck and Manuel Eberl and Tobias Nipkow},
title = {Treaps},
journal = {Archive of Formal Proofs},
month = feb,
year = 2018,
note = {\url{http://isaafp.org/entries/Treaps.html},
Formal proof development},
ISSN = {2150914x},
}
