		Search-engine friendly clone of the ACL2 documentation.

Stat-root-depth-zero-p

Constraint on the root depth in the wallet state.

The key tree is rooted at the master key, which has depth 0.

Function: stat-root-depth-zero-p

(defun stat-root-depth-zero-p (stat)
  (declare (xargs :guard (statp stat)))
  (equal (bip32-key-tree->root-depth (stat->keys stat))
         0))

Theorem: booleanp-of-stat-root-depth-zero-p

(defthm booleanp-of-stat-root-depth-zero-p
  (b* ((yes/no (stat-root-depth-zero-p stat)))
    (booleanp yes/no))
  :rule-classes :rewrite)