		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Backref-alist-in-bounds

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

Definitions and Theorems

Function: backref-alist-in-bounds

(defun backref-alist-in-bounds (x str)
  (declare (xargs :guard (and (backref-alist-p x)
                              (stringp str))))
  (let ((__function__ 'backref-alist-in-bounds))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (or (not (mbt (consp (car x))))
               (backref-in-bounds (cdar x) str))
           (backref-alist-in-bounds (cdr x)
                                    str)))))

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

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

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

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

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

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

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

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

Theorem: backref-alist-in-bounds-of-cons

(defthm backref-alist-in-bounds-of-cons
  (equal (backref-alist-in-bounds (cons (cons key backref) rest)
                                  str)
         (and (backref-in-bounds backref str)
              (backref-alist-in-bounds rest str))))

Theorem: backref-alist-in-bounds-of-nil

(defthm backref-alist-in-bounds-of-nil
  (backref-alist-in-bounds nil str))

Theorem: backref-in-bounds-of-lookup

(defthm backref-in-bounds-of-lookup
  (implies (and (backref-alist-in-bounds x str)
                (cdr (assoc name x)))
           (backref-in-bounds (cdr (assoc name x))
                              str)))