		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Initdeclor-list-rename-fn

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

Definitions and Theorems

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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