		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-maskfree-rewrite-nrev

Signature
(svexlist-maskfree-rewrite-nrev x acl2::nrev) → new-nrev
Arguments: x — Guard (svexlist-p x).

Definitions and Theorems

Function: svexlist-maskfree-rewrite-nrev

(defun svexlist-maskfree-rewrite-nrev (x acl2::nrev)
  (declare (xargs :stobjs (acl2::nrev)))
  (declare (xargs :guard (svexlist-p x)))
  (let ((__function__ 'svexlist-maskfree-rewrite-nrev))
    (declare (ignorable __function__))
    (b* ((acl2::nrev (acl2::nrev-fix acl2::nrev))
         ((when (atom x)) acl2::nrev)
         (first (svex-maskfree-rewrite (car x)))
         (acl2::nrev (acl2::nrev-push first acl2::nrev)))
      (svexlist-maskfree-rewrite-nrev (cdr x)
                                      acl2::nrev))))

Theorem: svexlist-maskfree-rewrite-nrev-removal

(defthm svexlist-maskfree-rewrite-nrev-removal
  (b* ((?new-nrev (svexlist-maskfree-rewrite-nrev x acl2::nrev)))
    (b* ((out-spec (svexlist-maskfree-rewrite x)))
      (equal new-nrev
             (append acl2::nrev out-spec)))))

Theorem: svexlist-maskfree-rewrite-nrev-of-svexlist-fix-x

(defthm svexlist-maskfree-rewrite-nrev-of-svexlist-fix-x
  (equal (svexlist-maskfree-rewrite-nrev (svexlist-fix x)
                                         acl2::nrev)
         (svexlist-maskfree-rewrite-nrev x acl2::nrev)))

Theorem: svexlist-maskfree-rewrite-nrev-svexlist-equiv-congruence-on-x

(defthm
      svexlist-maskfree-rewrite-nrev-svexlist-equiv-congruence-on-x
  (implies
       (svexlist-equiv x x-equiv)
       (equal (svexlist-maskfree-rewrite-nrev x acl2::nrev)
              (svexlist-maskfree-rewrite-nrev x-equiv acl2::nrev)))
  :rule-classes :congruence)