		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Enumer-list-rename-fn

Signature
(enumer-list-rename-fn c$::enumer-list uid new-fn) → fty::result
Arguments: c$::enumer-list — Guard (enumer-listp c$::enumer-list).; uid — Guard (c$::uidp uid).; new-fn — Guard (identp new-fn).
Returns: fty::result — Type (enumer-listp fty::result).

Definitions and Theorems

Theorem: enumer-list-rename-fn-type-prescription

(defthm enumer-list-rename-fn-type-prescription
  (true-listp (enumer-list-rename-fn c$::enumer-list uid new-fn))
  :rule-classes :type-prescription)

Theorem: enumer-list-rename-fn-when-atom

(defthm enumer-list-rename-fn-when-atom
  (implies (atom c$::enumer-list)
           (equal (enumer-list-rename-fn c$::enumer-list uid new-fn)
                  nil)))

Theorem: enumer-list-rename-fn-of-cons

(defthm enumer-list-rename-fn-of-cons
  (equal (enumer-list-rename-fn (cons enumer c$::enumer-list)
                                uid new-fn)
         (cons (enumer-rename-fn enumer uid new-fn)
               (enumer-list-rename-fn c$::enumer-list uid new-fn))))

Theorem: enumer-list-rename-fn-of-append

(defthm enumer-list-rename-fn-of-append
  (equal (enumer-list-rename-fn (append acl2::x acl2::y)
                                uid new-fn)
         (append (enumer-list-rename-fn acl2::x uid new-fn)
                 (enumer-list-rename-fn acl2::y uid new-fn))))

Theorem: consp-of-enumer-list-rename-fn

(defthm consp-of-enumer-list-rename-fn
  (equal (consp (enumer-list-rename-fn c$::enumer-list uid new-fn))
         (consp c$::enumer-list)))

Theorem: len-of-enumer-list-rename-fn

(defthm len-of-enumer-list-rename-fn
  (equal (len (enumer-list-rename-fn c$::enumer-list uid new-fn))
         (len c$::enumer-list)))

Theorem: nth-of-enumer-list-rename-fn

(defthm nth-of-enumer-list-rename-fn
  (equal (nth acl2::n
              (enumer-list-rename-fn c$::enumer-list uid new-fn))
         (if (< (nfix acl2::n) (len c$::enumer-list))
             (enumer-rename-fn (nth acl2::n c$::enumer-list)
                               uid new-fn)
           nil)))

Theorem: enumer-list-rename-fn-of-revappend

(defthm enumer-list-rename-fn-of-revappend
  (equal (enumer-list-rename-fn (revappend acl2::x acl2::y)
                                uid new-fn)
         (revappend (enumer-list-rename-fn acl2::x uid new-fn)
                    (enumer-list-rename-fn acl2::y uid new-fn))))

Theorem: enumer-list-rename-fn-of-reverse

(defthm enumer-list-rename-fn-of-reverse
 (equal
      (enumer-list-rename-fn (reverse c$::enumer-list)
                             uid new-fn)
      (reverse (enumer-list-rename-fn c$::enumer-list uid new-fn))))