		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Matchresult-in-bounds

Signature
(matchresult-in-bounds x) → *
Arguments: x — Guard (matchresult-p x).

Definitions and Theorems

Function: matchresult-in-bounds

(defun matchresult-in-bounds (x)
  (declare (xargs :guard (matchresult-p x)))
  (let ((__function__ 'matchresult-in-bounds))
    (declare (ignorable __function__))
    (b* (((matchresult x)))
      (and (mbe :logic
                (<= (+ x.loc x.len) (strlen x.str))
                :exec
                (if x.loc (<= (+ x.loc x.len) (strlen x.str))
                  (<= x.len (strlen x.str))))
           (backref-alist-in-bounds x.backrefs x.str)))))

Theorem: matchresult-in-bounds-of-matchresult-fix-x

(defthm matchresult-in-bounds-of-matchresult-fix-x
  (equal (matchresult-in-bounds (matchresult-fix x))
         (matchresult-in-bounds x)))

Theorem: matchresult-in-bounds-matchresult-equiv-congruence-on-x

(defthm matchresult-in-bounds-matchresult-equiv-congruence-on-x
  (implies (matchresult-equiv x x-equiv)
           (equal (matchresult-in-bounds x)
                  (matchresult-in-bounds x-equiv)))
  :rule-classes :congruence)