Version: 4.1.4.3

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
;;
;;=============================================================================