		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Maybe-backref-in-bounds

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

Definitions and Theorems

Function: maybe-backref-in-bounds

(defun maybe-backref-in-bounds (x str)
  (declare (xargs :guard (and (maybe-backref-p x)
                              (stringp str))))
  (let ((__function__ 'maybe-backref-in-bounds))
    (declare (ignorable __function__))
    (or (not x) (backref-in-bounds x str))))

Theorem: backref-in-bounds-when-maybe-backref-in-bounds

(defthm backref-in-bounds-when-maybe-backref-in-bounds
  (implies x
           (iff (maybe-backref-in-bounds x str)
                (backref-in-bounds x str))))

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

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

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

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

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

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

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

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