Binary search tree

DefinitionMembership in a binary tree#✓fully proved

A key \(x\) belongs to a binary tree \(T\) when it is the key of some node of \(T\): no key belongs to the empty tree, and \(x\) belongs to a node with key \(k\), left subtree \(L\) and right subtree \(R\) exactly when \(x\) belongs to \(L\), \(x = k\), or \(x\) belongs to \(R\).

This membership does not use the search-tree ordering.

public def Mem {α : Type u} (x : α) : BinaryTree α → Prop
  | .nil => False
  | .node key left right => Mem x left ∨ x = key ∨ Mem x right

Used by 61

Used byMembership in an AVL tree · Keys of an ordered AVL tree after deletion · AVL deletion keeps every other key · Membership after insertion into an AVL tree · AVL membership is membership in the underlying binary tree · The leftmost key lies in the tree · Deletion removes the deleted key from an ordered AVL tree · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · A predicate holds at all keys of a binary tree iff it holds at all its members · Search in a binary search tree is correct · Inorder traversal after deletion · Membership after deletion · Deletion keeps the other keys · Members of the binary search tree built from a list · Membership in the inorder traversal of a binary tree · Membership after insertion into a binary search tree · Membership in a join · The deleted key is gone · Inserting a present key into a binary search tree leaves its size unchanged · Inserting an absent key into a binary search tree adds one node · Deletion preserves the search-tree order · The inorder traversal of an ordered binary tree is strictly increasing · Joining separated ordered trees · Selecting the rank of a key returns the key · A predicate holds on every key iff it holds along the inorder traversal · Keys of a Cartesian tree · The root of a binary tree is one of its keys · The root of a Cartesian tree is a minimum of the list · The root of a heap-ordered tree is below every key · Search misses a key deleted from an order-statistic tree · Search in an ordered order-statistic tree is correct · Inorder traversal after order-statistic deletion · Keys of an order-statistic tree after deletion · Keys of an order-statistic tree built from a list · Keys of an order-statistic merge · Deleted key is absent from an order-statistic tree · Deletion preserves order in an order-statistic tree · Merging separated ordered order-statistic trees preserves order · Cached rank agrees with traversal rank · Select inverts rank in an order-statistic tree · Selecting the rank of a surviving key after deletion · Inorder traversal after deletion by rebuilding · Membership in a red-black tree · Membership after deletion by rebuilding · Red-black membership is membership in the underlying binary tree · Joining separated ordered trees preserves order · Splitting an ordered tree separates the keys around the split key · Correctness of the splay-tree membership test · Keys after splay-tree insertion · Splay-tree split parts contain only original keys · Splaying preserves membership · Keys other than the split key survive a split · Splaying preserves the search-tree property · Both parts of a split search tree are search trees · Splaying a present key brings it to the root · Root key after splaying a present key · Membership after weight-balanced rebalancing · Membership in a weight-balanced tree built from a list · Membership after weight-balanced insertion · Weight-balanced insertion preserves the search-tree order

DefinitionInorder traversal of a binary tree with an accumulator#✓fully proved

For a binary tree \(t\) and a list \(s\), the accumulated traversal of the empty tree onto \(s\) is \(s\), and the accumulated traversal of a node with key \(k\), left subtree \(L\) and right subtree \(R\) onto \(s\) is the accumulated traversal of \(L\) onto the list consisting of \(k\) followed by the accumulated traversal of \(R\) onto \(s\).

Unfolding the recursion, the result is the inorder traversal of \(t\) followed by \(s\).

public def inorderAux {α : Type u} : BinaryTree α → List α → List α
  | .nil, suffix => suffix
  | .node key left right, suffix =>
      inorderAux left (key :: inorderAux right suffix)

Used by 32

Used byInorder traversal of an AVL tree onto a suffix · AVL rebalancing preserves the inorder traversal · The inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · Inorder traversal of a binary tree · Inorder traversal after deletion · Inorder traversal of a join · Membership in the inorder traversal of a binary tree · The length of the inorder traversal of a binary tree is its number of nodes · The inorder traversal of an ordered binary tree is strictly increasing · Cartesian trees are heap-ordered · Inorder traversal of a Cartesian tree · Inorder traversal after order-statistic deletion · Inorder traversal of an order-statistic merge · Keys of an order-statistic tree after deletion · Keys of an order-statistic merge · Deletion preserves order in an order-statistic tree · Merging separated ordered order-statistic trees preserves order · Cached rank agrees with traversal rank · Cached select agrees with inorder select · Black height after double-black deletion · Inorder traversal onto a suffix · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Inorder traversal of a splice · Membership after insertion into a red-black tree · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order · Double-black deletion yields a valid tree from the structural invariants · Splaying preserves the inorder traversal · Splaying preserves the search-tree property · The optimal BST procedure finds the minimum expected search cost

