		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)