		Search-engine friendly clone of the ACL2 documentation.

Truth

Index-listp

Signature
(index-listp x numvars) → *
Arguments: numvars — Guard (natp numvars).

Definitions and Theorems

Function: index-listp

(defun index-listp (x numvars)
  (declare (xargs :guard (natp numvars)))
  (let ((__function__ 'index-listp))
    (declare (ignorable __function__))
    (if (atom x)
        (eq x nil)
      (and (natp (car x))
           (< (car x) (lnfix numvars))
           (index-listp (cdr x) numvars)))))

Theorem: natp-nth-of-index-listp

(defthm natp-nth-of-index-listp
  (implies (and (index-listp x numvars)
                (< (nfix n) (len x)))
           (natp (nth n x))))

Theorem: nfix-nth-in-index-list-bound

(defthm nfix-nth-in-index-list-bound
  (implies (and (index-listp x numvars)
                (posp numvars))
           (< (nfix (nth n x)) numvars))
  :rule-classes (:rewrite :linear))

Theorem: nth-in-index-list-bound

(defthm nth-in-index-list-bound
  (implies (and (index-listp x numvars)
                (natp numvars)
                (natp (nth n x)))
           (< (nth n x) numvars))
  :rule-classes (:rewrite :linear))

Theorem: nat-listp-when-index-listp

(defthm nat-listp-when-index-listp
  (implies (index-listp x numvars)
           (nat-listp x)))

Theorem: true-listp-when-index-listp

(defthm true-listp-when-index-listp
  (implies (index-listp x numvars)
           (true-listp x))
  :rule-classes :forward-chaining)

Theorem: index-listp-of-nfix-numvars

(defthm index-listp-of-nfix-numvars
  (equal (index-listp x (nfix numvars))
         (index-listp x numvars)))

Theorem: index-listp-nat-equiv-congruence-on-numvars

(defthm index-listp-nat-equiv-congruence-on-numvars
  (implies (nat-equiv numvars numvars-equiv)
           (equal (index-listp x numvars)
                  (index-listp x numvars-equiv)))
  :rule-classes :congruence)