DefinitionInorder traversal of a binary tree#✓fully proved

The inorder traversal of a binary tree \(t\) is the accumulated inorder traversal of \(t\) onto the empty list. Equivalently, the empty tree gives the empty list, and a node with key \(k\), left subtree \(L\) and right subtree \(R\) gives the inorder traversal of \(L\), then \(k\), then the inorder traversal of \(R\).

public def inorder {α : Type u} (tree : BinaryTree α) : List α :=
  inorderAux tree []

Uses 1 · Used by 47

Statement usesInorder traversal of a binary tree with an accumulator

Used byInorder traversal of an AVL tree · AVL rebalancing preserves the inorder traversal · The inorder traversal begins with the leftmost key · Inorder traversal after AVL deletion · AVL inorder traversal agrees with the erased binary search tree · Inorder traversal after deletion · Inorder traversal of a join · The inorder traversal of a binary search tree has no duplicates · Membership in the inorder traversal of a binary tree · The length of the inorder traversal of a binary tree is its number of nodes · The inorder traversal of an ordered binary tree is strictly increasing · Rank of a key in a binary tree · Rank counts the smaller inorder entries · The rank of a selected key is its index · Inorder selection in a binary tree · Selection is indexing into the inorder traversal · Selecting the rank of a key returns the key · A predicate holds on every key iff it holds along the inorder traversal · Cartesian trees are heap-ordered · Inorder traversal of a Cartesian tree · Keys of a Cartesian tree · The keys of a Cartesian tree permute its input · Inorder traversal of an order-statistic tree · Inorder traversal after order-statistic deletion · Inorder traversal of an order-statistic merge · Keys of an order-statistic tree after deletion · Keys of an order-statistic merge · Deletion preserves order in an order-statistic tree · Merging separated ordered order-statistic trees preserves order · Cached rank agrees with traversal rank · Cached select agrees with inorder select · Black height after double-black deletion · Inorder traversal of a red-black tree · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Inorder traversal ignores colors · Inorder traversal of a splice · Membership after insertion into a red-black tree · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order · Double-black deletion yields a valid tree from the structural invariants · Splaying preserves the inorder traversal · Splaying preserves membership · Splaying preserves the number of nodes · Splaying preserves the search-tree property · Expected search cost of a binary search tree · The optimal BST procedure finds the minimum expected search cost

DefinitionA predicate holding at every key of a binary tree#✓fully proved

For a predicate \(p\) on a type \(\alpha\), the empty binary tree satisfies "every key satisfies \(p\)", and a node with key \(k\), left subtree \(L\) and right subtree \(R\) satisfies it exactly when \(L\) satisfies it, \(p(k)\) holds and \(R\) satisfies it.

public def All {α : Type u} (p : α → Prop) : BinaryTree α → Prop
  | .nil => True
  | .node key left right => All p left ∧ p key ∧ All p right

Used by 45

Used byEvery key of an AVL tree satisfies a predicate · Keys left after removing the minimum exceed it · The all-keys predicate is unchanged by erasing height caches · Inorder traversal after AVL deletion · Deletion removes the deleted key from an ordered AVL tree · Rebalancing an AVL node preserves the search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · AVL insertion preserves the search-tree order · A predicate holds at all keys of a binary tree iff it holds at all its members · Search in a binary search tree is correct · Inorder traversal after deletion · The deleted key is gone · Inserting a present key into a binary search tree leaves its size unchanged · Ordered binary trees · Deletion preserves the search-tree order · The inorder traversal of an ordered binary tree is strictly increasing · Binary search tree insertion preserves order · Joining separated ordered trees · A predicate holds on every key iff it holds along the inorder traversal · Min-heap ordered binary tree · Cartesian trees are heap-ordered · The root of a heap-ordered tree is below every key · Inorder traversal after order-statistic deletion · Keys of an order-statistic tree after deletion · Deletion preserves order in an order-statistic tree · Merging separated ordered order-statistic trees preserves order · Cached rank agrees with traversal rank · Predicate holding at every key of a red-black tree · All keys of a red-black tree via its color erasure · Black height after double-black deletion · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Membership after deletion by rebuilding · Double-black deletion preserves the search-tree order · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Double-black deletion yields a valid tree from the structural invariants · Splitting an ordered tree separates the keys around the split key · Splay-tree insertion preserves the search-tree property · Splaying preserves the search-tree property · Both parts of a split search tree are search trees · Splaying a present key brings it to the root · Weight-balanced rebalancing preserves ordering · Weight-balanced insertion preserves the search-tree order

