		Search-engine friendly clone of the ACL2 documentation.

Regexlist-p

Regexlist-p-basics

Basic theorems about regexlist-p, generated by std::deflist.

Definitions and Theorems

Theorem: regexlist-p-of-cons

(defthm regexlist-p-of-cons
  (equal (regexlist-p (cons acl2::a acl2::x))
         (and (regex-p acl2::a)
              (regexlist-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: regexlist-p-of-cdr-when-regexlist-p

(defthm regexlist-p-of-cdr-when-regexlist-p
  (implies (regexlist-p (double-rewrite acl2::x))
           (regexlist-p (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: regexlist-p-when-not-consp

(defthm regexlist-p-when-not-consp
  (implies (not (consp acl2::x))
           (equal (regexlist-p acl2::x)
                  (not acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: regex-p-of-car-when-regexlist-p

(defthm regex-p-of-car-when-regexlist-p
  (implies (regexlist-p acl2::x)
           (iff (regex-p (car acl2::x))
                (or (consp acl2::x) (regex-p nil))))
  :rule-classes ((:rewrite)))

Theorem: true-listp-when-regexlist-p-compound-recognizer

(defthm true-listp-when-regexlist-p-compound-recognizer
  (implies (regexlist-p acl2::x)
           (true-listp acl2::x))
  :rule-classes :compound-recognizer)