		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstack-clean

Signature
(svstack-clean x) → new-x
Arguments: x — Guard (svstack-p x).
Returns: new-x — Type (svstack-p new-x).

Definitions and Theorems

Function: svstack-clean

(defun svstack-clean (x)
  (declare (xargs :guard (svstack-p x)))
  (let ((__function__ 'svstack-clean))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (fast-alist-clean (svex-alist-fix (car x)))
            (svstack-clean (cdr x))))))

Theorem: svstack-p-of-svstack-clean

(defthm svstack-p-of-svstack-clean
  (b* ((new-x (svstack-clean x)))
    (svstack-p new-x))
  :rule-classes :rewrite)

Theorem: member-vars-of-svstack-clean

(defthm member-vars-of-svstack-clean
 (implies
  (not (member v
               (svex-alist-vars (svstack-to-svex-alist x))))
  (not
   (member
     v
     (svex-alist-vars (svstack-to-svex-alist (svstack-clean x)))))))

Theorem: svex-lookup-of-svstack-clean

(defthm svex-lookup-of-svstack-clean
  (iff (svex-lookup v
                    (svstack-to-svex-alist (svstack-clean x)))
       (svex-lookup v (svstack-to-svex-alist x))))

Theorem: consp-of-svstack-clean

(defthm consp-of-svstack-clean
  (b* ((?new-x (svstack-clean x)))
    (equal (consp new-x) (consp x))))

Theorem: svstack-clean-of-svstack-fix-x

(defthm svstack-clean-of-svstack-fix-x
  (equal (svstack-clean (svstack-fix x))
         (svstack-clean x)))

Theorem: svstack-clean-svstack-equiv-congruence-on-x

(defthm svstack-clean-svstack-equiv-congruence-on-x
  (implies (svstack-equiv x x-equiv)
           (equal (svstack-clean x)
                  (svstack-clean x-equiv)))
  :rule-classes :congruence)