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