		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Param-declon-list-rename-fn

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

Definitions and Theorems

Theorem: param-declon-list-rename-fn-type-prescription

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

Theorem: param-declon-list-rename-fn-when-atom

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

Theorem: param-declon-list-rename-fn-of-cons

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

Theorem: param-declon-list-rename-fn-of-append

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

Theorem: consp-of-param-declon-list-rename-fn

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

Theorem: len-of-param-declon-list-rename-fn

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

Theorem: nth-of-param-declon-list-rename-fn

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

Theorem: param-declon-list-rename-fn-of-revappend

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

Theorem: param-declon-list-rename-fn-of-reverse

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