Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)

Literature.

[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

Chapter. Programs Operating on Trees.

Section. Binary Search Trees.

[CL] Remark. See the auxiliary module Maux.

Insertion in binary search trees.

• \cup {x} = \frac{x}{• ∣ •}

\frac{y}{l ∣ r} \cup {x} = \frac{y}{l \cup {x} ∣ r} \leftarrow x < y

\frac{y}{l ∣ r} \cup {x} = \frac{y}{l ∣ r} \leftarrow x = y

\frac{y}{l ∣ r} \cup {x} = \frac{y}{l ∣ r \cup {x}} \leftarrow x > y

Exercise. Prove

Bst (t) \to y \in t \cup {x} \leftrightarrow y \in t \lor y = x

Bst (t) \to Bst (t \cup {x})

Bst (t) \to y \in t \cup {x} \leftrightarrow y \in t \lor y = x

Bst (t) \to Bst (t \cup {x})