		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Matchstatelist-in-bounds

Signature
(matchstatelist-in-bounds sts str) → *
Arguments: sts — Guard (matchstatelist-p sts).; str — Guard (stringp str).

Definitions and Theorems

Function: matchstatelist-in-bounds

(defun matchstatelist-in-bounds (sts str)
  (declare (xargs :guard (and (matchstatelist-p sts)
                              (stringp str))))
  (let ((__function__ 'matchstatelist-in-bounds))
    (declare (ignorable __function__))
    (if (atom sts)
        t
      (and (matchstate-in-bounds (car sts) str)
           (matchstatelist-in-bounds (cdr sts)
                                     str)))))

Theorem: matchstatelist-in-bounds-of-cons

(defthm matchstatelist-in-bounds-of-cons
  (equal (matchstatelist-in-bounds (cons st rest)
                                   str)
         (and (matchstate-in-bounds st str)
              (matchstatelist-in-bounds rest str))))

Theorem: matchstatelist-in-bounds-of-nil

(defthm matchstatelist-in-bounds-of-nil
  (matchstatelist-in-bounds nil str))

Theorem: matchstatelist-in-bounds-of-remove

(defthm matchstatelist-in-bounds-of-remove
  (implies (matchstatelist-in-bounds sts x)
           (matchstatelist-in-bounds (remove st sts)
                                     x)))

Theorem: matchstatelist-in-bounds-of-set-diff

(defthm matchstatelist-in-bounds-of-set-diff
  (implies (matchstatelist-in-bounds sts x)
           (matchstatelist-in-bounds (set-difference$ sts sts2)
                                     x)))

Theorem: matchstatelist-in-bounds-of-undup

(defthm matchstatelist-in-bounds-of-undup
  (implies (matchstatelist-in-bounds sts x)
           (matchstatelist-in-bounds (undup sts)
                                     x)))

Theorem: matchstatelist-in-bounds-of-append

(defthm matchstatelist-in-bounds-of-append
  (implies (and (matchstatelist-in-bounds a x)
                (matchstatelist-in-bounds b x))
           (matchstatelist-in-bounds (append a b)
                                     x)))

Theorem: matchstatelist-in-bounds-of-rev

(defthm matchstatelist-in-bounds-of-rev
  (implies (matchstatelist-in-bounds sts x)
           (matchstatelist-in-bounds (rev sts) x)))

Theorem: matchstatelist-in-bounds-of-matches-add-backref

(defthm matchstatelist-in-bounds-of-matches-add-backref
 (implies
      (and (matchstatelist-in-bounds sts str)
           (matchstatelist-indices-gte index sts))
      (matchstatelist-in-bounds (matches-add-backref name index sts)
                                str)))

Theorem: matchstatelist-in-bounds-of-remove-zero-length

(defthm matchstatelist-in-bounds-of-remove-zero-length
 (implies
    (matchstatelist-in-bounds sts str)
    (matchstatelist-in-bounds (matches-remove-zero-length index sts)
                              str)))

Theorem: matchstate-in-bounds-of-car-of-matchstatelist

(defthm matchstate-in-bounds-of-car-of-matchstatelist
  (implies (and (matchstatelist-in-bounds sts str)
                (consp sts))
           (matchstate-in-bounds (car sts) str)))

Theorem: matchstatelist-in-bounds-of-matchstatelist-fix-sts

(defthm matchstatelist-in-bounds-of-matchstatelist-fix-sts
  (equal (matchstatelist-in-bounds (matchstatelist-fix sts)
                                   str)
         (matchstatelist-in-bounds sts str)))

Theorem: matchstatelist-in-bounds-matchstatelist-equiv-congruence-on-sts

(defthm
    matchstatelist-in-bounds-matchstatelist-equiv-congruence-on-sts
  (implies (matchstatelist-equiv sts sts-equiv)
           (equal (matchstatelist-in-bounds sts str)
                  (matchstatelist-in-bounds sts-equiv str)))
  :rule-classes :congruence)

Theorem: matchstatelist-in-bounds-of-str-fix-str

(defthm matchstatelist-in-bounds-of-str-fix-str
  (equal (matchstatelist-in-bounds sts (acl2::str-fix str))
         (matchstatelist-in-bounds sts str)))

Theorem: matchstatelist-in-bounds-streqv-congruence-on-str

(defthm matchstatelist-in-bounds-streqv-congruence-on-str
  (implies (acl2::streqv str str-equiv)
           (equal (matchstatelist-in-bounds sts str)
                  (matchstatelist-in-bounds sts str-equiv)))
  :rule-classes :congruence)