		Search-engine friendly clone of the ACL2 documentation.

Bfrstate

Bfrstate->bound

Access the node index bound field of a bfrstate object.

Signature
(bfrstate->bound x) → bound
Arguments: x — Guard (bfrstate-p x).
Returns: bound — Type (natp bound).

Definitions and Theorems

Function: bfrstate->bound$inline

(defun bfrstate->bound$inline (x)
  (declare (xargs :guard (bfrstate-p x)))
  (let ((__function__ 'bfrstate->bound))
    (declare (ignorable __function__))
    (ash (bfrstate-fix x) -2)))

Theorem: natp-of-bfrstate->bound

(defthm natp-of-bfrstate->bound
  (b* ((bound (bfrstate->bound$inline x)))
    (natp bound))
  :rule-classes :type-prescription)

Theorem: bfrstate->bound-of-bfrstate

(defthm bfrstate->bound-of-bfrstate
  (equal (bfrstate->bound (bfrstate mode bound))
         (nfix bound)))

Theorem: bfrstate->bound$inline-of-bfrstate-fix-x

(defthm bfrstate->bound$inline-of-bfrstate-fix-x
  (equal (bfrstate->bound$inline (bfrstate-fix x))
         (bfrstate->bound$inline x)))

Theorem: bfrstate->bound$inline-bfrstate-equiv-congruence-on-x

(defthm bfrstate->bound$inline-bfrstate-equiv-congruence-on-x
  (implies (bfrstate-equiv x x-equiv)
           (equal (bfrstate->bound$inline x)
                  (bfrstate->bound$inline x-equiv)))
  :rule-classes :congruence)