ϵ">]>
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 Search Trees.
[CL] Remark. See the auxiliary module Maux*.
Membership in binary search trees. Define the predicate x ∈s t such that
Insertion in binary search trees.
Exercise. (bonus 3 points) Prove
##
Extraction of the maximal element from binary search trees. Define the function Emax (t) such that
Joining two binary search trees. Define the function t1 ⊔ t2 such that
where
Define the operation with the help of the function Emaxt (t) .
Deletion in binary search trees. Define the function t∖ {x} such that