		Search-engine friendly clone of the ACL2 documentation.

Tree-nonleaf

Tree-nonleaf->branches

Get the branches field from a tree-nonleaf.

Signature
(tree-nonleaf->branches x) → branches
Arguments: x — Guard (treep x).
Returns: branches — Type (tree-list-listp branches).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: tree-nonleaf->branches$inline

(defun tree-nonleaf->branches$inline (x)
  (declare (xargs :guard (treep x)))
  (declare (xargs :guard (equal (tree-kind x) :nonleaf)))
  (let ((__function__ 'tree-nonleaf->branches))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and (equal (tree-kind x) :nonleaf) x)))
           (tree-list-list-fix (std::da-nth 1 (cdr x))))
         :exec (std::da-nth 1 (cdr x)))))

Theorem: tree-list-listp-of-tree-nonleaf->branches

(defthm tree-list-listp-of-tree-nonleaf->branches
  (b* ((branches (tree-nonleaf->branches$inline x)))
    (tree-list-listp branches))
  :rule-classes :rewrite)

Theorem: tree-nonleaf->branches$inline-of-tree-fix-x

(defthm tree-nonleaf->branches$inline-of-tree-fix-x
  (equal (tree-nonleaf->branches$inline (tree-fix x))
         (tree-nonleaf->branches$inline x)))

Theorem: tree-nonleaf->branches$inline-tree-equiv-congruence-on-x

(defthm tree-nonleaf->branches$inline-tree-equiv-congruence-on-x
  (implies (tree-equiv x x-equiv)
           (equal (tree-nonleaf->branches$inline x)
                  (tree-nonleaf->branches$inline x-equiv)))
  :rule-classes :congruence)

Theorem: tree-nonleaf->branches-when-wrong-kind

(defthm tree-nonleaf->branches-when-wrong-kind
  (implies (not (equal (tree-kind x) :nonleaf))
           (equal (tree-nonleaf->branches x)
                  (tree-list-list-fix nil))))