		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svarlist-idxaddr-okp

(svarlist-idxaddr-okp x bound) recognizes lists where every element satisfies svar-idxaddr-okp.

Signature
(svarlist-idxaddr-okp x bound) → std::bool

This is an ordinary std::deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: svarlist-idxaddr-okp

(defun svarlist-idxaddr-okp (x bound)
  (declare (xargs :guard (and (svarlist-p x) (natp bound))))
  (let ((__function__ 'svarlist-idxaddr-okp))
    (declare (ignorable __function__))
    (if (consp x)
        (and (svar-idxaddr-okp (car x) bound)
             (svarlist-idxaddr-okp (cdr x) bound))
      t)))

Theorem: svarlist-idxaddr-okp-of-svarlist-fix-x

(defthm svarlist-idxaddr-okp-of-svarlist-fix-x
  (equal (svarlist-idxaddr-okp (svarlist-fix x)
                               bound)
         (svarlist-idxaddr-okp x bound)))

Theorem: svarlist-idxaddr-okp-svarlist-equiv-congruence-on-x

(defthm svarlist-idxaddr-okp-svarlist-equiv-congruence-on-x
  (implies (svarlist-equiv x x-equiv)
           (equal (svarlist-idxaddr-okp x bound)
                  (svarlist-idxaddr-okp x-equiv bound)))
  :rule-classes :congruence)

Theorem: svarlist-idxaddr-okp-of-nfix-bound

(defthm svarlist-idxaddr-okp-of-nfix-bound
  (equal (svarlist-idxaddr-okp x (nfix bound))
         (svarlist-idxaddr-okp x bound)))

Theorem: svarlist-idxaddr-okp-nat-equiv-congruence-on-bound

(defthm svarlist-idxaddr-okp-nat-equiv-congruence-on-bound
  (implies (nat-equiv bound bound-equiv)
           (equal (svarlist-idxaddr-okp x bound)
                  (svarlist-idxaddr-okp x bound-equiv)))
  :rule-classes :congruence)

Theorem: svarlist-idxaddr-okp-of-greater

(defthm svarlist-idxaddr-okp-of-greater
  (implies (and (svarlist-idxaddr-okp x bound1)
                (<= (nfix bound1) (nfix bound2)))
           (svarlist-idxaddr-okp x bound2)))

Subtopics

Svarlist-idxaddr-okp-basics: Basic theorems about svarlist-idxaddr-okp, generated by std::deflist.