		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Backref-in-bounds

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

Definitions and Theorems

Function: backref-in-bounds

(defun backref-in-bounds (x str)
  (declare (xargs :guard (and (backref-p x) (stringp str))))
  (let ((__function__ 'backref-in-bounds))
    (declare (ignorable __function__))
    (b* (((backref x)))
      (<= (+ x.loc x.len) (strlen str)))))

Theorem: backref-in-bounds-of-make-backref

(defthm backref-in-bounds-of-make-backref
  (equal (backref-in-bounds (backref loc len)
                            str)
         (<= (+ (nfix loc) (nfix len))
             (strlen str))))

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

(defthm backref-in-bounds-of-backref-fix-x
  (equal (backref-in-bounds (backref-fix x) str)
         (backref-in-bounds x str)))

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

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

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

(defthm backref-in-bounds-of-str-fix-str
  (equal (backref-in-bounds x (acl2::str-fix str))
         (backref-in-bounds x str)))

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

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