		Search-engine friendly clone of the ACL2 documentation.

Svex-env

Svarlist-x-env

Creates an env alist that maps the given variables to X.

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

Definitions and Theorems

Function: svarlist-x-env

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

Theorem: svex-env-p-of-svarlist-x-env

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

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

(defthm svex-env-lookup-of-svarlist-x-env
  (equal (svex-env-lookup var (svarlist-x-env x))
         (4vec-x)))

Theorem: svex-env-boundp-of-svarlist-x-env

(defthm svex-env-boundp-of-svarlist-x-env
  (iff (svex-env-boundp var (svarlist-x-env x))
       (member-equal (svar-fix var)
                     (svarlist-fix x))))

Theorem: svarlist-x-env-of-svarlist-fix-x

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

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

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