ϵ">]>
Literature.
[1] J. Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
Chapter. Programs Operating on Trees.
Section. Binary Trees.
Subsection. Basic Operations and Predicates.
Subtrees. Given binary trees t1 and t2 , the predicate t1 ⊴ t2 holds if the tree t1 is a subtree of the tree t2 .
We have
Section. Binary Search Trees.
Binary search trees.
Membership in binary search trees. Define the predicate x ∈s t such that
Insertion in binary search trees. Define the function t∪ {x} such that
Minimal element in a binary search tree. Define the function Mint (t) such that
Maximal element in a binary search tree. Define the function Maxt (t) such that
Deletion of the minimal element in a binary search tree. Define the function Delmint (t) such that
Deletion of the maximal element in a binary search tree. Define the function Delmaxt (t) such that
Join of two binary search trees. Define the function t1 ⊔ t2 such that
where
Define the operation with the help of the functions Maxt (t) and Delmaxt (t) , or alternatively with the help of Mint (t) and Delmint (t) .
Deletion in binary search trees. (2 points) Define the function t∖ {x} such that