		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

Svex-envs-common-constants

Signature
(svex-envs-common-constants masks env1 env2) → consts
Arguments: masks — Guard (svex-mask-alist-p masks).; env1 — Guard (svex-env-p env1).; env2 — Guard (svex-env-p env2).
Returns: consts — Type (svex-env-p consts).

Definitions and Theorems

Function: svex-envs-common-constants

(defun svex-envs-common-constants (masks env1 env2)
  (declare (xargs :guard (and (svex-mask-alist-p masks)
                              (svex-env-p env1)
                              (svex-env-p env2))))
  (let ((__function__ 'svex-envs-common-constants))
    (declare (ignorable __function__))
    (svex-envs-common-constants-aux
         (acl2::hons-union (alist-keys (svex-env-fix env1))
                           (alist-keys (svex-env-fix env2)))
         masks env1 env2 nil)))

Theorem: svex-env-p-of-svex-envs-common-constants

(defthm svex-env-p-of-svex-envs-common-constants
  (b* ((consts (svex-envs-common-constants masks env1 env2)))
    (svex-env-p consts))
  :rule-classes :rewrite)

Theorem: not-boundp-of-svex-envs-common-constants

(defthm not-boundp-of-svex-envs-common-constants
  (b* ((?consts (svex-envs-common-constants masks env1 env2)))
    (implies (or (not (svex-env-boundp v env1))
                 (not (svex-env-boundp v env2)))
             (not (svex-env-boundp v consts)))))

Theorem: lookup-when-boundp-of-svex-envs-common-constants-equals-env1

(defthm lookup-when-boundp-of-svex-envs-common-constants-equals-env1
  (b* ((?consts (svex-envs-common-constants masks env1 env2)))
    (implies (svex-env-boundp v consts)
             (equal (svex-env-lookup v consts)
                    (4vec-mask (svex-mask-lookup (svex-var v) masks)
                               (svex-env-lookup v env1))))))

Theorem: lookup-when-boundp-of-svex-envs-common-constants-equals-env2

(defthm lookup-when-boundp-of-svex-envs-common-constants-equals-env2
  (b* ((?consts (svex-envs-common-constants masks env1 env2)))
    (implies (svex-env-boundp v consts)
             (equal (svex-env-lookup v consts)
                    (4vec-mask (svex-mask-lookup (svex-var v) masks)
                               (svex-env-lookup v env2))))))