		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Lhs->mask

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

Definitions and Theorems

Function: lhs->mask

(defun lhs->mask (x)
  (declare (xargs :guard (lhs-p x)))
  (let ((__function__ 'lhs->mask))
    (declare (ignorable __function__))
    (b* (((when (atom x)) 0)
         ((lhrange xf) (car x))
         (rest (ash (lhs->mask (cdr x)) xf.w))
         ((when (eq (lhatom-kind xf.atom) :z))
          rest))
      (logior (lognot (ash -1 xf.w)) rest))))

Theorem: natp-of-lhs->mask

(defthm natp-of-lhs->mask
  (b* ((mask (lhs->mask x))) (natp mask))
  :rule-classes :type-prescription)

Theorem: lhs->mask-of-lhs-fix-x

(defthm lhs->mask-of-lhs-fix-x
  (equal (lhs->mask (lhs-fix x))
         (lhs->mask x)))

Theorem: lhs->mask-lhs-equiv-congruence-on-x

(defthm lhs->mask-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs->mask x)
                  (lhs->mask x-equiv)))
  :rule-classes :congruence)