		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhssvex-unbounded-p

Signature
(lhssvex-unbounded-p x) → *
Arguments: x — Guard (svex-p x).

Definitions and Theorems

Function: lhssvex-unbounded-p

(defun lhssvex-unbounded-p (x)
  (declare (xargs :guard (svex-p x)))
  (let ((__function__ 'lhssvex-unbounded-p))
    (declare (ignorable __function__))
    (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 w lo hi) x.args))
                           (and (eq (svex-kind w) :quote)
                                (4vec-index-p (svex-quote->val w))
                                (lhssvex-unbounded-p lo)
                                (lhssvex-unbounded-p 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-unbounded-p xx))))))))

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

(defthm lhssvex-unbounded-p-of-svex-fix-x
  (equal (lhssvex-unbounded-p (svex-fix x))
         (lhssvex-unbounded-p x)))

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

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