		Search-engine friendly clone of the ACL2 documentation.

Lhprobe

Lhprobe/4vec-vars

Collect variables present in an lhprobe/4vec

Signature
(lhprobe/4vec-vars x) → vars
Arguments: x — Guard (lhprobe/4vec-p x).
Returns: vars — Type (svarlist-p vars).

Definitions and Theorems

Function: lhprobe/4vec-vars

(defun lhprobe/4vec-vars (x)
  (declare (xargs :guard (lhprobe/4vec-p x)))
  (let ((__function__ 'lhprobe/4vec-vars))
    (declare (ignorable __function__))
    (lhprobe/4vec-case x
                       :4vec nil
                       :lhprobe (lhprobe-vars x))))

Theorem: svarlist-p-of-lhprobe/4vec-vars

(defthm svarlist-p-of-lhprobe/4vec-vars
  (b* ((vars (lhprobe/4vec-vars x)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: lhprobe/4vec-eval-of-svex-envlist-extract-vars

(defthm lhprobe/4vec-eval-of-svex-envlist-extract-vars
 (implies
  (subsetp-equal (lhprobe/4vec-vars x)
                 (svarlist-fix vars))
  (equal (lhprobe/4vec-eval x (svex-envlist-extract-keys vars envs))
         (lhprobe/4vec-eval x envs))))

Theorem: lhprobe/4vec-vars-of-lhprobe/4vec-fix-x

(defthm lhprobe/4vec-vars-of-lhprobe/4vec-fix-x
  (equal (lhprobe/4vec-vars (lhprobe/4vec-fix x))
         (lhprobe/4vec-vars x)))

Theorem: lhprobe/4vec-vars-lhprobe/4vec-equiv-congruence-on-x

(defthm lhprobe/4vec-vars-lhprobe/4vec-equiv-congruence-on-x
  (implies (lhprobe/4vec-equiv x x-equiv)
           (equal (lhprobe/4vec-vars x)
                  (lhprobe/4vec-vars x-equiv)))
  :rule-classes :congruence)