DefinitionOrdered binary trees#✓fully proved

Let \(\alpha\) be a type with a relation \(<\). The empty tree is ordered, and a binary tree with root key \(k\), left subtree \(L\) and right subtree \(R\) is ordered when \(L\) and \(R\) are ordered, every key of \(L\) is less than \(k\), and \(k\) is less than every key of \(R\).

public def Ordered {α : Type u} [LT α] : BinaryTree α → Prop
  | .nil => True
  | .node key left right =>
      Ordered left ∧ Ordered right ∧ All (· < key) left ∧ All (key < ·) right

Uses 1 · Used by 49

Statement usesA predicate holding at every key of a binary tree

Used byKeys left after removing the minimum exceed it · Inorder traversal after AVL deletion · Deletion removes the deleted key from an ordered AVL tree · Ordered AVL trees · Rebalancing an AVL node preserves the search-tree order · AVL deletion preserves search-tree order · Removing the leftmost key preserves search-tree order · AVL insertion preserves the search-tree order · Order of an AVL tree via its underlying binary tree · Search in a binary search tree is correct · Inorder traversal after deletion · The inorder traversal of a binary search tree has no duplicates · Membership after deletion · The deleted key is gone · Inserting a present key into a binary search tree leaves its size unchanged · Deletion preserves the search-tree order · Binary search trees built from a list are ordered · The inorder traversal of an ordered binary tree is strictly increasing · Binary search tree insertion preserves order · Joining separated ordered trees · The rank of a selected key is its index · Selecting the rank of a key returns the key · Inorder traversal after order-statistic deletion · Keys of an order-statistic tree after deletion · Ordered order-statistic tree · Deletion preserves order in an order-statistic tree · Insertion preserves ordering of order-statistic trees · Merging separated ordered order-statistic trees preserves order · Cached rank agrees with traversal rank · Black height after double-black deletion · Inorder traversal after deletion by rebuilding · Double-black deletion erases the key from the inorder traversal · Membership after deletion by rebuilding · Ordered red-black tree · Double-black deletion preserves the search-tree order · A red-black tree is ordered exactly when its underlying binary tree is · Red-black insertion preserves the search-tree order · Joining separated ordered trees preserves order · Double-black deletion yields a valid tree from the structural invariants · Splitting an ordered tree separates the keys around the split key · Correctness of the splay-tree membership test · Splay-tree insertion preserves the search-tree property · Splaying preserves the search-tree property · Both parts of a split search tree are search trees · Splaying a present key brings it to the root · Root key after splaying a present key · Weight-balanced rebalancing preserves ordering · Weight-balanced trees built from a list are ordered · Weight-balanced insertion preserves the search-tree order

DefinitionSearch in a binary search tree#✓fully proved

For a linearly ordered type \(\alpha\), a key \(x \in \alpha\) and a binary tree \(t\) with keys in \(\alpha\), the search for \(x\) in \(t\) returns a Boolean: false if \(t\) is empty, and if \(t\) is a node with key \(k\), left subtree \(L\) and right subtree \(R\), the search for \(x\) in \(L\) when \(x < k\), the search for \(x\) in \(R\) when \(k < x\), and true otherwise.

Unlike the index of a key in a binary tree, which encodes the root-to-node path as a positive binary number, this search returns only whether the key was found.

public def contains {α : Type u} [LinearOrder α] (x : α) : BinaryTree α → Bool
  | .nil => false
  | .node key left right =>
      if x < key then contains x left
      else if key < x then contains x right
      else true

Used by 4

Used byCorrectness of AVL search · Search in a binary search tree is correct · Search in an ordered order-statistic tree is correct · Search in an ordered red-black tree is correct

DefinitionInsertion into a binary search tree#✓fully proved

For a linearly ordered type \(\alpha\), a key \(x \in \alpha\) and a binary tree \(t\) with keys in \(\alpha\), inserting \(x\) into the empty tree gives the single node with key \(x\) and empty subtrees; inserting \(x\) into a node with key \(k\), left subtree \(L\) and right subtree \(R\) inserts \(x\) into \(L\) when \(x < k\), inserts \(x\) into \(R\) when \(k < x\), and returns the node unchanged when \(x = k\).

public def insert {α : Type u} [LinearOrder α] (x : α) : BinaryTree α → BinaryTree α
  | .nil => .node x .nil .nil
  | tree@(.node key left right) =>
      if x < key then .node key (insert x left) right
      else if key < x then .node key left (insert x right)
      else tree

