2.2 "avl-rational-keys"

(include-book "avl-rational-keys" :dir :teachpacks)

Documentation under construction.

;;=============================================================================

;; Function usage notes

;;

;; 1. (avl-retrieve tr key)

;;   assumes

;;     tr         has been constructed by one of the AVL-tree constructors

;;                (empty-tree, avl-insert, and avl-delete)

;;     new-key    is a rational number

;;

;;   delivers

;;     either a two element list (k d)

;;       such that k equals key and

;;                 tr contains a subtree with k and d in its root

;;     or nil, in case key does not occur in tr

;;

;; 2. (empty-tree)

;;   delivers an empty AVL-tree

;;

;; 3. (avl-insert tr key datum)

;;   assumes

;;      tr       has been constructed by the AVL-tree constructors

;;               (empty-tree, avl-insert, or avl-delete)

;;      key      is a rational number

;;   delivers an AVL tree with the following property

;;     (and (equal (avl-retrieve (avl-insert tr key datum) key)

;;                 (list key datum))

;;          (iff (avl-retrieve (avl-insert tr key datum) k)

;;               (or (avl-retrieve tr k)

;;                   (key= k key))))

;;

;; 4. (avl-delete tr key)

;;   assumes

;;      tr       has been constructed by the AVL-tree constructors

;;               (empty-tree, avl-insert, and avl-delete)

;;      key      is a rational number

;;   delivers an AVL tree with the following property

;;     (equal (avl-retrieve (avl-delete tr key) key)

;;            nil)

;;

;; 5. (avl-flatten tr)

;;   assumes

;;      tr       has been constructed by the AVL-tree constructors

;;               (empty-tree, avl-insert, and avl-delete)

;;   delivers a list of cons-pairs with the following properties

;;      (and (implies (occurs-in-tree? k tr)

;;                    (and (occurs-in-pairs? k (avl-flatten tr))

;;                         (meta-property-DF tr k)))

;;           (implies (not (occurs-in-tree? k tr))

;;                    (not (occurs-in-pairs? k (avl-flatten tr)))))

;;           (increasing-pairs? (avl-flatten tr)))

;;     where (meta-property-DF tr k) means that one of the elements, e, in

;;     the list (avl-flatten tr) satisfies (equal (car e) k)) and

;;     (cadr e) is the datum at the root of the subtree of tr where k occurs

;;

;;=============================================================================