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