		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-equiv

Equivalence up to tree-fix.

Signature
(tree-equiv x y) → *
Arguments: x — Guard (binary-tree-p x).; y — Guard (binary-tree-p y).

Definitions and Theorems

Function: tree-equiv$inline

(defun tree-equiv$inline (x y)
  (declare (xargs :guard (and (binary-tree-p x)
                              (binary-tree-p y))))
  (declare (xargs :type-prescription (booleanp (tree-equiv x y))))
  (equal (tree-fix x) (tree-fix y)))

Theorem: tree-equiv-is-an-equivalence

(defthm tree-equiv-is-an-equivalence
  (and (booleanp (tree-equiv x y))
       (tree-equiv x x)
       (implies (tree-equiv x y)
                (tree-equiv y x))
       (implies (and (tree-equiv x y) (tree-equiv y z))
                (tree-equiv x z)))
  :rule-classes (:equivalence))