		Search-engine friendly clone of the ACL2 documentation.

Svex-env

Svarlist-x-subst

Creates a substitution alist that maps the given variables to X.

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

Definitions and Theorems

Function: svarlist-x-subst

(defun svarlist-x-subst (x)
  (declare (xargs :guard (svarlist-p x)))
  (let ((__function__ 'svarlist-x-subst))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil))
      (cons (cons (svar-fix (car x)) (svex-x))
            (svarlist-x-subst (cdr x))))))

Theorem: svex-alist-p-of-svarlist-x-subst

(defthm svex-alist-p-of-svarlist-x-subst
  (b* ((subst (svarlist-x-subst x)))
    (svex-alist-p subst))
  :rule-classes :rewrite)

Theorem: svex-lookup-of-svarlist-x-subst

(defthm svex-lookup-of-svarlist-x-subst
  (implies (and (not (member v (svarlist-fix x)))
                (svar-p v))
           (not (svex-lookup v (svarlist-x-subst x)))))

Theorem: vars-of-svarlist-x-subst

(defthm vars-of-svarlist-x-subst
  (equal (svex-alist-vars (svarlist-x-subst x))
         nil))

Theorem: svex-alist-eval-of-svarlist-x-subst

(defthm svex-alist-eval-of-svarlist-x-subst
  (equal (svex-alist-eval (svarlist-x-subst x)
                          env)
         (svarlist-x-env x)))

Theorem: svex-alist-keys-of-svarlist-x-subst

(defthm svex-alist-keys-of-svarlist-x-subst
  (equal (svex-alist-keys (svarlist-x-subst x))
         (svarlist-fix x)))

Theorem: svarlist-x-subst-of-svarlist-fix-x

(defthm svarlist-x-subst-of-svarlist-fix-x
  (equal (svarlist-x-subst (svarlist-fix x))
         (svarlist-x-subst x)))

Theorem: svarlist-x-subst-svarlist-equiv-congruence-on-x

(defthm svarlist-x-subst-svarlist-equiv-congruence-on-x
  (implies (svarlist-equiv x x-equiv)
           (equal (svarlist-x-subst x)
                  (svarlist-x-subst x-equiv)))
  :rule-classes :congruence)