		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Genassoc-list-rename-fn

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

Definitions and Theorems

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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