		Search-engine friendly clone of the ACL2 documentation.

Tree-nonleaf

Tree-nonleaf->rulename?

Get the rulename? field from a tree-nonleaf.

Signature
(tree-nonleaf->rulename? x) → rulename?
Arguments: x — Guard (treep x).
Returns: rulename? — Type (rulename-optionp rulename?).

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

Definitions and Theorems

Function: tree-nonleaf->rulename?$inline

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

Theorem: rulename-optionp-of-tree-nonleaf->rulename?

(defthm rulename-optionp-of-tree-nonleaf->rulename?
  (b* ((rulename? (tree-nonleaf->rulename?$inline x)))
    (rulename-optionp rulename?))
  :rule-classes :rewrite)

Theorem: tree-nonleaf->rulename?$inline-of-tree-fix-x

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

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

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

Theorem: tree-nonleaf->rulename?-when-wrong-kind

(defthm tree-nonleaf->rulename?-when-wrong-kind
  (implies (not (equal (tree-kind x) :nonleaf))
           (equal (tree-nonleaf->rulename? x)
                  (rulename-option-fix nil))))