Used by 9

Used byBinary search tree built from a list · Members of the binary search tree built from a list · Membership after insertion into a binary search tree · Inserting a present key into a binary search tree leaves its size unchanged · Inserting an absent key into a binary search tree adds one node · Binary search tree insertion preserves order · Insertion commutes with forgetting the size caches · Keys of an order-statistic tree built from a list · Insertion preserves ordering of order-statistic trees

DefinitionRank of a key in a binary tree#✓fully proved

For a linearly ordered type \(\alpha\), a key \(x \in \alpha\) and a binary tree \(t\) with keys in \(\alpha\), the rank of \(x\) in \(t\) is the number of positions of the inorder traversal of \(t\) whose entry is strictly less than \(x\).

public def rank {α : Type u} [LinearOrder α] (x : α) (tree : BinaryTree α) : Nat :=
  ((inorder tree).filter (· < x)).length

Uses 1 · Used by 7

Statement usesInorder traversal of a binary tree

Used byRank counts the smaller inorder entries · The rank of a selected key is its index · Selecting the rank of a key returns the key · Rank after deletion in an order-statistic tree · Cached rank agrees with traversal rank · Rank inverts select in an order-statistic tree · Select inverts rank in an order-statistic tree

DefinitionInorder selection in a binary tree#✓fully proved

For a binary tree \(t\) and a natural number \(i\), selecting index \(i\) in \(t\) returns the entry at zero-based position \(i\) of the inorder traversal of \(t\) when \(i\) is less than the length of that traversal, and returns nothing otherwise.

public def select {α : Type u} (tree : BinaryTree α) (index : Nat) : Option α :=
  (inorder tree)[index]?

Uses 1 · Used by 7

Statement usesInorder traversal of a binary tree

Used byThe rank of a selected key is its index · Selection is indexing into the inorder traversal · Selecting the rank of a key returns the key · Rank inverts select in an order-statistic tree · Selection after deletion in an order-statistic tree · Cached select agrees with inorder select · Select inverts rank in an order-statistic tree

DefinitionBinary search tree built from a list#✓fully proved

For a linearly ordered type \(\alpha\), the binary tree built from a list \([x_1, \ldots, x_n]\) of elements of \(\alpha\) is obtained from the empty tree by inserting \(x_n\), then \(x_{n-1}\), and so on down to \(x_1\), using binary search tree insertion; the empty list gives the empty tree.

public def fromList {α : Type u} [LinearOrder α] : List α → BinaryTree α
  | [] => .nil
  | x :: xs => insert x (fromList xs)

Uses 1 · Used by 3

Statement usesInsertion into a binary search tree

Used byMembers of the binary search tree built from a list · Binary search trees built from a list are ordered · Keys of an order-statistic tree built from a list

TheoremA predicate holds at all keys of a binary tree iff it holds at all its members#✓fully proved

For a type \(\alpha\), a predicate \(p\) on \(\alpha\) and a binary tree \(t\) with keys in \(\alpha\), every key of \(t\) satisfies \(p\) in the recursive sense (the empty tree qualifies, and a node qualifies when its left subtree qualifies, its key satisfies \(p\) and its right subtree qualifies) if and only if \(p(x)\) holds for every \(x\) that is a member of \(t\).

public theorem all_iff_forall_mem {α : Type u} {p : α → Prop}
    {tree : BinaryTree α} :
    All p tree ↔ ∀ x, x ∈ tree → p x

Uses 2 · Used by 21

Statement usesA predicate holding at every key of a binary tree · Membership in a binary tree

Used byThe all-keys predicate in terms of membership (AVL trees) · Search in a binary search tree is correct · Inorder traversal after deletion · The deleted key is gone · Inserting a present key into a binary search tree leaves its size unchanged · Deletion preserves the search-tree order · The inorder traversal of an ordered binary tree is strictly increasing · Joining separated ordered trees · A predicate holds on every key iff it holds along the inorder traversal · The root of a heap-ordered tree is below every key · Inorder traversal after order-statistic deletion · Keys of an order-statistic tree after deletion · Deletion preserves order in an order-statistic tree · Merging separated ordered order-statistic trees preserves order · Cached rank agrees with traversal rank · All keys versus members of a red-black tree · Splitting an ordered tree separates the keys around the split key · Splaying preserves the search-tree property · Both parts of a split search tree are search trees · Splaying a present key brings it to the root · Weight-balanced insertion preserves the search-tree order

TheoremMembership in the inorder traversal of a binary tree#✓fully proved

