		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Filepath-transunit-map-rename

Signature
(filepath-transunit-map-rename c$::filepath-transunit-map subst) → fty::result
Arguments: c$::filepath-transunit-map — Guard (filepath-transunit-mapp c$::filepath-transunit-map).; subst — Guard (ident-ident-alistp subst).
Returns: fty::result — Type (filepath-transunit-mapp fty::result).

Definitions and Theorems

Function: filepath-transunit-map-rename

(defun filepath-transunit-map-rename
       (c$::filepath-transunit-map subst)
 (declare
  (xargs
    :guard (and (filepath-transunit-mapp c$::filepath-transunit-map)
                (ident-ident-alistp subst))))
 (let ((__function__ 'filepath-transunit-map-rename))
  (declare (ignorable __function__))
  (if
   (or
    (not (mbt (filepath-transunit-mapp c$::filepath-transunit-map)))
    (omap::emptyp c$::filepath-transunit-map))
   nil
   (omap::update
       (omap::head-key c$::filepath-transunit-map)
       (transunit-rename (omap::head-val c$::filepath-transunit-map)
                         subst)
       (filepath-transunit-map-rename
            (omap::tail c$::filepath-transunit-map)
            subst)))))

Theorem: filepath-transunit-mapp-of-filepath-transunit-map-rename

(defthm filepath-transunit-mapp-of-filepath-transunit-map-rename
  (b* ((fty::result (filepath-transunit-map-rename
                         c$::filepath-transunit-map subst)))
    (filepath-transunit-mapp fty::result))
  :rule-classes :rewrite)

Theorem: filepath-transunit-map-rename-type-prescription

(defthm filepath-transunit-map-rename-type-prescription
 (true-listp
   (filepath-transunit-map-rename c$::filepath-transunit-map subst))
 :rule-classes :type-prescription)

Theorem: filepath-transunit-map-rename-when-emptyp

(defthm filepath-transunit-map-rename-when-emptyp
 (implies
  (omap::emptyp c$::filepath-transunit-map)
  (equal
    (filepath-transunit-map-rename c$::filepath-transunit-map subst)
    nil)))

Theorem: emptyp-of-filepath-transunit-map-rename

(defthm emptyp-of-filepath-transunit-map-rename
 (equal
  (omap::emptyp
   (filepath-transunit-map-rename c$::filepath-transunit-map subst))
  (omap::emptyp
      (c$::filepath-transunit-map-fix c$::filepath-transunit-map))))

Theorem: keys-of-filepath-transunit-map-rename

(defthm keys-of-filepath-transunit-map-rename
 (equal
  (omap::keys
   (filepath-transunit-map-rename c$::filepath-transunit-map subst))
  (omap::keys
      (c$::filepath-transunit-map-fix c$::filepath-transunit-map))))

Theorem: assoc-of-filepath-transunit-map-rename

(defthm assoc-of-filepath-transunit-map-rename
 (equal
  (omap::assoc
   fty::key
   (filepath-transunit-map-rename c$::filepath-transunit-map subst))
  (if
   (omap::assoc
        fty::key
        (c$::filepath-transunit-map-fix c$::filepath-transunit-map))
   (cons
    fty::key
    (transunit-rename
     (cdr
      (omap::assoc
       fty::key
       (c$::filepath-transunit-map-fix c$::filepath-transunit-map)))
     subst))
   nil)))

Theorem: filepath-transunit-map-rename-of-filepath-transunit-map-fix-filepath-transunit-map

(defthm
 filepath-transunit-map-rename-of-filepath-transunit-map-fix-filepath-transunit-map
 (equal
  (filepath-transunit-map-rename
       (c$::filepath-transunit-map-fix c$::filepath-transunit-map)
       subst)
  (filepath-transunit-map-rename c$::filepath-transunit-map subst)))

Theorem: filepath-transunit-map-rename-filepath-transunit-map-equiv-congruence-on-filepath-transunit-map

(defthm
 filepath-transunit-map-rename-filepath-transunit-map-equiv-congruence-on-filepath-transunit-map
 (implies
  (c$::filepath-transunit-map-equiv c$::filepath-transunit-map
                                    filepath-transunit-map-equiv)
  (equal
    (filepath-transunit-map-rename c$::filepath-transunit-map subst)
    (filepath-transunit-map-rename
         filepath-transunit-map-equiv subst)))
 :rule-classes :congruence)

Theorem: filepath-transunit-map-rename-of-ident-ident-alist-fix-subst

(defthm filepath-transunit-map-rename-of-ident-ident-alist-fix-subst
 (equal
  (filepath-transunit-map-rename c$::filepath-transunit-map
                                 (ident-ident-alist-fix subst))
  (filepath-transunit-map-rename c$::filepath-transunit-map subst)))

Theorem: filepath-transunit-map-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 filepath-transunit-map-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
  (ident-ident-alist-equiv subst subst-equiv)
  (equal
    (filepath-transunit-map-rename c$::filepath-transunit-map subst)
    (filepath-transunit-map-rename c$::filepath-transunit-map
                                   subst-equiv)))
 :rule-classes :congruence)