		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstack-to-svex-alist

Signature
(svstack-to-svex-alist x) → x-alist
Arguments: x — Guard (svstack-p x).
Returns: x-alist — Type (svex-alist-p x-alist).

Definitions and Theorems

Function: svstack-to-svex-alist

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

Theorem: svex-alist-p-of-svstack-to-svex-alist

(defthm svex-alist-p-of-svstack-to-svex-alist
  (b* ((x-alist (svstack-to-svex-alist x)))
    (svex-alist-p x-alist))
  :rule-classes :rewrite)

Theorem: svex-lookup-of-svstack-to-svex-alist-cons

(defthm svex-lookup-of-svstack-to-svex-alist-cons
  (equal (svex-lookup k (svstack-to-svex-alist (cons a b)))
         (or (svex-lookup k a)
             (svex-lookup k (svstack-to-svex-alist b)))))

Theorem: svex-lookup-of-svstack-to-svex-alist-consp

(defthm svex-lookup-of-svstack-to-svex-alist-consp
 (implies
      (consp x)
      (equal (svex-lookup k (svstack-to-svex-alist x))
             (or (svex-lookup k (car x))
                 (svex-lookup k (svstack-to-svex-alist (cdr x)))))))

Theorem: svex-vars-of-svstack-to-svex-alist-cons

(defthm svex-vars-of-svstack-to-svex-alist-cons
  (set-equiv (svex-alist-vars (svstack-to-svex-alist (cons a b)))
             (append (svex-alist-vars a)
                     (svex-alist-vars (svstack-to-svex-alist b)))))

Theorem: svstack-to-svex-alist-when-atom

(defthm svstack-to-svex-alist-when-atom
  (implies (atom x)
           (equal (svstack-to-svex-alist x) nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svstack-to-svex-alist-of-svstack-fix-x

(defthm svstack-to-svex-alist-of-svstack-fix-x
  (equal (svstack-to-svex-alist (svstack-fix x))
         (svstack-to-svex-alist x)))

Theorem: svstack-to-svex-alist-svstack-equiv-congruence-on-x

(defthm svstack-to-svex-alist-svstack-equiv-congruence-on-x
  (implies (svstack-equiv x x-equiv)
           (equal (svstack-to-svex-alist x)
                  (svstack-to-svex-alist x-equiv)))
  :rule-classes :congruence)