For every binary tree \(T\) and every key \(x\), \(x\) occurs in the inorder traversal of \(T\) if and only if \(x\) lies in \(T\).

public theorem mem_inorder {α : Type u} {x : α} {tree : BinaryTree α} :
    x ∈ inorder tree ↔ x ∈ tree

Uses 3 · Used by 15

Statement usesMembership in a binary tree · Inorder traversal of a binary tree

Proof usesInorder traversal of a binary tree with an accumulator

Used byMembership in the inorder traversal of an AVL tree · Inorder traversal after deletion · The inorder traversal of an ordered binary tree is strictly increasing · Selecting the rank of a key returns the key · A predicate holds on every key iff it holds along the inorder traversal · Keys of a Cartesian tree · Inorder traversal after order-statistic deletion · Keys of an order-statistic tree after deletion · Keys of an order-statistic merge · Deletion preserves order in an order-statistic tree · Merging separated ordered order-statistic trees preserves order · Cached rank agrees with traversal rank · Membership in the inorder traversal of a red-black tree · Splaying preserves membership · Splaying preserves the search-tree property

TheoremMembership after insertion into a binary search tree#✓fully proved

Let the keys be linearly ordered. For all keys \(x, y\) and every binary tree \(T\), \(y\) lies in the tree obtained by inserting \(x\) into \(T\) if and only if \(y = x\) or \(y\) lies in \(T\).

public theorem mem_insert {α : Type u} [LinearOrder α] {x y : α}
    {tree : BinaryTree α} :
    y ∈ insert x tree ↔ y = x ∨ y ∈ tree

Uses 2 · Used by 1

Statement usesMembership in a binary tree · Insertion into a binary search tree

Used byMembers of the binary search tree built from a list

TheoremBinary search tree insertion preserves order#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every key \(x \in \alpha\) and every ordered binary tree \(T\) over \(\alpha\), the tree obtained by inserting \(x\) into \(T\) is ordered.

public theorem ordered_insert {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} (hTree : Ordered tree) : Ordered (insert x tree)

Uses 3 · Used by 2

Statement usesOrdered binary trees · Insertion into a binary search tree

Proof usesA predicate holding at every key of a binary tree

Used byBinary search trees built from a list are ordered · Insertion preserves ordering of order-statistic trees

TheoremSearch in a binary search tree is correct#✓fully proved

