		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-post-order

Create a post-order list of values from a tree.

Signature
(tree-post-order tree) → list
Arguments: tree — Guard (binary-tree-p tree).
Returns: list — Type (true-listp list).

Definitions and Theorems

Function: tree-post-order

(defun tree-post-order (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (let ((__function__ 'tree-post-order))
    (declare (ignorable __function__))
    (if (tree-emptyp tree)
        nil
      (append (tree-pre-order (tree-left tree))
              (append (tree-post-order (tree-right tree))
                      (list (tree-head tree)))))))

Theorem: true-listp-of-tree-post-order

(defthm true-listp-of-tree-post-order
  (b* ((list (tree-post-order tree)))
    (true-listp list))
  :rule-classes :rewrite)