A skip list container class in Python

#================================================================
# Verification functions
#----------------------------------------------------------------
# children-are-ordered ( x, y ) ==
#   if self.allowDups ->
#       cmp ( key-of ( x ), key-of ( y ) ) <= 0
#   else ->
#       cmp ( key-of ( x ), key-of ( y ) ) < 0
#--
# Similar to the keys-are-ordered predicate, but operates on
# child objects.

#----------------------------------------------------------------
# insertion-cut-list ( key ) ==
#   a list L of size self.__maxLevels, such that each element
#   L[i] equals insertion-point ( i, key )
#--
#   An ``insertion cut list'' is a list of the _SkipItem objects
#   that must be updated when a new elements is inserted.  Element
#   [i] of the cut list points to the element whose forward
#   pointer has to be repaired in the (i)th list.

#----------------------------------------------------------------
# insertion-point ( level, key ) ==
#   the last element E in nth-list ( self.__heads, level ) such
#   that insertion-precedes ( E, key ) is true
#--
#   This describes the predecessor _SkipItem whose forward link
#   must be updated when a new item with key (key) is inserted.

#----------------------------------------------------------------
# insertion-point-after ( level, key, searchItem ) ==
#   the last element E in nth-list(searchItem,level) such that
#   insertion-precedes(E, key) is true
#--
#   Just like insertion-point(), except that it starts at an
#   arbitrary _SkipItem instead of self.__heads.

#----------------------------------------------------------------
# insertion-precedes ( skipItem, key ) ==
#   if skipItem is self.__terminator -> F
#   else if skipItem is self.__heads -> T
#   else ->
#     keys-are-ordered ( key-of ( skipItem's child ), key )
#--
#   This predicate is true when (skipItem) should be before
#   an item with key (key) in the level-0 list.

#----------------------------------------------------------------
# key-of ( child ) ==
#   if  not self.keyFunction ->
#       child
#   else ->
#       self.keyFunction ( child )

#----------------------------------------------------------------
# keys-are-ordered ( x, y ) ==
#   if self.allowDups ->
#       cmp ( x, y ) <= 0
#   else ->
#       cmp ( x, y ) < 0
#--
#   This is the ordering relation used in the key domain.
#   -   If we don't allow duplicates, then each key must be
#       strictly less than its successor.
#   -   If we allow duplicates, then two successive keys can
#       be equal.

#----------------------------------------------------------------
# nth-list ( root, n ) ==
#   the linked list of _SkipItem objects rooted at (root) and
#   using _SkipItem.links[n] as the next-item method
#--
#   This define is used to describe positions in the linked list
#   of objects at one level of the structure.  In particular,
#       nth-list ( self.__heads, n )
#   describes the entire skip list at level (n).

#----------------------------------------------------------------
# search-cut-list ( key ) ==
#   a list L of size self.__maxLevels such that
#   L[i] := search-point ( i, key )
#--
#   Like insert-cut-list(), but used for .delete() and .find()
#   operations.

#----------------------------------------------------------------
# search-point ( level, key ) ==
#   the last _SkipItem E in nth-list(self.__heads, level) such that
#   search-precedes(E, key) is true
#--
#   The predecessor whose forward link must be updated when
#   the item with key (key) is deleted.  Also used in
#   .find().

#----------------------------------------------------------------
# search-point-after ( level, key, searchItem ) ==
#   the last element E in nth-list(searchItem, level) such that
#   search-precedes(E, key) is true
#--
#   Like search-point except that the search starts at some
#   given item rather than at self.__heads.

#----------------------------------------------------------------
# search-precedes ( skipItem, key ) ==
#   if skip-compare ( skipitem, key ) < 0  ->  true
#   else -> false
#--
#   A predicate, true when the child in skipItem is before the
#   key (key).

#----------------------------------------------------------------
# skip-compare ( skipItem, key ) ==
#   if skipItem is self.__terminator -> 1
#   else -> cmp ( key-of ( skipItem's child ), key )
#--
#   Like cmp(), but we want to avoid trying to extract a key
#   from self.__terminator, because it doesn't have one.  If
#   skipItem is the terminator, we return 1 because the terminator
#   goes after all other elements.
#----------------------------------------------------------------