		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhssvex-bounded-p

Signature
(lhssvex-bounded-p w x) → *
Arguments: w — Guard (natp w).; x — Guard (svex-p x).

Definitions and Theorems

Function: lhssvex-bounded-p

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

Theorem: lhssvex-bounded-p-of-nfix-w

(defthm lhssvex-bounded-p-of-nfix-w
  (equal (lhssvex-bounded-p (nfix w) x)
         (lhssvex-bounded-p w x)))

Theorem: lhssvex-bounded-p-nat-equiv-congruence-on-w

(defthm lhssvex-bounded-p-nat-equiv-congruence-on-w
  (implies (nat-equiv w w-equiv)
           (equal (lhssvex-bounded-p w x)
                  (lhssvex-bounded-p w-equiv x)))
  :rule-classes :congruence)

Theorem: lhssvex-bounded-p-of-svex-fix-x

(defthm lhssvex-bounded-p-of-svex-fix-x
  (equal (lhssvex-bounded-p w (svex-fix x))
         (lhssvex-bounded-p w x)))

Theorem: lhssvex-bounded-p-svex-equiv-congruence-on-x

(defthm lhssvex-bounded-p-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (lhssvex-bounded-p w x)
                  (lhssvex-bounded-p w x-equiv)))
  :rule-classes :congruence)