For a linearly ordered type \(\alpha\), a key \(x \in \alpha\) and a binary tree \(t\) with keys in \(\alpha\) that is ordered (recursively, every key in the left subtree of a node is strictly smaller than the node's key and every key in its right subtree is strictly larger), the comparison search for \(x\) in \(t\) returns true if and only if \(x\) is a member of \(t\).

public theorem contains_eq_true_iff {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} (hTree : Ordered tree) :
    contains x tree = true ↔ x ∈ tree

Uses 5 · Used by 3

Statement usesMembership in a binary tree · Ordered binary trees · Search in a binary search tree

Proof usesA predicate holding at every key of a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members

Used byCorrectness of AVL search · Search in an ordered order-statistic tree is correct · Search in an ordered red-black tree is correct

TheoremThe inorder traversal of an ordered binary tree is strictly increasing#✓fully proved

Let \(\alpha\) be a linearly ordered type. If a binary tree \(T\) over \(\alpha\) is ordered, then in the inorder traversal of \(T\) every key is less than every key that comes after it.

public theorem ordered_inorder {α : Type u} [LinearOrder α]
    {tree : BinaryTree α} (hTree : Ordered tree) :
    List.Pairwise (· < ·) (inorder tree)

Uses 7 · Used by 6

Statement usesOrdered binary trees · Inorder traversal of a binary tree

Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · Inorder traversal of a binary tree with an accumulator · Membership in the inorder traversal of a binary tree

Used byThe inorder traversal of an ordered AVL tree is strictly increasing · The inorder traversal of a binary search tree has no duplicates · The rank of a selected key is its index · Selecting the rank of a key returns the key · The inorder traversal of an ordered red-black tree is strictly increasing · Splaying preserves the search-tree property

TheoremThe inorder traversal of a binary search tree has no duplicates#✓fully proved

For a linearly ordered type \(\alpha\) and a binary tree \(t\) with keys in \(\alpha\) that is ordered (recursively, every key in the left subtree of a node is strictly smaller than the node's key and every key in its right subtree is strictly larger), the inorder traversal of \(t\) is a list with no repeated entries.

public theorem inorder_nodup {α : Type u} [LinearOrder α]
    {tree : BinaryTree α} (hTree : Ordered tree) : (inorder tree).Nodup

Uses 3 · Used by 1

Statement usesOrdered binary trees · Inorder traversal of a binary tree

Proof usesThe inorder traversal of an ordered binary tree is strictly increasing

Used byThe inorder traversal of an ordered AVL tree has no duplicates

TheoremBinary search trees built from a list are ordered#✓fully proved

Let \(\alpha\) be a linearly ordered type. For every list \(xs\) of elements of \(\alpha\), the tree obtained from the empty tree by inserting the elements of \(xs\) one at a time, from the last element to the first, is ordered.

public theorem ordered_fromList {α : Type u} [LinearOrder α] {xs : List α} :
    Ordered (fromList xs)

Uses 3

Statement usesOrdered binary trees · Binary search tree built from a list

Proof usesBinary search tree insertion preserves order

TheoremMembers of the binary search tree built from a list#✓fully proved

For a linearly ordered type \(\alpha\), a key \(x \in \alpha\) and a list \(xs\) of elements of \(\alpha\), \(x\) is a member of the binary tree built from \(xs\) by successive binary search tree insertion if and only if \(x\) occurs in \(xs\).

public theorem mem_fromList {α : Type u} [LinearOrder α] {x : α} {xs : List α} :
    x ∈ fromList xs ↔ x ∈ xs

Uses 4 · Used by 1

Statement usesMembership in a binary tree · Binary search tree built from a list

Proof usesInsertion into a binary search tree · Membership after insertion into a binary search tree

Used byKeys of an order-statistic tree built from a list

TheoremThe length of the inorder traversal of a binary tree is its number of nodes#✓fully proved

For every binary tree \(T\), the number of nodes of \(T\) (each node carries one key, and the empty tree has none) equals the length of the inorder traversal of \(T\).

public theorem numNodes_eq_length_inorder {α : Type u} {tree : BinaryTree α} :
    tree.numNodes = (inorder tree).length

Uses 2 · Used by 5

Statement usesInorder traversal of a binary tree

Proof usesInorder traversal of a binary tree with an accumulator

Used byCached rank agrees with traversal rank · Cached select agrees with inorder select · Splaying preserves the number of nodes · Expected search cost of a binary search tree · The optimal BST procedure finds the minimum expected search cost

TheoremInserting a present key into a binary search tree leaves its size unchanged#✓fully proved

Let the keys be linearly ordered, and let \(T\) be an ordered binary tree. If a key \(x\) lies in \(T\), then the tree obtained by inserting \(x\) into \(T\) has the same number of nodes as \(T\).

public theorem numNodes_insert_of_mem {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} (hTree : Ordered tree) (hx : x ∈ tree) :
    (insert x tree).numNodes = tree.numNodes

Uses 5

Statement usesMembership in a binary tree · Ordered binary trees · Insertion into a binary search tree

Proof usesA predicate holding at every key of a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members

TheoremInserting an absent key into a binary search tree adds one node#✓fully proved

Let the keys be linearly ordered. For every binary tree \(T\) and every key \(x\) that does not lie in \(T\), the tree obtained by inserting \(x\) into \(T\) has one more node than \(T\).

public theorem numNodes_insert_of_not_mem {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} (hx : ¬x ∈ tree) :
    (insert x tree).numNodes = tree.numNodes + 1

Uses 2

Statement usesMembership in a binary tree · Insertion into a binary search tree

TheoremRank counts the smaller inorder entries#✓fully proved

For a linearly ordered type \(\alpha\), a key \(x \in \alpha\) and a binary tree \(t\) with keys in \(\alpha\), the rank of \(x\) in \(t\) equals the length of the list obtained from the inorder traversal of \(t\) by keeping exactly the entries strictly less than \(x\).

public theorem rank_eq_count_inorder {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} :
    rank x tree = ((inorder tree).filter (· < x)).length

Uses 2

Statement usesInorder traversal of a binary tree · Rank of a key in a binary tree

TheoremSelection is indexing into the inorder traversal#✓fully proved

For a binary tree \(t\) and a natural number \(i\), selecting index \(i\) in \(t\) gives the same result as looking up zero-based position \(i\) of the inorder traversal of \(t\): the entry at that position when \(i\) is less than the length of the traversal, and nothing otherwise.

public theorem select_eq_getElem?_inorder {α : Type u} {tree : BinaryTree α}
    {index : Nat} :
    select tree index = (inorder tree)[index]?

Uses 2

Statement usesInorder traversal of a binary tree · Inorder selection in a binary tree

TheoremSelecting the rank of a key returns the key#✓fully proved

Let \(\alpha\) be a linearly ordered type and let \(t\) be a binary search tree with keys in \(\alpha\), that is, at every node each key of the left subtree is strictly smaller and each key of the right subtree is strictly larger than the node's key. If \(x\) is a key of \(t\), then selecting, in \(t\), the index equal to the rank of \(x\) in \(t\) returns \(x\).

public theorem select_rank {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} (hTree : Ordered tree) (hx : x ∈ tree) :
    select tree (rank x tree) = some x

Uses 7 · Used by 1

Statement usesMembership in a binary tree · Ordered binary trees · Rank of a key in a binary tree · Inorder selection in a binary tree

Proof usesInorder traversal of a binary tree · Membership in the inorder traversal of a binary tree · The inorder traversal of an ordered binary tree is strictly increasing

Used bySelect inverts rank in an order-statistic tree

TheoremThe rank of a selected key is its index#✓fully proved

Let \(\alpha\) be a linearly ordered type and let \(t\) be a binary search tree with keys in \(\alpha\), that is, at every node each key of the left subtree is strictly smaller and each key of the right subtree is strictly larger than the node's key. If selecting index \(i\) in \(t\) returns a key \(x\), then the rank of \(x\) in \(t\) equals \(i\).

public theorem rank_select {α : Type u} [LinearOrder α] {tree : BinaryTree α}
    {index : Nat} {x : α} (hTree : Ordered tree)
    (hSelect : select tree index = some x) : rank x tree = index

Uses 5 · Used by 1

Statement usesOrdered binary trees · Rank of a key in a binary tree · Inorder selection in a binary tree

Proof usesInorder traversal of a binary tree · The inorder traversal of an ordered binary tree is strictly increasing

Used byRank inverts select in an order-statistic tree

DefinitionJoin of two binary trees#✓fully proved

The join of the empty tree and a tree \(R\) is \(R\). The join of a tree with root key \(k\), left subtree \(L_1\) and right subtree \(L_2\) and a tree \(R\) is the tree with root key \(k\), left subtree \(L_1\) and right subtree the join of \(L_2\) and \(R\). Thus, when the first tree is nonempty, \(R\) becomes the right subtree of its rightmost node.

In the inorder traversal of the join, every key of the first tree comes before every key of the second tree.

public def join {α : Type u} : BinaryTree α → BinaryTree α → BinaryTree α
  | .nil, right => right
  | .node key leftLeft leftRight, right =>
      .node key leftLeft (join leftRight right)

Used by 9

Used byDeletion from a binary search tree · Inorder traversal after deletion · Inorder traversal of a join · Membership after deletion · Deletion keeps the other keys · Membership in a join · The deleted key is gone · Deletion preserves the search-tree order · Joining separated ordered trees

DefinitionDeletion from a binary search tree#✓fully proved

Let \(x\) be a key of a linearly ordered type. Deleting \(x\) from the empty tree gives the empty tree. Deleting \(x\) from a tree with root key \(k\), left subtree \(L\) and right subtree \(R\) gives the tree with root key \(k\), left subtree \(L\) with \(x\) deleted and right subtree \(R\) if \(x < k\); the tree with root key \(k\), left subtree \(L\) and right subtree \(R\) with \(x\) deleted if \(k < x\); and the join of \(L\) and \(R\) otherwise, that is, if \(x = k\).

public def delete {α : Type u} [LinearOrder α] (x : α) :
    BinaryTree α → BinaryTree α
  | .nil => .nil
  | .node key left right =>
      if x < key then .node key (delete x left) right
      else if key < x then .node key left (delete x right)
      else join left right

Uses 1 · Used by 5

Statement usesJoin of two binary trees

Used byInorder traversal after deletion · Membership after deletion · Deletion keeps the other keys · The deleted key is gone · Deletion preserves the search-tree order

TheoremMembership in a join#✓fully proved

For binary trees \(L\) and \(R\), a key \(x\) occurs in the join of \(L\) and \(R\) if and only if \(x\) occurs in \(L\) or \(x\) occurs in \(R\).

public theorem mem_join {α : Type u} {x : α} {left right : BinaryTree α} :
    x ∈ join left right ↔ x ∈ left ∨ x ∈ right

Uses 2 · Used by 5

Statement usesMembership in a binary tree · Join of two binary trees

Used byMembership after deletion · Deletion keeps the other keys · The deleted key is gone · Deletion preserves the search-tree order · Joining separated ordered trees

TheoremInorder traversal of a join#✓fully proved

For binary trees \(L\) and \(R\), the inorder traversal of the join of \(L\) and \(R\) is the inorder traversal of \(L\) followed by the inorder traversal of \(R\).

public theorem inorder_join {α : Type u} {left right : BinaryTree α} :
    inorder (join left right) = inorder left ++ inorder right

Uses 3 · Used by 1

Statement usesInorder traversal of a binary tree · Join of two binary trees

Proof usesInorder traversal of a binary tree with an accumulator

Used byInorder traversal after deletion

TheoremJoining separated ordered trees#✓fully proved

Let \(L\) and \(R\) be ordered binary search trees over a type with a relation \(<\). If \(a < b\) for every key \(a\) of \(L\) and every key \(b\) of \(R\), then the join of \(L\) and \(R\) is ordered.

public theorem ordered_join {α : Type u} [LT α] {left right : BinaryTree α}
    (hLeft : Ordered left) (hRight : Ordered right)
    (hSeparated : ∀ a ∈ left, ∀ b ∈ right, a < b) :
    Ordered (join left right)

Uses 6 · Used by 1

Statement usesMembership in a binary tree · Ordered binary trees · Join of two binary trees

Proof usesA predicate holding at every key of a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · Membership in a join

Used byDeletion preserves the search-tree order

TheoremDeletion keeps the other keys#✓fully proved

Let \(t\) be a binary tree over a linearly ordered type, not necessarily ordered, and let \(x\) and \(y\) be keys with \(y \ne x\). If \(y\) occurs in \(t\), then \(y\) occurs in the tree obtained by deleting \(x\) from \(t\).

public theorem mem_delete_of_mem {α : Type u} [LinearOrder α] {x y : α}
    {tree : BinaryTree α} (hy : y ∈ tree) (hxy : y ≠ x) :
    y ∈ delete x tree

Uses 4 · Used by 1

Statement usesMembership in a binary tree · Deletion from a binary search tree

Proof usesJoin of two binary trees · Membership in a join

Used byMembership after deletion

TheoremThe deleted key is gone#✓fully proved

If \(t\) is an ordered binary search tree over a linearly ordered type and \(x\) is a key, then \(x\) does not occur in the tree obtained by deleting \(x\) from \(t\).

public theorem not_mem_delete_self {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} (hTree : Ordered tree) : x ∉ delete x tree

Uses 7 · Used by 1

Statement usesMembership in a binary tree · Ordered binary trees · Deletion from a binary search tree

Proof usesA predicate holding at every key of a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · Join of two binary trees · Membership in a join

Used byMembership after deletion

TheoremMembership after deletion#✓fully proved

If \(t\) is an ordered binary search tree over a linearly ordered type, then for all keys \(x\) and \(y\), the key \(y\) occurs in the tree obtained by deleting \(x\) from \(t\) if and only if \(y\) occurs in \(t\) and \(y \ne x\).

public theorem mem_delete {α : Type u} [LinearOrder α] {x y : α}
    {tree : BinaryTree α} (hTree : Ordered tree) :
    y ∈ delete x tree ↔ y ∈ tree ∧ y ≠ x

Uses 7

Statement usesMembership in a binary tree · Ordered binary trees · Deletion from a binary search tree

Proof usesJoin of two binary trees · Deletion keeps the other keys · Membership in a join · The deleted key is gone

TheoremDeletion preserves the search-tree order#✓fully proved

If \(t\) is an ordered binary search tree over a linearly ordered type, then for every key \(x\) the tree obtained by deleting \(x\) from \(t\) is ordered.

public theorem ordered_delete {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} (hTree : Ordered tree) :
    Ordered (delete x tree)

Uses 8

Statement usesOrdered binary trees · Deletion from a binary search tree

Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · Join of two binary trees · Membership in a join · Joining separated ordered trees

TheoremInorder traversal after deletion#✓fully proved

If \(t\) is an ordered binary search tree over a linearly ordered type and \(x\) is a key, then the inorder traversal of the tree obtained by deleting \(x\) from \(t\) is the inorder traversal of \(t\) with the first occurrence of \(x\) removed (and is the inorder traversal of \(t\) itself if \(x\) does not occur in it).

public theorem inorder_delete {α : Type u} [LinearOrder α] {x : α}
    {tree : BinaryTree α} (hTree : Ordered tree) :
    inorder (delete x tree) = (inorder tree).erase x

Uses 10

Statement usesOrdered binary trees · Deletion from a binary search tree · Inorder traversal of a binary tree

Proof usesA predicate holding at every key of a binary tree · Membership in a binary tree · A predicate holds at all keys of a binary tree iff it holds at all its members · Inorder traversal of a binary tree with an accumulator · Inorder traversal of a join · Join of two binary trees · Membership in the inorder traversal of a binary tree

36 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.