		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhssvex-range-p

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

Definitions and Theorems

Function: lhssvex-range-p

(defun lhssvex-range-p (rsh w x)
 (declare (xargs :guard (and (natp rsh) (natp w) (svex-p x))))
 (let ((__function__ 'lhssvex-range-p))
  (declare (ignorable __function__))
  (if (zp w)
      t
   (svex-case
    x :var t :quote (equal x.val (4vec-z))
    :call
    (case x.fn
     (concat
      (b* (((unless (eql (len x.args) 3)) nil)
           ((list w1 lo hi) x.args))
       (and
         (eq (svex-kind w1) :quote)
         (4vec-index-p (svex-quote->val w1))
         (b* ((w1 (2vec->val (svex-quote->val w1))))
           (cond ((<= w1 (lnfix rsh))
                  (lhssvex-range-p (- (lnfix rsh) w1)
                                   w hi))
                 ((<= (+ (lnfix rsh) w) w1)
                  (lhssvex-range-p rsh w lo))
                 (t (and (lhssvex-range-p rsh (- w1 (lnfix rsh))
                                          lo)
                         (lhssvex-range-p 0 (- (+ w (lnfix rsh)) w1)
                                          hi))))))))
     (rsh
        (b* (((unless (eql (len x.args) 2)) nil)
             ((list sh xx) x.args))
          (and (eq (svex-kind sh) :quote)
               (4vec-index-p (svex-quote->val sh))
               (lhssvex-range-p (+ (lnfix rsh)
                                   (2vec->val (svex-quote->val sh)))
                                w xx)))))))))

Theorem: lhssvex-range-p-of-nfix-rsh

(defthm lhssvex-range-p-of-nfix-rsh
  (equal (lhssvex-range-p (nfix rsh) w x)
         (lhssvex-range-p rsh w x)))

Theorem: lhssvex-range-p-nat-equiv-congruence-on-rsh

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

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

(defthm lhssvex-range-p-of-nfix-w
  (equal (lhssvex-range-p rsh (nfix w) x)
         (lhssvex-range-p rsh w x)))

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

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

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

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

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

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