		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svexarr-vars

Signature
(svexarr-vars svexarr) → vars
Returns: vars — Type (svarlist-p vars).

Definitions and Theorems

Function: svexarr-vars

(defun svexarr-vars (svexarr)
  (declare (xargs :stobjs (svexarr)))
  (declare (xargs :guard t))
  (let ((__function__ 'svexarr-vars))
    (declare (ignorable __function__))
    (svexarr-vars-aux (svexs-length svexarr)
                      svexarr)))

Theorem: svarlist-p-of-svexarr-vars

(defthm svarlist-p-of-svexarr-vars
  (b* ((vars (svexarr-vars svexarr)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: vars-of-get-svex

(defthm vars-of-get-svex
  (implies (not (member v (svexarr-vars svexarr)))
           (not (member v (svex-vars (nth n svexarr))))))

Function: svexarr-vars-witness

(defun svexarr-vars-witness (v svexarr)
  (declare (xargs :stobjs (svexarr)))
  (declare (xargs :guard t))
  (let ((__function__ 'svexarr-vars-witness))
    (declare (ignorable __function__))
    (svexarr-vars-witness-aux v (svexs-length svexarr)
                              svexarr)))

Theorem: return-type-of-svexarr-vars-witness

(defthm return-type-of-svexarr-vars-witness
  (b* ((idx (svexarr-vars-witness v svexarr)))
    (iff (natp idx) idx))
  :rule-classes :rewrite)

Theorem: type-of-svexarr-vars-witness

(defthm type-of-svexarr-vars-witness
  (or (not (svexarr-vars-witness v svexarr))
      (natp (svexarr-vars-witness v svexarr)))
  :rule-classes :type-prescription)

Theorem: type-of-svexarr-vars-witness2

(defthm type-of-svexarr-vars-witness2
  (implies (svexarr-vars-witness v svexarr)
           (natp (svexarr-vars-witness v svexarr))))

Theorem: bound-of-svexarr-vars-witness

(defthm bound-of-svexarr-vars-witness
  (implies (svexarr-vars-witness v svexarr)
           (< (svexarr-vars-witness v svexarr)
              (len svexarr)))
  :rule-classes
  ((:rewrite
        :corollary (implies (and (svexarr-vars-witness v svexarr)
                                 (equal y (len svexarr)))
                            (< (svexarr-vars-witness v svexarr)
                               y)))))

Theorem: svexarr-vars-witness-under-iff

(defthm svexarr-vars-witness-under-iff
  (implies
       (not (member v
                    (svex-vars (nth (svexarr-vars-witness v svexarr)
                                    svexarr))))
       (not (svexarr-vars-witness v svexarr))))

Theorem: member-svexarr-vars

(defthm member-svexarr-vars
  (implies (not (svexarr-vars-witness v svexarr))
           (not (member v (svexarr-vars svexarr)))))