		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svexarr-vars-witness-aux

Signature
(svexarr-vars-witness-aux v n svexarr) → idx
Arguments: n — Guard (natp n).
Returns: idx — Type (iff (natp idx) idx).

Definitions and Theorems

Function: svexarr-vars-witness-aux

(defun svexarr-vars-witness-aux (v n svexarr)
  (declare (xargs :stobjs (svexarr)))
  (declare (xargs :guard (natp n)))
  (declare (xargs :guard (<= (nfix n) (svexs-length svexarr))))
  (let ((__function__ 'svexarr-vars-witness-aux))
    (declare (ignorable __function__))
    (if (zp n)
        nil
      (if (member-equal v (svex-vars (get-svex (1- n) svexarr)))
          (1- n)
        (svexarr-vars-witness-aux v (1- n)
                                  svexarr)))))

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

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

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

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

Theorem: bound-of-svexarr-vars-witness-aux

(defthm bound-of-svexarr-vars-witness-aux
  (implies (svexarr-vars-witness-aux v n svexarr)
           (< (svexarr-vars-witness-aux v n svexarr)
              (nfix n)))
  :rule-classes :linear)

Theorem: svexarr-vars-aux-witness-under-iff

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

Theorem: member-svexarr-vars-aux

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

Theorem: svexarr-vars-witness-aux-of-nfix-n

(defthm svexarr-vars-witness-aux-of-nfix-n
  (equal (svexarr-vars-witness-aux v (nfix n)
                                   svexarr)
         (svexarr-vars-witness-aux v n svexarr)))

Theorem: svexarr-vars-witness-aux-nat-equiv-congruence-on-n

(defthm svexarr-vars-witness-aux-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (svexarr-vars-witness-aux v n svexarr)
                  (svexarr-vars-witness-aux v n-equiv svexarr)))
  :rule-classes :congruence)