A tree is balanced if for every node the heights of its two subtrees differ by at most 1.
The empty tree is represented as t.
A tree with value V, left subtree L and right subtree R is
represented as t(V,X,L,R).
X is the difference of the height of R and the height of L.
X can be -1, 0 or 1.
See: Niklaus Wirth, "Algorithmen und Datenstrukturen", 5.4
The trees are ordered with respect to a total ordering r/2 on a domain a/1.
For the specification and the implementation of the addavl program see : avl.
The goal of the whole proof is to show that if we add an element to an AVL-Tree we get a new
AVL-Tree, containing all the elements it already contained, plus the new one.
This is proved in the main file of the proof, with the some helping lemmas.
LPTP, March 11, 1997