		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svex->lhs-bound

Signature
(svex->lhs-bound w x) → lhs
Arguments: w — Guard (natp w).; x — Guard (svex-p x).
Returns: lhs — Type (lhs-p lhs).

Definitions and Theorems

Function: svex->lhs-bound

(defun svex->lhs-bound (w x)
  (declare (xargs :guard (and (natp w) (svex-p x))))
  (declare (xargs :guard (lhssvex-bounded-p w x)))
  (let ((__function__ 'svex->lhs-bound))
    (declare (ignorable __function__))
    (svex->lhs-range 0 w x)))

Theorem: lhs-p-of-svex->lhs-bound

(defthm lhs-p-of-svex->lhs-bound
  (b* ((lhs (svex->lhs-bound w x)))
    (lhs-p lhs))
  :rule-classes :rewrite)

Theorem: vars-of-svex->lhs-bound

(defthm vars-of-svex->lhs-bound
  (implies (not (member v (svex-vars x)))
           (not (member v (lhs-vars (svex->lhs-bound w x))))))

Theorem: svex->lhs-bound-of-nfix-w

(defthm svex->lhs-bound-of-nfix-w
  (equal (svex->lhs-bound (nfix w) x)
         (svex->lhs-bound w x)))

Theorem: svex->lhs-bound-nat-equiv-congruence-on-w

(defthm svex->lhs-bound-nat-equiv-congruence-on-w
  (implies (nat-equiv w w-equiv)
           (equal (svex->lhs-bound w x)
                  (svex->lhs-bound w-equiv x)))
  :rule-classes :congruence)

Theorem: svex->lhs-bound-of-svex-fix-x

(defthm svex->lhs-bound-of-svex-fix-x
  (equal (svex->lhs-bound w (svex-fix x))
         (svex->lhs-bound w x)))

Theorem: svex->lhs-bound-svex-equiv-congruence-on-x

(defthm svex->lhs-bound-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex->lhs-bound w x)
                  (svex->lhs-bound w x-equiv)))
  :rule-classes :congruence)

Theorem: svex->lhs-bound-correct

(defthm svex->lhs-bound-correct
  (implies (lhssvex-bounded-p w x)
           (equal (lhs-eval (svex->lhs-bound w x) env)
                  (4vec-concat (2vec (nfix w))
                               (svex-eval x env)
                               (4vec-z)))))