		Search-engine friendly clone of the ACL2 documentation.

Sequential-type

Regp

Correlates the sequential-type of a node with the regp/xorp of its bit encoding. This bit is set for :reg, :nxst, and xor nodes, so this returns 1 for those types and 0 for others.

Signature
(regp x) → regp
Arguments: x — Guard (stypep x).
Returns: regp — Type (bitp regp).

Definitions and Theorems

Function: regp

(defun regp (x)
       (declare (xargs :guard (stypep x)))
       (let ((__function__ 'regp))
            (declare (ignorable __function__))
            (if (member (stype-fix x)
                        '(:reg :nxst :xor))
                1 0)))

Theorem: bitp-of-regp

(defthm bitp-of-regp
        (b* ((regp (regp x))) (bitp regp))
        :rule-classes :rewrite)

Theorem: stype-equiv-implies-equal-regp-1

(defthm stype-equiv-implies-equal-regp-1
        (implies (stype-equiv x x-equiv)
                 (equal (regp x) (regp x-equiv)))
        :rule-classes (:congruence))

Theorem: regp-not-zero-implies-nonempty

(defthm
     regp-not-zero-implies-nonempty
     (implies (not (equal (regp (stype (car x))) 0))
              (consp x))
     :rule-classes
     ((:forward-chaining :trigger-terms ((regp (stype (car x)))))))

Theorem: regp-of-stype-fix-x

(defthm regp-of-stype-fix-x
        (equal (regp (stype-fix x)) (regp x)))

Theorem: regp-stype-equiv-congruence-on-x

(defthm regp-stype-equiv-congruence-on-x
        (implies (stype-equiv x x-equiv)
                 (equal (regp x) (regp x-equiv)))
        :rule-classes :congruence)