		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Matchstate-in-bounds

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

Definitions and Theorems

Function: matchstate-in-bounds

(defun matchstate-in-bounds (st str)
  (declare (xargs :guard (and (matchstate-p st) (stringp str))))
  (let ((__function__ 'matchstate-in-bounds))
    (declare (ignorable __function__))
    (b* (((matchstate st)))
      (and (<= (matchstate->index st) (strlen str))
           (backref-alist-in-bounds st.backrefs str)))))

Theorem: matchstate-in-bounds-of-make-matchstate

(defthm matchstate-in-bounds-of-make-matchstate
  (equal (matchstate-in-bounds (make-matchstate :index index
                                                :backrefs backrefs)
                               str)
         (and (<= (nfix index) (strlen str))
              (backref-alist-in-bounds backrefs str))))

Theorem: matchstate-in-bounds-implies-backref-alist-in-bounds

(defthm matchstate-in-bounds-implies-backref-alist-in-bounds
  (implies (matchstate-in-bounds st str)
           (backref-alist-in-bounds (matchstate->backrefs st)
                                    str)))

Theorem: matchstate-in-bounds-implies-index-in-bounds

(defthm matchstate-in-bounds-implies-index-in-bounds
  (implies (matchstate-in-bounds st str)
           (<= (matchstate->index st)
               (len (acl2::explode str))))
  :rule-classes ((:linear :trigger-terms ((matchstate->index st)))))

Theorem: matchstate-in-bounds-of-matchstate-fix-st

(defthm matchstate-in-bounds-of-matchstate-fix-st
  (equal (matchstate-in-bounds (matchstate-fix st)
                               str)
         (matchstate-in-bounds st str)))

Theorem: matchstate-in-bounds-matchstate-equiv-congruence-on-st

(defthm matchstate-in-bounds-matchstate-equiv-congruence-on-st
  (implies (matchstate-equiv st st-equiv)
           (equal (matchstate-in-bounds st str)
                  (matchstate-in-bounds st-equiv str)))
  :rule-classes :congruence)

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

(defthm matchstate-in-bounds-of-str-fix-str
  (equal (matchstate-in-bounds st (acl2::str-fix str))
         (matchstate-in-bounds st str)))

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

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