		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svarlist-boundedp

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

Signature
(svarlist-boundedp 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-boundedp

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

Theorem: svarlist-boundedp-of-svarlist-fix-x

(defthm svarlist-boundedp-of-svarlist-fix-x
        (equal (svarlist-boundedp (svarlist-fix x)
                                  bound)
               (svarlist-boundedp x bound)))

Theorem: svarlist-boundedp-svarlist-equiv-congruence-on-x

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

Theorem: svarlist-boundedp-of-nfix-bound

(defthm svarlist-boundedp-of-nfix-bound
        (equal (svarlist-boundedp x (nfix bound))
               (svarlist-boundedp x bound)))

Theorem: svarlist-boundedp-nat-equiv-congruence-on-bound

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

Theorem: svarlist-boundedp-of-greater

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

Subtopics

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