		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Exprs/decls/stmts-rename-fn

Definitions and Theorems

Function: expr-rename-fn

(defun expr-rename-fn (c$::expr uid new-fn)
 (declare (xargs :guard (and (exprp c$::expr)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::expr uid new-fn))
 (expr-case
  c$::expr
  :ident (expr-fix c$::expr)
  :const (expr-fix c$::expr)
  :string (expr-fix c$::expr)
  :paren
  (expr-paren (expr-rename-fn (c$::expr-paren->inner c$::expr)
                              uid new-fn))
  :gensel
  (c$::expr-gensel
       (expr-rename-fn (c$::expr-gensel->control c$::expr)
                       uid new-fn)
       (genassoc-list-rename-fn (c$::expr-gensel->assocs c$::expr)
                                uid new-fn))
  :arrsub
  (c$::expr-arrsub (expr-rename-fn (c$::expr-arrsub->arg1 c$::expr)
                                   uid new-fn)
                   (expr-rename-fn (c$::expr-arrsub->arg2 c$::expr)
                                   uid new-fn)
                   (c$::expr-arrsub->info c$::expr))
  :funcall
  (make-expr-funcall
       :fun (expr-funcall-fun-rename-fn expr.fun uid new-fn)
       :args (expr-list-rename-fn expr.args uid new-fn))
  :member
  (c$::expr-member (expr-rename-fn (c$::expr-member->arg c$::expr)
                                   uid new-fn)
                   (c$::expr-member->name c$::expr))
  :memberp
  (c$::expr-memberp (expr-rename-fn (c$::expr-memberp->arg c$::expr)
                                    uid new-fn)
                    (c$::expr-memberp->name c$::expr))
  :complit
  (c$::expr-complit
       (tyname-rename-fn (c$::expr-complit->type c$::expr)
                         uid new-fn)
       (desiniter-list-rename-fn (c$::expr-complit->elems c$::expr)
                                 uid new-fn)
       (c$::expr-complit->final-comma c$::expr))
  :unary
  (c$::expr-unary (c$::expr-unary->op c$::expr)
                  (expr-rename-fn (c$::expr-unary->arg c$::expr)
                                  uid new-fn)
                  (c$::expr-unary->info c$::expr))
  :label-addr (expr-fix c$::expr)
  :sizeof
  (expr-sizeof (tyname-rename-fn (c$::expr-sizeof->type c$::expr)
                                 uid new-fn))
  :sizeof-ambig
  (c$::expr-sizeof-ambig
       (amb-expr/tyname-rename-fn
            (c$::expr-sizeof-ambig->expr/tyname c$::expr)
            uid new-fn))
  :alignof
  (expr-alignof (tyname-rename-fn (c$::expr-alignof->type c$::expr)
                                  uid new-fn)
                (c$::expr-alignof->uscores c$::expr))
  :alignof-ambig
  (c$::expr-alignof-ambig
       (amb-expr/tyname-rename-fn
            (c$::expr-alignof-ambig->expr/tyname c$::expr)
            uid new-fn)
       (c$::expr-alignof-ambig->uscores c$::expr))
  :cast
  (c$::expr-cast (tyname-rename-fn (c$::expr-cast->type c$::expr)
                                   uid new-fn)
                 (expr-rename-fn (c$::expr-cast->arg c$::expr)
                                 uid new-fn))
  :binary
  (c$::expr-binary (expr-binary->op c$::expr)
                   (expr-rename-fn (expr-binary->arg1 c$::expr)
                                   uid new-fn)
                   (expr-rename-fn (expr-binary->arg2 c$::expr)
                                   uid new-fn)
                   (c$::expr-binary->info c$::expr))
  :cond (c$::expr-cond
             (expr-rename-fn (c$::expr-cond->test c$::expr)
                             uid new-fn)
             (expr-option-rename-fn (c$::expr-cond->then c$::expr)
                                    uid new-fn)
             (expr-rename-fn (c$::expr-cond->else c$::expr)
                             uid new-fn))
  :comma
  (c$::expr-comma (expr-rename-fn (c$::expr-comma->first c$::expr)
                                  uid new-fn)
                  (expr-rename-fn (c$::expr-comma->next c$::expr)
                                  uid new-fn))
  :cast/call-ambig
  (c$::expr-cast/call-ambig
       (amb-expr/tyname-rename-fn
            (c$::expr-cast/call-ambig->type/fun c$::expr)
            uid new-fn)
       (c$::expr-cast/call-ambig->inc/dec c$::expr)
       (expr-rename-fn (c$::expr-cast/call-ambig->arg/rest c$::expr)
                       uid new-fn))
  :cast/mul-ambig
  (c$::expr-cast/mul-ambig
       (amb-expr/tyname-rename-fn
            (c$::expr-cast/mul-ambig->type/arg1 c$::expr)
            uid new-fn)
       (c$::expr-cast/mul-ambig->inc/dec c$::expr)
       (expr-rename-fn (c$::expr-cast/mul-ambig->arg/arg2 c$::expr)
                       uid new-fn))
  :cast/add-ambig
  (c$::expr-cast/add-ambig
       (amb-expr/tyname-rename-fn
            (c$::expr-cast/add-ambig->type/arg1 c$::expr)
            uid new-fn)
       (c$::expr-cast/add-ambig->inc/dec c$::expr)
       (expr-rename-fn (c$::expr-cast/add-ambig->arg/arg2 c$::expr)
                       uid new-fn))
  :cast/sub-ambig
  (c$::expr-cast/sub-ambig
       (amb-expr/tyname-rename-fn
            (c$::expr-cast/sub-ambig->type/arg1 c$::expr)
            uid new-fn)
       (c$::expr-cast/sub-ambig->inc/dec c$::expr)
       (expr-rename-fn (c$::expr-cast/sub-ambig->arg/arg2 c$::expr)
                       uid new-fn))
  :cast/and-ambig
  (c$::expr-cast/and-ambig
       (amb-expr/tyname-rename-fn
            (c$::expr-cast/and-ambig->type/arg1 c$::expr)
            uid new-fn)
       (c$::expr-cast/and-ambig->inc/dec c$::expr)
       (expr-rename-fn (c$::expr-cast/and-ambig->arg/arg2 c$::expr)
                       uid new-fn))
  :cast/logand-ambig
  (c$::expr-cast/logand-ambig
     (amb-expr/tyname-rename-fn
          (c$::expr-cast/logand-ambig->type/arg1 c$::expr)
          uid new-fn)
     (c$::expr-cast/logand-ambig->inc/dec c$::expr)
     (expr-rename-fn (c$::expr-cast/logand-ambig->arg/arg2 c$::expr)
                     uid new-fn))
  :stmt
  (expr-stmt (comp-stmt-rename-fn (c$::expr-stmt->stmt c$::expr)
                                  uid new-fn))
  :tycompat
  (c$::expr-tycompat
       (tyname-rename-fn (c$::expr-tycompat->type1 c$::expr)
                         uid new-fn)
       (tyname-rename-fn (c$::expr-tycompat->type2 c$::expr)
                         uid new-fn))
  :offsetof
  (c$::expr-offsetof
     (tyname-rename-fn (c$::expr-offsetof->type c$::expr)
                       uid new-fn)
     (member-designor-rename-fn (c$::expr-offsetof->member c$::expr)
                                uid new-fn))
  :va-arg (c$::expr-va-arg
               (expr-rename-fn (c$::expr-va-arg->list c$::expr)
                               uid new-fn)
               (tyname-rename-fn (c$::expr-va-arg->type c$::expr)
                                 uid new-fn))
  :extension
  (expr-extension
       (expr-rename-fn (c$::expr-extension->expr c$::expr)
                       uid new-fn))))

Function: expr-list-rename-fn

(defun expr-list-rename-fn (c$::expr-list uid new-fn)
  (declare (xargs :guard (and (expr-listp c$::expr-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::expr-list)
      nil
    (cons (expr-rename-fn (car c$::expr-list)
                          uid new-fn)
          (expr-list-rename-fn (cdr c$::expr-list)
                               uid new-fn))))

Function: expr-option-rename-fn

(defun expr-option-rename-fn (c$::expr-option uid new-fn)
 (declare (xargs :guard (and (expr-optionp c$::expr-option)
                             (c$::uidp uid)
                             (identp new-fn))))
 (expr-option-case
    c$::expr-option
    :some
    (expr-fix
         (expr-rename-fn (c$::expr-option-some->val c$::expr-option)
                         uid new-fn))
    :none nil))

Function: const-expr-rename-fn

(defun const-expr-rename-fn (const-expr uid new-fn)
  (declare (xargs :guard (and (const-exprp const-expr)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable const-expr uid new-fn))
  (const-expr (expr-rename-fn (const-expr->expr const-expr)
                              uid new-fn)))

Function: const-expr-option-rename-fn

(defun const-expr-option-rename-fn
       (c$::const-expr-option uid new-fn)
 (declare
      (xargs :guard (and (const-expr-optionp c$::const-expr-option)
                         (c$::uidp uid)
                         (identp new-fn))))
 (const-expr-option-case
   c$::const-expr-option
   :some
   (c$::const-expr-fix
        (const-expr-rename-fn
             (c$::const-expr-option-some->val c$::const-expr-option)
             uid new-fn))
   :none nil))

Function: genassoc-rename-fn

(defun genassoc-rename-fn (c$::genassoc uid new-fn)
 (declare (xargs :guard (and (genassocp c$::genassoc)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::genassoc uid new-fn))
 (genassoc-case
      c$::genassoc
      :type
      (c$::genassoc-type
           (tyname-rename-fn (c$::genassoc-type->type c$::genassoc)
                             uid new-fn)
           (expr-rename-fn (c$::genassoc-type->expr c$::genassoc)
                           uid new-fn))
      :default
      (genassoc-default
           (expr-rename-fn (c$::genassoc-default->expr c$::genassoc)
                           uid new-fn))))

Function: genassoc-list-rename-fn

(defun genassoc-list-rename-fn (c$::genassoc-list uid new-fn)
  (declare (xargs :guard (and (genassoc-listp c$::genassoc-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::genassoc-list)
      nil
    (cons (genassoc-rename-fn (car c$::genassoc-list)
                              uid new-fn)
          (genassoc-list-rename-fn (cdr c$::genassoc-list)
                                   uid new-fn))))

Function: member-designor-rename-fn

(defun member-designor-rename-fn (c$::member-designor uid new-fn)
 (declare (xargs :guard (and (member-designorp c$::member-designor)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::member-designor uid new-fn))
 (member-designor-case
     c$::member-designor
     :ident (member-designor-fix c$::member-designor)
     :dot
     (c$::member-designor-dot
          (member-designor-rename-fn
               (c$::member-designor-dot->member c$::member-designor)
               uid new-fn)
          (c$::member-designor-dot->name c$::member-designor))
     :sub
     (c$::member-designor-sub
          (member-designor-rename-fn
               (c$::member-designor-sub->member c$::member-designor)
               uid new-fn)
          (expr-rename-fn
               (c$::member-designor-sub->index c$::member-designor)
               uid new-fn))))

Function: type-spec-rename-fn

(defun type-spec-rename-fn (c$::type-spec uid new-fn)
 (declare (xargs :guard (and (type-specp c$::type-spec)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::type-spec uid new-fn))
 (type-spec-case
  c$::type-spec
  :void (type-spec-fix c$::type-spec)
  :char (type-spec-fix c$::type-spec)
  :short (type-spec-fix c$::type-spec)
  :int (type-spec-fix c$::type-spec)
  :long (type-spec-fix c$::type-spec)
  :float (type-spec-fix c$::type-spec)
  :double (type-spec-fix c$::type-spec)
  :signed (type-spec-fix c$::type-spec)
  :unsigned (type-spec-fix c$::type-spec)
  :bool (type-spec-fix c$::type-spec)
  :complex (type-spec-fix c$::type-spec)
  :atomic
  (type-spec-atomic
       (tyname-rename-fn (c$::type-spec-atomic->type c$::type-spec)
                         uid new-fn))
  :struct
  (type-spec-struct
   (struni-spec-rename-fn (c$::type-spec-struct->spec c$::type-spec)
                          uid new-fn))
  :union
  (type-spec-union
    (struni-spec-rename-fn (c$::type-spec-union->spec c$::type-spec)
                           uid new-fn))
  :enum
  (type-spec-enum
       (enum-spec-rename-fn (c$::type-spec-enum->spec c$::type-spec)
                            uid new-fn))
  :typedef (type-spec-fix c$::type-spec)
  :int128 (type-spec-fix c$::type-spec)
  :locase-float80 (type-spec-fix c$::type-spec)
  :locase-float128 (type-spec-fix c$::type-spec)
  :float16 (type-spec-fix c$::type-spec)
  :float16x (type-spec-fix c$::type-spec)
  :float32 (type-spec-fix c$::type-spec)
  :float32x (type-spec-fix c$::type-spec)
  :float64 (type-spec-fix c$::type-spec)
  :float64x (type-spec-fix c$::type-spec)
  :float128 (type-spec-fix c$::type-spec)
  :float128x (type-spec-fix c$::type-spec)
  :builtin-va-list (type-spec-fix c$::type-spec)
  :struct-empty
  (c$::type-spec-struct-empty
       (attrib-spec-list-rename-fn
            (c$::type-spec-struct-empty->attribs c$::type-spec)
            uid new-fn)
       (c$::type-spec-struct-empty->name? c$::type-spec))
  :typeof-expr
  (c$::type-spec-typeof-expr
     (expr-rename-fn (c$::type-spec-typeof-expr->expr c$::type-spec)
                     uid new-fn)
     (c$::type-spec-typeof-expr->uscores c$::type-spec))
  :typeof-type
  (c$::type-spec-typeof-type
   (tyname-rename-fn (c$::type-spec-typeof-type->type c$::type-spec)
                     uid new-fn)
   (c$::type-spec-typeof-type->uscores c$::type-spec))
  :typeof-ambig
  (c$::type-spec-typeof-ambig
       (amb-expr/tyname-rename-fn
            (c$::type-spec-typeof-ambig->expr/type c$::type-spec)
            uid new-fn)
       (c$::type-spec-typeof-ambig->uscores c$::type-spec))
  :auto-type (type-spec-fix c$::type-spec)))

Function: spec/qual-rename-fn

(defun spec/qual-rename-fn (c$::spec/qual uid new-fn)
 (declare (xargs :guard (and (spec/qual-p c$::spec/qual)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::spec/qual uid new-fn))
 (spec/qual-case
  c$::spec/qual
  :typespec
  (spec/qual-typespec
   (type-spec-rename-fn (c$::spec/qual-typespec->spec c$::spec/qual)
                        uid new-fn))
  :typequal (spec/qual-fix c$::spec/qual)
  :align
  (spec/qual-align
     (align-spec-rename-fn (c$::spec/qual-align->spec c$::spec/qual)
                           uid new-fn))
  :attrib
  (spec/qual-attrib
   (attrib-spec-rename-fn (c$::spec/qual-attrib->spec c$::spec/qual)
                          uid new-fn))))

Function: spec/qual-list-rename-fn

(defun spec/qual-list-rename-fn (c$::spec/qual-list uid new-fn)
  (declare (xargs :guard (and (spec/qual-listp c$::spec/qual-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::spec/qual-list)
      nil
    (cons (spec/qual-rename-fn (car c$::spec/qual-list)
                               uid new-fn)
          (spec/qual-list-rename-fn (cdr c$::spec/qual-list)
                                    uid new-fn))))

Function: align-spec-rename-fn

(defun align-spec-rename-fn (c$::align-spec uid new-fn)
 (declare (xargs :guard (and (align-specp c$::align-spec)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::align-spec uid new-fn))
 (align-spec-case
  c$::align-spec
  :alignas-type
  (align-spec-alignas-type
       (tyname-rename-fn
            (c$::align-spec-alignas-type->type c$::align-spec)
            uid new-fn))
  :alignas-expr
  (align-spec-alignas-expr
       (const-expr-rename-fn
            (c$::align-spec-alignas-expr->expr c$::align-spec)
            uid new-fn))
  :alignas-ambig
  (c$::align-spec-alignas-ambig
       (amb-expr/tyname-rename-fn
            (c$::align-spec-alignas-ambig->expr/type c$::align-spec)
            uid new-fn))))

Function: decl-spec-rename-fn

(defun decl-spec-rename-fn (c$::decl-spec uid new-fn)
 (declare (xargs :guard (and (decl-specp c$::decl-spec)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::decl-spec uid new-fn))
 (decl-spec-case
  c$::decl-spec
  :stoclass (decl-spec-fix c$::decl-spec)
  :typespec
  (decl-spec-typespec
   (type-spec-rename-fn (c$::decl-spec-typespec->spec c$::decl-spec)
                        uid new-fn))
  :typequal (decl-spec-fix c$::decl-spec)
  :function (decl-spec-fix c$::decl-spec)
  :align
  (decl-spec-align
     (align-spec-rename-fn (c$::decl-spec-align->spec c$::decl-spec)
                           uid new-fn))
  :attrib
  (decl-spec-attrib
   (attrib-spec-rename-fn (c$::decl-spec-attrib->spec c$::decl-spec)
                          uid new-fn))
  :stdcall (decl-spec-fix c$::decl-spec)
  :declspec (decl-spec-fix c$::decl-spec)))

Function: decl-spec-list-rename-fn

(defun decl-spec-list-rename-fn (c$::decl-spec-list uid new-fn)
  (declare (xargs :guard (and (decl-spec-listp c$::decl-spec-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::decl-spec-list)
      nil
    (cons (decl-spec-rename-fn (car c$::decl-spec-list)
                               uid new-fn)
          (decl-spec-list-rename-fn (cdr c$::decl-spec-list)
                                    uid new-fn))))

Function: typequal/attribspec-rename-fn

(defun typequal/attribspec-rename-fn
       (c$::typequal/attribspec uid new-fn)
 (declare
  (xargs
     :guard (and (c$::typequal/attribspec-p c$::typequal/attribspec)
                 (c$::uidp uid)
                 (identp new-fn))))
 (declare (ignorable c$::typequal/attribspec uid new-fn))
 (c$::typequal/attribspec-case
  c$::typequal/attribspec
  :type (c$::typequal/attribspec-fix c$::typequal/attribspec)
  :attrib
  (c$::typequal/attribspec-attrib
   (attrib-spec-rename-fn
    (c$::typequal/attribspec-attrib->unwrap c$::typequal/attribspec)
    uid new-fn))))

Function: typequal/attribspec-list-rename-fn

(defun typequal/attribspec-list-rename-fn
       (c$::typequal/attribspec-list uid new-fn)
 (declare
  (xargs
   :guard
   (and (c$::typequal/attribspec-listp c$::typequal/attribspec-list)
        (c$::uidp uid)
        (identp new-fn))))
 (if (endp c$::typequal/attribspec-list)
     nil
  (cons
   (typequal/attribspec-rename-fn (car c$::typequal/attribspec-list)
                                  uid new-fn)
   (typequal/attribspec-list-rename-fn
        (cdr c$::typequal/attribspec-list)
        uid new-fn))))

Function: typequal/attribspec-list-list-rename-fn

(defun typequal/attribspec-list-list-rename-fn
       (c$::typequal/attribspec-list-list uid new-fn)
 (declare (xargs :guard (and (typequal/attribspec-list-listp
                                  c$::typequal/attribspec-list-list)
                             (c$::uidp uid)
                             (identp new-fn))))
 (if (endp c$::typequal/attribspec-list-list)
     nil
   (cons (typequal/attribspec-list-rename-fn
              (car c$::typequal/attribspec-list-list)
              uid new-fn)
         (typequal/attribspec-list-list-rename-fn
              (cdr c$::typequal/attribspec-list-list)
              uid new-fn))))

Function: initer-rename-fn

(defun initer-rename-fn (c$::initer uid new-fn)
 (declare (xargs :guard (and (initerp c$::initer)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::initer uid new-fn))
 (initer-case
  c$::initer
  :single (initer-single
               (expr-rename-fn (c$::initer-single->expr c$::initer)
                               uid new-fn))
  :list
  (c$::initer-list
       (desiniter-list-rename-fn (c$::initer-list->elems c$::initer)
                                 uid new-fn)
       (c$::initer-list->final-comma c$::initer))))

Function: initer-option-rename-fn

(defun initer-option-rename-fn (c$::initer-option uid new-fn)
 (declare (xargs :guard (and (initer-optionp c$::initer-option)
                             (c$::uidp uid)
                             (identp new-fn))))
 (initer-option-case
  c$::initer-option
  :some
  (initer-fix
   (initer-rename-fn (c$::initer-option-some->val c$::initer-option)
                     uid new-fn))
  :none nil))

Function: desiniter-rename-fn

(defun desiniter-rename-fn (desiniter uid new-fn)
  (declare (xargs :guard (and (desiniterp desiniter)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable desiniter uid new-fn))
  (desiniter
       (designor-list-rename-fn (c$::desiniter->designors desiniter)
                                uid new-fn)
       (initer-rename-fn (c$::desiniter->initer desiniter)
                         uid new-fn)))

Function: desiniter-list-rename-fn

(defun desiniter-list-rename-fn (c$::desiniter-list uid new-fn)
  (declare (xargs :guard (and (desiniter-listp c$::desiniter-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::desiniter-list)
      nil
    (cons (desiniter-rename-fn (car c$::desiniter-list)
                               uid new-fn)
          (desiniter-list-rename-fn (cdr c$::desiniter-list)
                                    uid new-fn))))

Function: designor-rename-fn

(defun designor-rename-fn (c$::designor uid new-fn)
 (declare (xargs :guard (and (designorp c$::designor)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::designor uid new-fn))
 (designor-case
   c$::designor
   :sub
   (c$::designor-sub
        (const-expr-rename-fn (c$::designor-sub->index c$::designor)
                              uid new-fn)
        (const-expr-option-rename-fn
             (c$::designor-sub->range? c$::designor)
             uid new-fn))
   :dot (designor-fix c$::designor)))

Function: designor-list-rename-fn

(defun designor-list-rename-fn (c$::designor-list uid new-fn)
  (declare (xargs :guard (and (designor-listp c$::designor-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::designor-list)
      nil
    (cons (designor-rename-fn (car c$::designor-list)
                              uid new-fn)
          (designor-list-rename-fn (cdr c$::designor-list)
                                   uid new-fn))))

Function: declor-rename-fn

(defun declor-rename-fn (declor uid new-fn)
  (declare (xargs :guard (and (declorp declor)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable declor uid new-fn))
  (declor (typequal/attribspec-list-list-rename-fn
               (c$::declor->pointers declor)
               uid new-fn)
          (dirdeclor-rename-fn (declor->direct declor)
                               uid new-fn)))

Function: declor-option-rename-fn

(defun declor-option-rename-fn (c$::declor-option uid new-fn)
 (declare (xargs :guard (and (declor-optionp c$::declor-option)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declor-option-case
  c$::declor-option
  :some
  (declor-fix
   (declor-rename-fn (c$::declor-option-some->val c$::declor-option)
                     uid new-fn))
  :none nil))

Function: dirdeclor-rename-fn

(defun dirdeclor-rename-fn (dirdeclor uid new-fn)
 (declare (xargs :guard (and (dirdeclorp dirdeclor)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable dirdeclor uid new-fn))
 (dirdeclor-case
  dirdeclor
  :ident (dirdeclor-fix dirdeclor)
  :paren
  (dirdeclor-paren
       (declor-rename-fn (c$::dirdeclor-paren->inner dirdeclor)
                         uid new-fn))
  :array
  (c$::dirdeclor-array
       (dirdeclor-rename-fn (c$::dirdeclor-array->declor dirdeclor)
                            uid new-fn)
       (typequal/attribspec-list-rename-fn
            (c$::dirdeclor-array->qualspecs dirdeclor)
            uid new-fn)
       (expr-option-rename-fn (c$::dirdeclor-array->size? dirdeclor)
                              uid new-fn))
  :array-static1
  (c$::dirdeclor-array-static1
       (dirdeclor-rename-fn
            (c$::dirdeclor-array-static1->declor dirdeclor)
            uid new-fn)
       (typequal/attribspec-list-rename-fn
            (c$::dirdeclor-array-static1->qualspecs dirdeclor)
            uid new-fn)
       (expr-rename-fn (c$::dirdeclor-array-static1->size dirdeclor)
                       uid new-fn))
  :array-static2
  (c$::dirdeclor-array-static2
       (dirdeclor-rename-fn
            (c$::dirdeclor-array-static2->declor dirdeclor)
            uid new-fn)
       (typequal/attribspec-list-rename-fn
            (c$::dirdeclor-array-static2->qualspecs dirdeclor)
            uid new-fn)
       (expr-rename-fn (c$::dirdeclor-array-static2->size dirdeclor)
                       uid new-fn))
  :array-star
  (c$::dirdeclor-array-star
   (dirdeclor-rename-fn (c$::dirdeclor-array-star->declor dirdeclor)
                        uid new-fn)
   (typequal/attribspec-list-rename-fn
        (c$::dirdeclor-array-star->qualspecs dirdeclor)
        uid new-fn))
  :function-params
  (c$::dirdeclor-function-params
       (dirdeclor-rename-fn
            (dirdeclor-function-params->declor dirdeclor)
            uid new-fn)
       (param-declon-list-rename-fn
            (dirdeclor-function-params->params dirdeclor)
            uid new-fn)
       (c$::dirdeclor-function-params->ellipsis dirdeclor))
  :function-names
  (c$::dirdeclor-function-names
       (dirdeclor-rename-fn
            (c$::dirdeclor-function-names->declor dirdeclor)
            uid new-fn)
       (dirdeclor-function-names->names dirdeclor))))

Function: absdeclor-rename-fn

(defun absdeclor-rename-fn (absdeclor uid new-fn)
 (declare (xargs :guard (and (absdeclorp absdeclor)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable absdeclor uid new-fn))
 (absdeclor
   (typequal/attribspec-list-list-rename-fn
        (c$::absdeclor->pointers absdeclor)
        uid new-fn)
   (dirabsdeclor-option-rename-fn (c$::absdeclor->direct? absdeclor)
                                  uid new-fn)))

Function: absdeclor-option-rename-fn

(defun absdeclor-option-rename-fn (c$::absdeclor-option uid new-fn)
 (declare
      (xargs :guard (and (absdeclor-optionp c$::absdeclor-option)
                         (c$::uidp uid)
                         (identp new-fn))))
 (absdeclor-option-case
     c$::absdeclor-option
     :some
     (absdeclor-fix
          (absdeclor-rename-fn
               (c$::absdeclor-option-some->val c$::absdeclor-option)
               uid new-fn))
     :none nil))

Function: dirabsdeclor-rename-fn

(defun dirabsdeclor-rename-fn (c$::dirabsdeclor uid new-fn)
 (declare (xargs :guard (and (dirabsdeclorp c$::dirabsdeclor)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::dirabsdeclor uid new-fn))
 (dirabsdeclor-case
  c$::dirabsdeclor
  :dummy-base (dirabsdeclor-fix c$::dirabsdeclor)
  :paren (dirabsdeclor-paren
              (absdeclor-rename-fn
                   (c$::dirabsdeclor-paren->inner c$::dirabsdeclor)
                   uid new-fn))
  :array
  (c$::dirabsdeclor-array
       (dirabsdeclor-option-rename-fn
            (c$::dirabsdeclor-array->declor? c$::dirabsdeclor)
            uid new-fn)
       (typequal/attribspec-list-rename-fn
            (c$::dirabsdeclor-array->qualspecs c$::dirabsdeclor)
            uid new-fn)
       (expr-option-rename-fn
            (c$::dirabsdeclor-array->size? c$::dirabsdeclor)
            uid new-fn))
  :array-static1
  (c$::dirabsdeclor-array-static1
   (dirabsdeclor-option-rename-fn
        (c$::dirabsdeclor-array-static1->declor? c$::dirabsdeclor)
        uid new-fn)
   (typequal/attribspec-list-rename-fn
        (c$::dirabsdeclor-array-static1->qualspecs c$::dirabsdeclor)
        uid new-fn)
   (expr-rename-fn
        (c$::dirabsdeclor-array-static1->size c$::dirabsdeclor)
        uid new-fn))
  :array-static2
  (c$::dirabsdeclor-array-static2
   (dirabsdeclor-option-rename-fn
        (c$::dirabsdeclor-array-static2->declor? c$::dirabsdeclor)
        uid new-fn)
   (typequal/attribspec-list-rename-fn
        (c$::dirabsdeclor-array-static2->qualspecs c$::dirabsdeclor)
        uid new-fn)
   (expr-rename-fn
        (c$::dirabsdeclor-array-static2->size c$::dirabsdeclor)
        uid new-fn))
  :array-star
  (dirabsdeclor-array-star
       (dirabsdeclor-option-rename-fn
            (c$::dirabsdeclor-array-star->declor? c$::dirabsdeclor)
            uid new-fn))
  :function
  (c$::dirabsdeclor-function
       (dirabsdeclor-option-rename-fn
            (c$::dirabsdeclor-function->declor? c$::dirabsdeclor)
            uid new-fn)
       (param-declon-list-rename-fn
            (c$::dirabsdeclor-function->params c$::dirabsdeclor)
            uid new-fn)
       (c$::dirabsdeclor-function->ellipsis c$::dirabsdeclor))))

Function: dirabsdeclor-option-rename-fn

(defun dirabsdeclor-option-rename-fn
       (c$::dirabsdeclor-option uid new-fn)
 (declare
   (xargs :guard (and (dirabsdeclor-optionp c$::dirabsdeclor-option)
                      (c$::uidp uid)
                      (identp new-fn))))
 (dirabsdeclor-option-case
  c$::dirabsdeclor-option
  :some
  (dirabsdeclor-fix
    (dirabsdeclor-rename-fn
         (c$::dirabsdeclor-option-some->val c$::dirabsdeclor-option)
         uid new-fn))
  :none nil))

Function: param-declon-rename-fn

(defun param-declon-rename-fn (param-declon uid new-fn)
 (declare (xargs :guard (and (param-declonp param-declon)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable param-declon uid new-fn))
 (param-declon
    (decl-spec-list-rename-fn (c$::param-declon->specs param-declon)
                              uid new-fn)
    (param-declor-rename-fn (c$::param-declon->declor param-declon)
                            uid new-fn)
    (attrib-spec-list-rename-fn
         (c$::param-declon->attribs param-declon)
         uid new-fn)))

Function: param-declon-list-rename-fn

(defun param-declon-list-rename-fn
       (c$::param-declon-list uid new-fn)
  (declare
       (xargs :guard (and (param-declon-listp c$::param-declon-list)
                          (c$::uidp uid)
                          (identp new-fn))))
  (if (endp c$::param-declon-list)
      nil
    (cons (param-declon-rename-fn (car c$::param-declon-list)
                                  uid new-fn)
          (param-declon-list-rename-fn (cdr c$::param-declon-list)
                                       uid new-fn))))

Function: param-declor-rename-fn

(defun param-declor-rename-fn (c$::param-declor uid new-fn)
 (declare (xargs :guard (and (param-declorp c$::param-declor)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::param-declor uid new-fn))
 (param-declor-case
  c$::param-declor
  :nonabstract
  (c$::param-declor-nonabstract
       (declor-rename-fn
            (param-declor-nonabstract->declor c$::param-declor)
            uid new-fn)
       (c$::param-declor-nonabstract->info c$::param-declor))
  :abstract
  (param-declor-abstract
       (absdeclor-rename-fn
            (c$::param-declor-abstract->declor c$::param-declor)
            uid new-fn))
  :none (param-declor-fix c$::param-declor)
  :ambig (c$::param-declor-ambig
              (amb-declor/absdeclor-rename-fn
                   (c$::param-declor-ambig->declor c$::param-declor)
                   uid new-fn))))

Function: tyname-rename-fn

(defun tyname-rename-fn (tyname uid new-fn)
  (declare (xargs :guard (and (tynamep tyname)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable tyname uid new-fn))
  (tyname (spec/qual-list-rename-fn (c$::tyname->specquals tyname)
                                    uid new-fn)
          (absdeclor-option-rename-fn (c$::tyname->declor? tyname)
                                      uid new-fn)
          (tyname->info tyname)))

Function: struni-spec-rename-fn

(defun struni-spec-rename-fn (struni-spec uid new-fn)
 (declare (xargs :guard (and (struni-specp struni-spec)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable struni-spec uid new-fn))
 (struni-spec
  (attrib-spec-list-rename-fn (c$::struni-spec->attribs struni-spec)
                              uid new-fn)
  (c$::struni-spec->name? struni-spec)
  (struct-declon-list-rename-fn
       (c$::struni-spec->members struni-spec)
       uid new-fn)))

Function: struct-declon-rename-fn

(defun struct-declon-rename-fn (c$::struct-declon uid new-fn)
 (declare (xargs :guard (and (struct-declonp c$::struct-declon)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::struct-declon uid new-fn))
 (struct-declon-case
  c$::struct-declon
  :member
  (c$::struct-declon-member
       (c$::struct-declon-member->extension c$::struct-declon)
       (spec/qual-list-rename-fn
            (c$::struct-declon-member->specquals c$::struct-declon)
            uid new-fn)
       (struct-declor-list-rename-fn
            (c$::struct-declon-member->declors c$::struct-declon)
            uid new-fn)
       (attrib-spec-list-rename-fn
            (c$::struct-declon-member->attribs c$::struct-declon)
            uid new-fn))
  :statassert
  (struct-declon-statassert
       (statassert-rename-fn
            (c$::struct-declon-statassert->unwrap c$::struct-declon)
            uid new-fn))
  :empty (struct-declon-fix c$::struct-declon)))

Function: struct-declon-list-rename-fn

(defun struct-declon-list-rename-fn
       (c$::struct-declon-list uid new-fn)
 (declare
     (xargs :guard (and (struct-declon-listp c$::struct-declon-list)
                        (c$::uidp uid)
                        (identp new-fn))))
 (if (endp c$::struct-declon-list)
     nil
   (cons (struct-declon-rename-fn (car c$::struct-declon-list)
                                  uid new-fn)
         (struct-declon-list-rename-fn (cdr c$::struct-declon-list)
                                       uid new-fn))))

Function: struct-declor-rename-fn

(defun struct-declor-rename-fn (struct-declor uid new-fn)
  (declare (xargs :guard (and (struct-declorp struct-declor)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable struct-declor uid new-fn))
  (struct-declor (declor-option-rename-fn
                      (c$::struct-declor->declor? struct-declor)
                      uid new-fn)
                 (const-expr-option-rename-fn
                      (c$::struct-declor->expr? struct-declor)
                      uid new-fn)))

Function: struct-declor-list-rename-fn

(defun struct-declor-list-rename-fn
       (c$::struct-declor-list uid new-fn)
 (declare
     (xargs :guard (and (struct-declor-listp c$::struct-declor-list)
                        (c$::uidp uid)
                        (identp new-fn))))
 (if (endp c$::struct-declor-list)
     nil
   (cons (struct-declor-rename-fn (car c$::struct-declor-list)
                                  uid new-fn)
         (struct-declor-list-rename-fn (cdr c$::struct-declor-list)
                                       uid new-fn))))

Function: enum-spec-rename-fn

(defun enum-spec-rename-fn (enum-spec uid new-fn)
  (declare (xargs :guard (and (enum-specp enum-spec)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable enum-spec uid new-fn))
  (enum-spec (c$::enum-spec->name enum-spec)
             (enumer-list-rename-fn (c$::enum-spec->list enum-spec)
                                    uid new-fn)
             (c$::enum-spec->final-comma enum-spec)))

Function: enumer-rename-fn

(defun enumer-rename-fn (enumer uid new-fn)
  (declare (xargs :guard (and (enumerp enumer)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable enumer uid new-fn))
  (enumer (c$::enumer->name enumer)
          (const-expr-option-rename-fn (c$::enumer->value enumer)
                                       uid new-fn)))

Function: enumer-list-rename-fn

(defun enumer-list-rename-fn (c$::enumer-list uid new-fn)
  (declare (xargs :guard (and (enumer-listp c$::enumer-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::enumer-list)
      nil
    (cons (enumer-rename-fn (car c$::enumer-list)
                            uid new-fn)
          (enumer-list-rename-fn (cdr c$::enumer-list)
                                 uid new-fn))))

Function: statassert-rename-fn

(defun statassert-rename-fn (statassert uid new-fn)
 (declare (xargs :guard (and (statassertp statassert)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable statassert uid new-fn))
 (statassert (const-expr-rename-fn (c$::statassert->test statassert)
                                   uid new-fn)
             (c$::statassert->message statassert)))

Function: attrib-rename-fn

(defun attrib-rename-fn (c$::attrib uid new-fn)
 (declare (xargs :guard (and (c$::attribp c$::attrib)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::attrib uid new-fn))
 (c$::attrib-case
  c$::attrib
  :name-only (c$::attrib-fix c$::attrib)
  :name-param
  (c$::attrib-name-param
      (c$::attrib-name-param->name c$::attrib)
      (expr-list-rename-fn (c$::attrib-name-param->param c$::attrib)
                           uid new-fn))))

Function: attrib-list-rename-fn

(defun attrib-list-rename-fn (c$::attrib-list uid new-fn)
  (declare (xargs :guard (and (c$::attrib-listp c$::attrib-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::attrib-list)
      nil
    (cons (attrib-rename-fn (car c$::attrib-list)
                            uid new-fn)
          (attrib-list-rename-fn (cdr c$::attrib-list)
                                 uid new-fn))))

Function: attrib-spec-rename-fn

(defun attrib-spec-rename-fn (c$::attrib-spec uid new-fn)
 (declare (xargs :guard (and (c$::attrib-specp c$::attrib-spec)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::attrib-spec uid new-fn))
 (c$::attrib-spec
   (c$::attrib-spec->uscores c$::attrib-spec)
   (attrib-list-rename-fn (c$::attrib-spec->attribs c$::attrib-spec)
                          uid new-fn)))

Function: attrib-spec-list-rename-fn

(defun attrib-spec-list-rename-fn (c$::attrib-spec-list uid new-fn)
  (declare
       (xargs :guard (and (attrib-spec-listp c$::attrib-spec-list)
                          (c$::uidp uid)
                          (identp new-fn))))
  (if (endp c$::attrib-spec-list)
      nil
    (cons (attrib-spec-rename-fn (car c$::attrib-spec-list)
                                 uid new-fn)
          (attrib-spec-list-rename-fn (cdr c$::attrib-spec-list)
                                      uid new-fn))))

Function: initdeclor-rename-fn

(defun initdeclor-rename-fn (initdeclor uid new-fn)
 (declare (xargs :guard (and (initdeclorp initdeclor)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable initdeclor uid new-fn))
 (initdeclor
    (declor-rename-fn (initdeclor->declor initdeclor)
                      uid new-fn)
    (c$::initdeclor->asm? initdeclor)
    (attrib-spec-list-rename-fn (c$::initdeclor->attribs initdeclor)
                                uid new-fn)
    (initer-option-rename-fn (initdeclor->init? initdeclor)
                             uid new-fn)
    (c$::initdeclor->info initdeclor)))

Function: initdeclor-list-rename-fn

(defun initdeclor-list-rename-fn (c$::initdeclor-list uid new-fn)
  (declare (xargs :guard (and (initdeclor-listp c$::initdeclor-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::initdeclor-list)
      nil
    (cons (initdeclor-rename-fn (car c$::initdeclor-list)
                                uid new-fn)
          (initdeclor-list-rename-fn (cdr c$::initdeclor-list)
                                     uid new-fn))))

Function: decl-rename-fn

(defun decl-rename-fn (decl uid new-fn)
 (declare (xargs :guard (and (declp decl)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable decl uid new-fn))
 (decl-case
    decl
    :decl
    (c$::decl-decl (decl-decl->extension decl)
                   (decl-spec-list-rename-fn (decl-decl->specs decl)
                                             uid new-fn)
                   (initdeclor-list-rename-fn (decl-decl->init decl)
                                              uid new-fn))
    :statassert
    (decl-statassert
         (statassert-rename-fn (c$::decl-statassert->unwrap decl)
                               uid new-fn))))

Function: decl-list-rename-fn

(defun decl-list-rename-fn (c$::decl-list uid new-fn)
  (declare (xargs :guard (and (decl-listp c$::decl-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::decl-list)
      nil
    (cons (decl-rename-fn (car c$::decl-list)
                          uid new-fn)
          (decl-list-rename-fn (cdr c$::decl-list)
                               uid new-fn))))

Function: label-rename-fn

(defun label-rename-fn (c$::label uid new-fn)
 (declare (xargs :guard (and (labelp c$::label)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::label uid new-fn))
 (label-case
  c$::label
  :name
  (c$::label-name
     (c$::label-name->name c$::label)
     (attrib-spec-list-rename-fn (c$::label-name->attribs c$::label)
                                 uid new-fn))
  :casexpr
  (c$::label-casexpr
       (const-expr-rename-fn (c$::label-casexpr->expr c$::label)
                             uid new-fn)
       (const-expr-option-rename-fn
            (c$::label-casexpr->range? c$::label)
            uid new-fn))
  :default (label-fix c$::label)))

Function: asm-output-rename-fn

(defun asm-output-rename-fn (c$::asm-output uid new-fn)
  (declare (xargs :guard (and (c$::asm-outputp c$::asm-output)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable c$::asm-output uid new-fn))
  (c$::asm-output
       (c$::asm-output->name c$::asm-output)
       (c$::asm-output->constraint c$::asm-output)
       (expr-rename-fn (c$::asm-output->lvalue c$::asm-output)
                       uid new-fn)))

Function: asm-output-list-rename-fn

(defun asm-output-list-rename-fn (c$::asm-output-list uid new-fn)
  (declare
       (xargs :guard (and (c$::asm-output-listp c$::asm-output-list)
                          (c$::uidp uid)
                          (identp new-fn))))
  (if (endp c$::asm-output-list)
      nil
    (cons (asm-output-rename-fn (car c$::asm-output-list)
                                uid new-fn)
          (asm-output-list-rename-fn (cdr c$::asm-output-list)
                                     uid new-fn))))

Function: asm-input-rename-fn

(defun asm-input-rename-fn (c$::asm-input uid new-fn)
  (declare (xargs :guard (and (c$::asm-inputp c$::asm-input)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable c$::asm-input uid new-fn))
  (c$::asm-input
       (c$::asm-input->name c$::asm-input)
       (c$::asm-input->constraint c$::asm-input)
       (expr-rename-fn (c$::asm-input->rvalue c$::asm-input)
                       uid new-fn)))

Function: asm-input-list-rename-fn

(defun asm-input-list-rename-fn (c$::asm-input-list uid new-fn)
  (declare
       (xargs :guard (and (c$::asm-input-listp c$::asm-input-list)
                          (c$::uidp uid)
                          (identp new-fn))))
  (if (endp c$::asm-input-list)
      nil
    (cons (asm-input-rename-fn (car c$::asm-input-list)
                               uid new-fn)
          (asm-input-list-rename-fn (cdr c$::asm-input-list)
                                    uid new-fn))))

Function: asm-stmt-rename-fn

(defun asm-stmt-rename-fn (c$::asm-stmt uid new-fn)
 (declare (xargs :guard (and (c$::asm-stmtp c$::asm-stmt)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::asm-stmt uid new-fn))
 (c$::asm-stmt
     (c$::asm-stmt->uscores c$::asm-stmt)
     (c$::asm-stmt->quals c$::asm-stmt)
     (c$::asm-stmt->template c$::asm-stmt)
     (c$::asm-stmt->num-colons c$::asm-stmt)
     (asm-output-list-rename-fn (c$::asm-stmt->outputs c$::asm-stmt)
                                uid new-fn)
     (asm-input-list-rename-fn (c$::asm-stmt->inputs c$::asm-stmt)
                               uid new-fn)
     (c$::asm-stmt->clobbers c$::asm-stmt)
     (c$::asm-stmt->labels c$::asm-stmt)))

Function: stmt-rename-fn

(defun stmt-rename-fn (c$::stmt uid new-fn)
 (declare (xargs :guard (and (stmtp c$::stmt)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::stmt uid new-fn))
 (stmt-case
  c$::stmt
  :labeled (c$::stmt-labeled
                (label-rename-fn (c$::stmt-labeled->label c$::stmt)
                                 uid new-fn)
                (stmt-rename-fn (c$::stmt-labeled->stmt c$::stmt)
                                uid new-fn))
  :compound
  (stmt-compound (comp-stmt-rename-fn (stmt-compound->stmt c$::stmt)
                                      uid new-fn))
  :expr (c$::stmt-expr
             (expr-option-rename-fn (c$::stmt-expr->expr? c$::stmt)
                                    uid new-fn)
             (c$::stmt-expr->info c$::stmt))
  :if (c$::stmt-if (expr-rename-fn (c$::stmt-if->test c$::stmt)
                                   uid new-fn)
                   (stmt-rename-fn (c$::stmt-if->then c$::stmt)
                                   uid new-fn))
  :ifelse
  (c$::stmt-ifelse (expr-rename-fn (c$::stmt-ifelse->test c$::stmt)
                                   uid new-fn)
                   (stmt-rename-fn (c$::stmt-ifelse->then c$::stmt)
                                   uid new-fn)
                   (stmt-rename-fn (c$::stmt-ifelse->else c$::stmt)
                                   uid new-fn))
  :switch (c$::stmt-switch
               (expr-rename-fn (c$::stmt-switch->target c$::stmt)
                               uid new-fn)
               (stmt-rename-fn (c$::stmt-switch->body c$::stmt)
                               uid new-fn))
  :while
  (c$::stmt-while (expr-rename-fn (c$::stmt-while->test c$::stmt)
                                  uid new-fn)
                  (stmt-rename-fn (c$::stmt-while->body c$::stmt)
                                  uid new-fn))
  :dowhile (c$::stmt-dowhile
                (stmt-rename-fn (c$::stmt-dowhile->body c$::stmt)
                                uid new-fn)
                (expr-rename-fn (c$::stmt-dowhile->test c$::stmt)
                                uid new-fn))
  :for-expr
  (c$::stmt-for-expr
       (expr-option-rename-fn (c$::stmt-for-expr->init c$::stmt)
                              uid new-fn)
       (expr-option-rename-fn (c$::stmt-for-expr->test c$::stmt)
                              uid new-fn)
       (expr-option-rename-fn (c$::stmt-for-expr->next c$::stmt)
                              uid new-fn)
       (stmt-rename-fn (c$::stmt-for-expr->body c$::stmt)
                       uid new-fn))
  :for-decl
  (c$::stmt-for-decl
       (decl-rename-fn (c$::stmt-for-decl->init c$::stmt)
                       uid new-fn)
       (expr-option-rename-fn (c$::stmt-for-decl->test c$::stmt)
                              uid new-fn)
       (expr-option-rename-fn (c$::stmt-for-decl->next c$::stmt)
                              uid new-fn)
       (stmt-rename-fn (c$::stmt-for-decl->body c$::stmt)
                       uid new-fn))
  :for-ambig
  (c$::stmt-for-ambig
       (amb-decl/stmt-rename-fn (c$::stmt-for-ambig->init c$::stmt)
                                uid new-fn)
       (expr-option-rename-fn (c$::stmt-for-ambig->test c$::stmt)
                              uid new-fn)
       (expr-option-rename-fn (c$::stmt-for-ambig->next c$::stmt)
                              uid new-fn)
       (stmt-rename-fn (c$::stmt-for-ambig->body c$::stmt)
                       uid new-fn))
  :goto (stmt-fix c$::stmt)
  :gotoe
  (stmt-gotoe (expr-rename-fn (c$::stmt-gotoe->label c$::stmt)
                              uid new-fn))
  :continue (stmt-fix c$::stmt)
  :break (stmt-fix c$::stmt)
  :return
  (c$::stmt-return
       (expr-option-rename-fn (c$::stmt-return->expr? c$::stmt)
                              uid new-fn)
       (c$::stmt-return->info c$::stmt))
  :asm
  (c$::stmt-asm (asm-stmt-rename-fn (c$::stmt-asm->unwrap c$::stmt)
                                    uid new-fn))))

Function: comp-stmt-rename-fn

(defun comp-stmt-rename-fn (comp-stmt uid new-fn)
  (declare (xargs :guard (and (comp-stmtp comp-stmt)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable comp-stmt uid new-fn))
  (comp-stmt (comp-stmt->labels comp-stmt)
             (block-item-list-rename-fn (comp-stmt->items comp-stmt)
                                        uid new-fn)))

Function: block-item-rename-fn

(defun block-item-rename-fn (c$::block-item uid new-fn)
 (declare (xargs :guard (and (block-itemp c$::block-item)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::block-item uid new-fn))
 (block-item-case
     c$::block-item
     :decl
     (c$::block-item-decl
          (decl-rename-fn (c$::block-item-decl->decl c$::block-item)
                          uid new-fn)
          (c$::block-item-decl->info c$::block-item))
     :stmt
     (c$::block-item-stmt
          (stmt-rename-fn (c$::block-item-stmt->stmt c$::block-item)
                          uid new-fn)
          (c$::block-item-stmt->info c$::block-item))
     :ambig (c$::block-item-ambig
                 (amb-decl/stmt-rename-fn
                      (c$::block-item-ambig->unwrap c$::block-item)
                      uid new-fn))))

Function: block-item-list-rename-fn

(defun block-item-list-rename-fn (c$::block-item-list uid new-fn)
  (declare (xargs :guard (and (block-item-listp c$::block-item-list)
                              (c$::uidp uid)
                              (identp new-fn))))
  (if (endp c$::block-item-list)
      nil
    (cons (block-item-rename-fn (car c$::block-item-list)
                                uid new-fn)
          (block-item-list-rename-fn (cdr c$::block-item-list)
                                     uid new-fn))))

Function: amb-expr/tyname-rename-fn

(defun amb-expr/tyname-rename-fn (c$::amb-expr/tyname uid new-fn)
 (declare
      (xargs :guard (and (c$::amb-expr/tyname-p c$::amb-expr/tyname)
                         (c$::uidp uid)
                         (identp new-fn))))
 (declare (ignorable c$::amb-expr/tyname uid new-fn))
 (c$::amb-expr/tyname
     (expr-rename-fn (c$::amb-expr/tyname->expr c$::amb-expr/tyname)
                     uid new-fn)
     (tyname-rename-fn
          (c$::amb-expr/tyname->tyname c$::amb-expr/tyname)
          uid new-fn)))

Function: amb-declor/absdeclor-rename-fn

(defun amb-declor/absdeclor-rename-fn
       (c$::amb-declor/absdeclor uid new-fn)
 (declare
  (xargs
   :guard (and (c$::amb-declor/absdeclor-p c$::amb-declor/absdeclor)
               (c$::uidp uid)
               (identp new-fn))))
 (declare (ignorable c$::amb-declor/absdeclor uid new-fn))
 (c$::amb-declor/absdeclor
  (declor-rename-fn
       (c$::amb-declor/absdeclor->declor c$::amb-declor/absdeclor)
       uid new-fn)
  (absdeclor-rename-fn
      (c$::amb-declor/absdeclor->absdeclor c$::amb-declor/absdeclor)
      uid new-fn)))

Function: amb-decl/stmt-rename-fn

(defun amb-decl/stmt-rename-fn (c$::amb-decl/stmt uid new-fn)
 (declare (xargs :guard (and (c$::amb-decl/stmt-p c$::amb-decl/stmt)
                             (c$::uidp uid)
                             (identp new-fn))))
 (declare (ignorable c$::amb-decl/stmt uid new-fn))
 (c$::amb-decl/stmt
      (decl-rename-fn (c$::amb-decl/stmt->decl c$::amb-decl/stmt)
                      uid new-fn)
      (expr-rename-fn (c$::amb-decl/stmt->stmt c$::amb-decl/stmt)
                      uid new-fn)))

Theorem: return-type-of-expr-rename-fn.result

(defthm return-type-of-expr-rename-fn.result
  (b* ((fty::?result (expr-rename-fn c$::expr uid new-fn)))
    (exprp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-expr-list-rename-fn.result

(defthm return-type-of-expr-list-rename-fn.result
 (b* ((fty::?result (expr-list-rename-fn c$::expr-list uid new-fn)))
   (expr-listp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-expr-option-rename-fn.result

(defthm return-type-of-expr-option-rename-fn.result
  (b* ((fty::?result
            (expr-option-rename-fn c$::expr-option uid new-fn)))
    (expr-optionp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-const-expr-rename-fn.result

(defthm return-type-of-const-expr-rename-fn.result
  (b* ((fty::?result (const-expr-rename-fn const-expr uid new-fn)))
    (const-exprp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-const-expr-option-rename-fn.result

(defthm return-type-of-const-expr-option-rename-fn.result
 (b*
  ((fty::?result
    (const-expr-option-rename-fn c$::const-expr-option uid new-fn)))
  (const-expr-optionp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-genassoc-rename-fn.result

(defthm return-type-of-genassoc-rename-fn.result
  (b* ((fty::?result (genassoc-rename-fn c$::genassoc uid new-fn)))
    (genassocp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-genassoc-list-rename-fn.result

(defthm return-type-of-genassoc-list-rename-fn.result
  (b* ((fty::?result
            (genassoc-list-rename-fn c$::genassoc-list uid new-fn)))
    (genassoc-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-member-designor-rename-fn.result

(defthm return-type-of-member-designor-rename-fn.result
 (b*
  ((fty::?result
        (member-designor-rename-fn c$::member-designor uid new-fn)))
  (member-designorp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-type-spec-rename-fn.result

(defthm return-type-of-type-spec-rename-fn.result
 (b* ((fty::?result (type-spec-rename-fn c$::type-spec uid new-fn)))
   (type-specp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-spec/qual-rename-fn.result

(defthm return-type-of-spec/qual-rename-fn.result
 (b* ((fty::?result (spec/qual-rename-fn c$::spec/qual uid new-fn)))
   (spec/qual-p fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-spec/qual-list-rename-fn.result

(defthm return-type-of-spec/qual-list-rename-fn.result
  (b*
    ((fty::?result
          (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn)))
    (spec/qual-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-align-spec-rename-fn.result

(defthm return-type-of-align-spec-rename-fn.result
  (b*
   ((fty::?result (align-spec-rename-fn c$::align-spec uid new-fn)))
   (align-specp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-decl-spec-rename-fn.result

(defthm return-type-of-decl-spec-rename-fn.result
 (b* ((fty::?result (decl-spec-rename-fn c$::decl-spec uid new-fn)))
   (decl-specp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-decl-spec-list-rename-fn.result

(defthm return-type-of-decl-spec-list-rename-fn.result
  (b*
    ((fty::?result
          (decl-spec-list-rename-fn c$::decl-spec-list uid new-fn)))
    (decl-spec-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-typequal/attribspec-rename-fn.result

(defthm return-type-of-typequal/attribspec-rename-fn.result
  (b* ((fty::?result (typequal/attribspec-rename-fn
                          c$::typequal/attribspec uid new-fn)))
    (c$::typequal/attribspec-p fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-typequal/attribspec-list-rename-fn.result

(defthm return-type-of-typequal/attribspec-list-rename-fn.result
 (b*
  ((fty::?result
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid new-fn)))
  (c$::typequal/attribspec-listp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-typequal/attribspec-list-list-rename-fn.result

(defthm
      return-type-of-typequal/attribspec-list-list-rename-fn.result
  (b* ((fty::?result (typequal/attribspec-list-list-rename-fn
                          c$::typequal/attribspec-list-list
                          uid new-fn)))
    (typequal/attribspec-list-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-initer-rename-fn.result

(defthm return-type-of-initer-rename-fn.result
  (b* ((fty::?result (initer-rename-fn c$::initer uid new-fn)))
    (initerp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-initer-option-rename-fn.result

(defthm return-type-of-initer-option-rename-fn.result
  (b* ((fty::?result
            (initer-option-rename-fn c$::initer-option uid new-fn)))
    (initer-optionp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-desiniter-rename-fn.result

(defthm return-type-of-desiniter-rename-fn.result
  (b* ((fty::?result (desiniter-rename-fn desiniter uid new-fn)))
    (desiniterp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-desiniter-list-rename-fn.result

(defthm return-type-of-desiniter-list-rename-fn.result
  (b*
    ((fty::?result
          (desiniter-list-rename-fn c$::desiniter-list uid new-fn)))
    (desiniter-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-designor-rename-fn.result

(defthm return-type-of-designor-rename-fn.result
  (b* ((fty::?result (designor-rename-fn c$::designor uid new-fn)))
    (designorp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-designor-list-rename-fn.result

(defthm return-type-of-designor-list-rename-fn.result
  (b* ((fty::?result
            (designor-list-rename-fn c$::designor-list uid new-fn)))
    (designor-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-declor-rename-fn.result

(defthm return-type-of-declor-rename-fn.result
  (b* ((fty::?result (declor-rename-fn declor uid new-fn)))
    (declorp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-declor-option-rename-fn.result

(defthm return-type-of-declor-option-rename-fn.result
  (b* ((fty::?result
            (declor-option-rename-fn c$::declor-option uid new-fn)))
    (declor-optionp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-dirdeclor-rename-fn.result

(defthm return-type-of-dirdeclor-rename-fn.result
  (b* ((fty::?result (dirdeclor-rename-fn dirdeclor uid new-fn)))
    (dirdeclorp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-absdeclor-rename-fn.result

(defthm return-type-of-absdeclor-rename-fn.result
  (b* ((fty::?result (absdeclor-rename-fn absdeclor uid new-fn)))
    (absdeclorp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-absdeclor-option-rename-fn.result

(defthm return-type-of-absdeclor-option-rename-fn.result
 (b*
  ((fty::?result
      (absdeclor-option-rename-fn c$::absdeclor-option uid new-fn)))
  (absdeclor-optionp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-dirabsdeclor-rename-fn.result

(defthm return-type-of-dirabsdeclor-rename-fn.result
  (b* ((fty::?result
            (dirabsdeclor-rename-fn c$::dirabsdeclor uid new-fn)))
    (dirabsdeclorp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-dirabsdeclor-option-rename-fn.result

(defthm return-type-of-dirabsdeclor-option-rename-fn.result
  (b* ((fty::?result (dirabsdeclor-option-rename-fn
                          c$::dirabsdeclor-option uid new-fn)))
    (dirabsdeclor-optionp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-param-declon-rename-fn.result

(defthm return-type-of-param-declon-rename-fn.result
  (b*
   ((fty::?result (param-declon-rename-fn param-declon uid new-fn)))
   (param-declonp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-param-declon-list-rename-fn.result

(defthm return-type-of-param-declon-list-rename-fn.result
 (b*
  ((fty::?result
    (param-declon-list-rename-fn c$::param-declon-list uid new-fn)))
  (param-declon-listp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-param-declor-rename-fn.result

(defthm return-type-of-param-declor-rename-fn.result
  (b* ((fty::?result
            (param-declor-rename-fn c$::param-declor uid new-fn)))
    (param-declorp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-tyname-rename-fn.result

(defthm return-type-of-tyname-rename-fn.result
  (b* ((fty::?result (tyname-rename-fn tyname uid new-fn)))
    (tynamep fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-struni-spec-rename-fn.result

(defthm return-type-of-struni-spec-rename-fn.result
 (b* ((fty::?result (struni-spec-rename-fn struni-spec uid new-fn)))
   (struni-specp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-struct-declon-rename-fn.result

(defthm return-type-of-struct-declon-rename-fn.result
  (b* ((fty::?result
            (struct-declon-rename-fn c$::struct-declon uid new-fn)))
    (struct-declonp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-struct-declon-list-rename-fn.result

(defthm return-type-of-struct-declon-list-rename-fn.result
  (b* ((fty::?result (struct-declon-list-rename-fn
                          c$::struct-declon-list uid new-fn)))
    (struct-declon-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-struct-declor-rename-fn.result

(defthm return-type-of-struct-declor-rename-fn.result
  (b* ((fty::?result
            (struct-declor-rename-fn struct-declor uid new-fn)))
    (struct-declorp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-struct-declor-list-rename-fn.result

(defthm return-type-of-struct-declor-list-rename-fn.result
  (b* ((fty::?result (struct-declor-list-rename-fn
                          c$::struct-declor-list uid new-fn)))
    (struct-declor-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-enum-spec-rename-fn.result

(defthm return-type-of-enum-spec-rename-fn.result
  (b* ((fty::?result (enum-spec-rename-fn enum-spec uid new-fn)))
    (enum-specp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-enumer-rename-fn.result

(defthm return-type-of-enumer-rename-fn.result
  (b* ((fty::?result (enumer-rename-fn enumer uid new-fn)))
    (enumerp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-enumer-list-rename-fn.result

(defthm return-type-of-enumer-list-rename-fn.result
  (b* ((fty::?result
            (enumer-list-rename-fn c$::enumer-list uid new-fn)))
    (enumer-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-statassert-rename-fn.result

(defthm return-type-of-statassert-rename-fn.result
  (b* ((fty::?result (statassert-rename-fn statassert uid new-fn)))
    (statassertp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-attrib-rename-fn.result

(defthm return-type-of-attrib-rename-fn.result
  (b* ((fty::?result (attrib-rename-fn c$::attrib uid new-fn)))
    (c$::attribp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-attrib-list-rename-fn.result

(defthm return-type-of-attrib-list-rename-fn.result
  (b* ((fty::?result
            (attrib-list-rename-fn c$::attrib-list uid new-fn)))
    (c$::attrib-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-attrib-spec-rename-fn.result

(defthm return-type-of-attrib-spec-rename-fn.result
  (b* ((fty::?result
            (attrib-spec-rename-fn c$::attrib-spec uid new-fn)))
    (c$::attrib-specp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-attrib-spec-list-rename-fn.result

(defthm return-type-of-attrib-spec-list-rename-fn.result
 (b*
  ((fty::?result
      (attrib-spec-list-rename-fn c$::attrib-spec-list uid new-fn)))
  (attrib-spec-listp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-initdeclor-rename-fn.result

(defthm return-type-of-initdeclor-rename-fn.result
  (b* ((fty::?result (initdeclor-rename-fn initdeclor uid new-fn)))
    (initdeclorp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-initdeclor-list-rename-fn.result

(defthm return-type-of-initdeclor-list-rename-fn.result
 (b*
  ((fty::?result
        (initdeclor-list-rename-fn c$::initdeclor-list uid new-fn)))
  (initdeclor-listp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-decl-rename-fn.result

(defthm return-type-of-decl-rename-fn.result
  (b* ((fty::?result (decl-rename-fn decl uid new-fn)))
    (declp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-decl-list-rename-fn.result

(defthm return-type-of-decl-list-rename-fn.result
 (b* ((fty::?result (decl-list-rename-fn c$::decl-list uid new-fn)))
   (decl-listp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-label-rename-fn.result

(defthm return-type-of-label-rename-fn.result
  (b* ((fty::?result (label-rename-fn c$::label uid new-fn)))
    (labelp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-asm-output-rename-fn.result

(defthm return-type-of-asm-output-rename-fn.result
  (b*
   ((fty::?result (asm-output-rename-fn c$::asm-output uid new-fn)))
   (c$::asm-outputp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-asm-output-list-rename-fn.result

(defthm return-type-of-asm-output-list-rename-fn.result
 (b*
  ((fty::?result
        (asm-output-list-rename-fn c$::asm-output-list uid new-fn)))
  (c$::asm-output-listp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-asm-input-rename-fn.result

(defthm return-type-of-asm-input-rename-fn.result
 (b* ((fty::?result (asm-input-rename-fn c$::asm-input uid new-fn)))
   (c$::asm-inputp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-asm-input-list-rename-fn.result

(defthm return-type-of-asm-input-list-rename-fn.result
  (b*
    ((fty::?result
          (asm-input-list-rename-fn c$::asm-input-list uid new-fn)))
    (c$::asm-input-listp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-asm-stmt-rename-fn.result

(defthm return-type-of-asm-stmt-rename-fn.result
  (b* ((fty::?result (asm-stmt-rename-fn c$::asm-stmt uid new-fn)))
    (c$::asm-stmtp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-stmt-rename-fn.result

(defthm return-type-of-stmt-rename-fn.result
  (b* ((fty::?result (stmt-rename-fn c$::stmt uid new-fn)))
    (stmtp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-comp-stmt-rename-fn.result

(defthm return-type-of-comp-stmt-rename-fn.result
  (b* ((fty::?result (comp-stmt-rename-fn comp-stmt uid new-fn)))
    (comp-stmtp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-block-item-rename-fn.result

(defthm return-type-of-block-item-rename-fn.result
  (b*
   ((fty::?result (block-item-rename-fn c$::block-item uid new-fn)))
   (block-itemp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-block-item-list-rename-fn.result

(defthm return-type-of-block-item-list-rename-fn.result
 (b*
  ((fty::?result
        (block-item-list-rename-fn c$::block-item-list uid new-fn)))
  (block-item-listp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-amb-expr/tyname-rename-fn.result

(defthm return-type-of-amb-expr/tyname-rename-fn.result
 (b*
  ((fty::?result
        (amb-expr/tyname-rename-fn c$::amb-expr/tyname uid new-fn)))
  (c$::amb-expr/tyname-p fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-amb-declor/absdeclor-rename-fn.result

(defthm return-type-of-amb-declor/absdeclor-rename-fn.result
  (b* ((fty::?result (amb-declor/absdeclor-rename-fn
                          c$::amb-declor/absdeclor uid new-fn)))
    (c$::amb-declor/absdeclor-p fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-amb-decl/stmt-rename-fn.result

(defthm return-type-of-amb-decl/stmt-rename-fn.result
  (b* ((fty::?result
            (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid new-fn)))
    (c$::amb-decl/stmt-p fty::result))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: expr-option-rename-fn-under-iff

(defthm expr-option-rename-fn-under-iff
  (iff (expr-option-rename-fn c$::expr-option uid new-fn)
       c$::expr-option))

Theorem: const-expr-option-rename-fn-under-iff

(defthm const-expr-option-rename-fn-under-iff
 (iff (const-expr-option-rename-fn c$::const-expr-option uid new-fn)
      c$::const-expr-option))

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))))

Theorem: spec/qual-list-rename-fn-type-prescription

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

Theorem: spec/qual-list-rename-fn-when-atom

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

Theorem: spec/qual-list-rename-fn-of-cons

(defthm spec/qual-list-rename-fn-of-cons
 (equal
   (spec/qual-list-rename-fn (cons c$::spec/qual c$::spec/qual-list)
                             uid new-fn)
   (cons (spec/qual-rename-fn c$::spec/qual uid new-fn)
         (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn))))

Theorem: spec/qual-list-rename-fn-of-append

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

Theorem: consp-of-spec/qual-list-rename-fn

(defthm consp-of-spec/qual-list-rename-fn
 (equal
    (consp (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn))
    (consp c$::spec/qual-list)))

Theorem: len-of-spec/qual-list-rename-fn

(defthm len-of-spec/qual-list-rename-fn
 (equal
      (len (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn))
      (len c$::spec/qual-list)))

Theorem: nth-of-spec/qual-list-rename-fn

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

Theorem: spec/qual-list-rename-fn-of-revappend

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

Theorem: spec/qual-list-rename-fn-of-reverse

(defthm spec/qual-list-rename-fn-of-reverse
 (equal
    (spec/qual-list-rename-fn (reverse c$::spec/qual-list)
                              uid new-fn)
    (reverse
         (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn))))

Theorem: decl-spec-list-rename-fn-type-prescription

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

Theorem: decl-spec-list-rename-fn-when-atom

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

Theorem: decl-spec-list-rename-fn-of-cons

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

Theorem: decl-spec-list-rename-fn-of-append

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

Theorem: consp-of-decl-spec-list-rename-fn

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

Theorem: len-of-decl-spec-list-rename-fn

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

Theorem: nth-of-decl-spec-list-rename-fn

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

Theorem: decl-spec-list-rename-fn-of-revappend

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

Theorem: decl-spec-list-rename-fn-of-reverse

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

Theorem: typequal/attribspec-list-rename-fn-type-prescription

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

Theorem: typequal/attribspec-list-rename-fn-when-atom

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

Theorem: typequal/attribspec-list-rename-fn-of-cons

(defthm typequal/attribspec-list-rename-fn-of-cons
 (equal
  (typequal/attribspec-list-rename-fn
       (cons c$::typequal/attribspec
             c$::typequal/attribspec-list)
       uid new-fn)
  (cons
    (typequal/attribspec-rename-fn
         c$::typequal/attribspec uid new-fn)
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid new-fn))))

Theorem: typequal/attribspec-list-rename-fn-of-append

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

Theorem: consp-of-typequal/attribspec-list-rename-fn

(defthm consp-of-typequal/attribspec-list-rename-fn
 (equal
  (consp
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid new-fn))
  (consp c$::typequal/attribspec-list)))

Theorem: len-of-typequal/attribspec-list-rename-fn

(defthm len-of-typequal/attribspec-list-rename-fn
 (equal
  (len
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid new-fn))
  (len c$::typequal/attribspec-list)))

Theorem: nth-of-typequal/attribspec-list-rename-fn

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

Theorem: typequal/attribspec-list-rename-fn-of-revappend

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

Theorem: typequal/attribspec-list-rename-fn-of-reverse

(defthm typequal/attribspec-list-rename-fn-of-reverse
 (equal
  (typequal/attribspec-list-rename-fn
       (reverse c$::typequal/attribspec-list)
       uid new-fn)
  (reverse
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid new-fn))))

Theorem: typequal/attribspec-list-list-rename-fn-type-prescription

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

Theorem: typequal/attribspec-list-list-rename-fn-when-atom

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

Theorem: typequal/attribspec-list-list-rename-fn-of-cons

(defthm typequal/attribspec-list-list-rename-fn-of-cons
  (equal (typequal/attribspec-list-list-rename-fn
              (cons c$::typequal/attribspec-list
                    c$::typequal/attribspec-list-list)
              uid new-fn)
         (cons (typequal/attribspec-list-rename-fn
                    c$::typequal/attribspec-list uid new-fn)
               (typequal/attribspec-list-list-rename-fn
                    c$::typequal/attribspec-list-list
                    uid new-fn))))

Theorem: typequal/attribspec-list-list-rename-fn-of-append

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

Theorem: consp-of-typequal/attribspec-list-list-rename-fn

(defthm consp-of-typequal/attribspec-list-list-rename-fn
  (equal (consp (typequal/attribspec-list-list-rename-fn
                     c$::typequal/attribspec-list-list
                     uid new-fn))
         (consp c$::typequal/attribspec-list-list)))

Theorem: len-of-typequal/attribspec-list-list-rename-fn

(defthm len-of-typequal/attribspec-list-list-rename-fn
  (equal (len (typequal/attribspec-list-list-rename-fn
                   c$::typequal/attribspec-list-list
                   uid new-fn))
         (len c$::typequal/attribspec-list-list)))

Theorem: nth-of-typequal/attribspec-list-list-rename-fn

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

Theorem: typequal/attribspec-list-list-rename-fn-of-revappend

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

Theorem: typequal/attribspec-list-list-rename-fn-of-reverse

(defthm typequal/attribspec-list-list-rename-fn-of-reverse
  (equal (typequal/attribspec-list-list-rename-fn
              (reverse c$::typequal/attribspec-list-list)
              uid new-fn)
         (reverse (typequal/attribspec-list-list-rename-fn
                       c$::typequal/attribspec-list-list
                       uid new-fn))))

Theorem: initer-option-rename-fn-under-iff

(defthm initer-option-rename-fn-under-iff
  (iff (initer-option-rename-fn c$::initer-option uid new-fn)
       c$::initer-option))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: declor-option-rename-fn-under-iff

(defthm declor-option-rename-fn-under-iff
  (iff (declor-option-rename-fn c$::declor-option uid new-fn)
       c$::declor-option))

Theorem: absdeclor-option-rename-fn-under-iff

(defthm absdeclor-option-rename-fn-under-iff
  (iff (absdeclor-option-rename-fn c$::absdeclor-option uid new-fn)
       c$::absdeclor-option))

Theorem: dirabsdeclor-option-rename-fn-under-iff

(defthm dirabsdeclor-option-rename-fn-under-iff
 (iff
  (dirabsdeclor-option-rename-fn c$::dirabsdeclor-option uid new-fn)
  c$::dirabsdeclor-option))

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))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: struct-declor-list-rename-fn-type-prescription

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

Theorem: struct-declor-list-rename-fn-when-atom

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

Theorem: struct-declor-list-rename-fn-of-cons

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

Theorem: struct-declor-list-rename-fn-of-append

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

Theorem: consp-of-struct-declor-list-rename-fn

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

Theorem: len-of-struct-declor-list-rename-fn

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

Theorem: nth-of-struct-declor-list-rename-fn

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

Theorem: struct-declor-list-rename-fn-of-revappend

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

Theorem: struct-declor-list-rename-fn-of-reverse

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

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))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: attrib-spec-list-rename-fn-type-prescription

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

Theorem: attrib-spec-list-rename-fn-when-atom

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

Theorem: attrib-spec-list-rename-fn-of-cons

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

Theorem: attrib-spec-list-rename-fn-of-append

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

Theorem: consp-of-attrib-spec-list-rename-fn

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

Theorem: len-of-attrib-spec-list-rename-fn

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

Theorem: nth-of-attrib-spec-list-rename-fn

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

Theorem: attrib-spec-list-rename-fn-of-revappend

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

Theorem: attrib-spec-list-rename-fn-of-reverse

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

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))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: asm-output-list-rename-fn-type-prescription

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

Theorem: asm-output-list-rename-fn-when-atom

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

Theorem: asm-output-list-rename-fn-of-cons

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

Theorem: asm-output-list-rename-fn-of-append

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

Theorem: consp-of-asm-output-list-rename-fn

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

Theorem: len-of-asm-output-list-rename-fn

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

Theorem: nth-of-asm-output-list-rename-fn

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

Theorem: asm-output-list-rename-fn-of-revappend

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

Theorem: asm-output-list-rename-fn-of-reverse

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

Theorem: asm-input-list-rename-fn-type-prescription

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

Theorem: asm-input-list-rename-fn-when-atom

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

Theorem: asm-input-list-rename-fn-of-cons

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

Theorem: asm-input-list-rename-fn-of-append

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

Theorem: consp-of-asm-input-list-rename-fn

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

Theorem: len-of-asm-input-list-rename-fn

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

Theorem: nth-of-asm-input-list-rename-fn

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

Theorem: asm-input-list-rename-fn-of-revappend

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

Theorem: asm-input-list-rename-fn-of-reverse

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

Theorem: block-item-list-rename-fn-type-prescription

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

Theorem: block-item-list-rename-fn-when-atom

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

Theorem: block-item-list-rename-fn-of-cons

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

Theorem: block-item-list-rename-fn-of-append

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

Theorem: consp-of-block-item-list-rename-fn

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

Theorem: len-of-block-item-list-rename-fn

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

Theorem: nth-of-block-item-list-rename-fn

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

Theorem: block-item-list-rename-fn-of-revappend

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

Theorem: block-item-list-rename-fn-of-reverse

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

Theorem: expr-rename-fn-of-expr-fix-expr

(defthm expr-rename-fn-of-expr-fix-expr
  (equal (expr-rename-fn (expr-fix c$::expr)
                         uid new-fn)
         (expr-rename-fn c$::expr uid new-fn)))

Theorem: expr-rename-fn-of-uid-fix-uid

(defthm expr-rename-fn-of-uid-fix-uid
  (equal (expr-rename-fn c$::expr (c$::uid-fix uid)
                         new-fn)
         (expr-rename-fn c$::expr uid new-fn)))

Theorem: expr-rename-fn-of-ident-fix-new-fn

(defthm expr-rename-fn-of-ident-fix-new-fn
  (equal (expr-rename-fn c$::expr uid (ident-fix new-fn))
         (expr-rename-fn c$::expr uid new-fn)))

Theorem: expr-list-rename-fn-of-expr-list-fix-expr-list

(defthm expr-list-rename-fn-of-expr-list-fix-expr-list
  (equal (expr-list-rename-fn (expr-list-fix c$::expr-list)
                              uid new-fn)
         (expr-list-rename-fn c$::expr-list uid new-fn)))

Theorem: expr-list-rename-fn-of-uid-fix-uid

(defthm expr-list-rename-fn-of-uid-fix-uid
  (equal (expr-list-rename-fn c$::expr-list (c$::uid-fix uid)
                              new-fn)
         (expr-list-rename-fn c$::expr-list uid new-fn)))

Theorem: expr-list-rename-fn-of-ident-fix-new-fn

(defthm expr-list-rename-fn-of-ident-fix-new-fn
  (equal (expr-list-rename-fn c$::expr-list uid (ident-fix new-fn))
         (expr-list-rename-fn c$::expr-list uid new-fn)))

Theorem: expr-option-rename-fn-of-expr-option-fix-expr-option

(defthm expr-option-rename-fn-of-expr-option-fix-expr-option
  (equal (expr-option-rename-fn (expr-option-fix c$::expr-option)
                                uid new-fn)
         (expr-option-rename-fn c$::expr-option uid new-fn)))

Theorem: expr-option-rename-fn-of-uid-fix-uid

(defthm expr-option-rename-fn-of-uid-fix-uid
  (equal (expr-option-rename-fn c$::expr-option (c$::uid-fix uid)
                                new-fn)
         (expr-option-rename-fn c$::expr-option uid new-fn)))

Theorem: expr-option-rename-fn-of-ident-fix-new-fn

(defthm expr-option-rename-fn-of-ident-fix-new-fn
 (equal
      (expr-option-rename-fn c$::expr-option uid (ident-fix new-fn))
      (expr-option-rename-fn c$::expr-option uid new-fn)))

Theorem: const-expr-rename-fn-of-const-expr-fix-const-expr

(defthm const-expr-rename-fn-of-const-expr-fix-const-expr
  (equal (const-expr-rename-fn (c$::const-expr-fix const-expr)
                               uid new-fn)
         (const-expr-rename-fn const-expr uid new-fn)))

Theorem: const-expr-rename-fn-of-uid-fix-uid

(defthm const-expr-rename-fn-of-uid-fix-uid
  (equal (const-expr-rename-fn const-expr (c$::uid-fix uid)
                               new-fn)
         (const-expr-rename-fn const-expr uid new-fn)))

Theorem: const-expr-rename-fn-of-ident-fix-new-fn

(defthm const-expr-rename-fn-of-ident-fix-new-fn
  (equal (const-expr-rename-fn const-expr uid (ident-fix new-fn))
         (const-expr-rename-fn const-expr uid new-fn)))

Theorem: const-expr-option-rename-fn-of-const-expr-option-fix-const-expr-option

(defthm
 const-expr-option-rename-fn-of-const-expr-option-fix-const-expr-option
 (equal
    (const-expr-option-rename-fn
         (const-expr-option-fix c$::const-expr-option)
         uid new-fn)
    (const-expr-option-rename-fn c$::const-expr-option uid new-fn)))

Theorem: const-expr-option-rename-fn-of-uid-fix-uid

(defthm const-expr-option-rename-fn-of-uid-fix-uid
 (equal
    (const-expr-option-rename-fn
         c$::const-expr-option (c$::uid-fix uid)
         new-fn)
    (const-expr-option-rename-fn c$::const-expr-option uid new-fn)))

Theorem: const-expr-option-rename-fn-of-ident-fix-new-fn

(defthm const-expr-option-rename-fn-of-ident-fix-new-fn
 (equal
    (const-expr-option-rename-fn c$::const-expr-option
                                 uid (ident-fix new-fn))
    (const-expr-option-rename-fn c$::const-expr-option uid new-fn)))

Theorem: genassoc-rename-fn-of-genassoc-fix-genassoc

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

Theorem: genassoc-rename-fn-of-uid-fix-uid

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

Theorem: genassoc-rename-fn-of-ident-fix-new-fn

(defthm genassoc-rename-fn-of-ident-fix-new-fn
  (equal (genassoc-rename-fn c$::genassoc uid (ident-fix new-fn))
         (genassoc-rename-fn c$::genassoc uid new-fn)))

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

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

Theorem: genassoc-list-rename-fn-of-uid-fix-uid

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

Theorem: genassoc-list-rename-fn-of-ident-fix-new-fn

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

Theorem: member-designor-rename-fn-of-member-designor-fix-member-designor

(defthm
   member-designor-rename-fn-of-member-designor-fix-member-designor
 (equal (member-designor-rename-fn
             (member-designor-fix c$::member-designor)
             uid new-fn)
        (member-designor-rename-fn c$::member-designor uid new-fn)))

Theorem: member-designor-rename-fn-of-uid-fix-uid

(defthm member-designor-rename-fn-of-uid-fix-uid
 (equal
    (member-designor-rename-fn c$::member-designor (c$::uid-fix uid)
                               new-fn)
    (member-designor-rename-fn c$::member-designor uid new-fn)))

Theorem: member-designor-rename-fn-of-ident-fix-new-fn

(defthm member-designor-rename-fn-of-ident-fix-new-fn
 (equal (member-designor-rename-fn c$::member-designor
                                   uid (ident-fix new-fn))
        (member-designor-rename-fn c$::member-designor uid new-fn)))

Theorem: type-spec-rename-fn-of-type-spec-fix-type-spec

(defthm type-spec-rename-fn-of-type-spec-fix-type-spec
  (equal (type-spec-rename-fn (type-spec-fix c$::type-spec)
                              uid new-fn)
         (type-spec-rename-fn c$::type-spec uid new-fn)))

Theorem: type-spec-rename-fn-of-uid-fix-uid

(defthm type-spec-rename-fn-of-uid-fix-uid
  (equal (type-spec-rename-fn c$::type-spec (c$::uid-fix uid)
                              new-fn)
         (type-spec-rename-fn c$::type-spec uid new-fn)))

Theorem: type-spec-rename-fn-of-ident-fix-new-fn

(defthm type-spec-rename-fn-of-ident-fix-new-fn
  (equal (type-spec-rename-fn c$::type-spec uid (ident-fix new-fn))
         (type-spec-rename-fn c$::type-spec uid new-fn)))

Theorem: spec/qual-rename-fn-of-spec/qual-fix-spec/qual

(defthm spec/qual-rename-fn-of-spec/qual-fix-spec/qual
  (equal (spec/qual-rename-fn (spec/qual-fix c$::spec/qual)
                              uid new-fn)
         (spec/qual-rename-fn c$::spec/qual uid new-fn)))

Theorem: spec/qual-rename-fn-of-uid-fix-uid

(defthm spec/qual-rename-fn-of-uid-fix-uid
  (equal (spec/qual-rename-fn c$::spec/qual (c$::uid-fix uid)
                              new-fn)
         (spec/qual-rename-fn c$::spec/qual uid new-fn)))

Theorem: spec/qual-rename-fn-of-ident-fix-new-fn

(defthm spec/qual-rename-fn-of-ident-fix-new-fn
  (equal (spec/qual-rename-fn c$::spec/qual uid (ident-fix new-fn))
         (spec/qual-rename-fn c$::spec/qual uid new-fn)))

Theorem: spec/qual-list-rename-fn-of-spec/qual-list-fix-spec/qual-list

(defthm
      spec/qual-list-rename-fn-of-spec/qual-list-fix-spec/qual-list
 (equal
   (spec/qual-list-rename-fn (spec/qual-list-fix c$::spec/qual-list)
                             uid new-fn)
   (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn)))

Theorem: spec/qual-list-rename-fn-of-uid-fix-uid

(defthm spec/qual-list-rename-fn-of-uid-fix-uid
 (equal
      (spec/qual-list-rename-fn c$::spec/qual-list (c$::uid-fix uid)
                                new-fn)
      (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn)))

Theorem: spec/qual-list-rename-fn-of-ident-fix-new-fn

(defthm spec/qual-list-rename-fn-of-ident-fix-new-fn
  (equal (spec/qual-list-rename-fn c$::spec/qual-list
                                   uid (ident-fix new-fn))
         (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn)))

Theorem: align-spec-rename-fn-of-align-spec-fix-align-spec

(defthm align-spec-rename-fn-of-align-spec-fix-align-spec
  (equal (align-spec-rename-fn (align-spec-fix c$::align-spec)
                               uid new-fn)
         (align-spec-rename-fn c$::align-spec uid new-fn)))

Theorem: align-spec-rename-fn-of-uid-fix-uid

(defthm align-spec-rename-fn-of-uid-fix-uid
  (equal (align-spec-rename-fn c$::align-spec (c$::uid-fix uid)
                               new-fn)
         (align-spec-rename-fn c$::align-spec uid new-fn)))

Theorem: align-spec-rename-fn-of-ident-fix-new-fn

(defthm align-spec-rename-fn-of-ident-fix-new-fn
 (equal (align-spec-rename-fn c$::align-spec uid (ident-fix new-fn))
        (align-spec-rename-fn c$::align-spec uid new-fn)))

Theorem: decl-spec-rename-fn-of-decl-spec-fix-decl-spec

(defthm decl-spec-rename-fn-of-decl-spec-fix-decl-spec
  (equal (decl-spec-rename-fn (decl-spec-fix c$::decl-spec)
                              uid new-fn)
         (decl-spec-rename-fn c$::decl-spec uid new-fn)))

Theorem: decl-spec-rename-fn-of-uid-fix-uid

(defthm decl-spec-rename-fn-of-uid-fix-uid
  (equal (decl-spec-rename-fn c$::decl-spec (c$::uid-fix uid)
                              new-fn)
         (decl-spec-rename-fn c$::decl-spec uid new-fn)))

Theorem: decl-spec-rename-fn-of-ident-fix-new-fn

(defthm decl-spec-rename-fn-of-ident-fix-new-fn
  (equal (decl-spec-rename-fn c$::decl-spec uid (ident-fix new-fn))
         (decl-spec-rename-fn c$::decl-spec uid new-fn)))

Theorem: decl-spec-list-rename-fn-of-decl-spec-list-fix-decl-spec-list

(defthm
      decl-spec-list-rename-fn-of-decl-spec-list-fix-decl-spec-list
 (equal
   (decl-spec-list-rename-fn (decl-spec-list-fix c$::decl-spec-list)
                             uid new-fn)
   (decl-spec-list-rename-fn c$::decl-spec-list uid new-fn)))

Theorem: decl-spec-list-rename-fn-of-uid-fix-uid

(defthm decl-spec-list-rename-fn-of-uid-fix-uid
 (equal
      (decl-spec-list-rename-fn c$::decl-spec-list (c$::uid-fix uid)
                                new-fn)
      (decl-spec-list-rename-fn c$::decl-spec-list uid new-fn)))

Theorem: decl-spec-list-rename-fn-of-ident-fix-new-fn

(defthm decl-spec-list-rename-fn-of-ident-fix-new-fn
  (equal (decl-spec-list-rename-fn c$::decl-spec-list
                                   uid (ident-fix new-fn))
         (decl-spec-list-rename-fn c$::decl-spec-list uid new-fn)))

Theorem: typequal/attribspec-rename-fn-of-typequal/attribspec-fix-typequal/attribspec

(defthm
 typequal/attribspec-rename-fn-of-typequal/attribspec-fix-typequal/attribspec
 (equal (typequal/attribspec-rename-fn
             (c$::typequal/attribspec-fix c$::typequal/attribspec)
             uid new-fn)
        (typequal/attribspec-rename-fn
             c$::typequal/attribspec uid new-fn)))

Theorem: typequal/attribspec-rename-fn-of-uid-fix-uid

(defthm typequal/attribspec-rename-fn-of-uid-fix-uid
  (equal (typequal/attribspec-rename-fn c$::typequal/attribspec
                                        (c$::uid-fix uid)
                                        new-fn)
         (typequal/attribspec-rename-fn
              c$::typequal/attribspec uid new-fn)))

Theorem: typequal/attribspec-rename-fn-of-ident-fix-new-fn

(defthm typequal/attribspec-rename-fn-of-ident-fix-new-fn
  (equal (typequal/attribspec-rename-fn c$::typequal/attribspec
                                        uid (ident-fix new-fn))
         (typequal/attribspec-rename-fn
              c$::typequal/attribspec uid new-fn)))

Theorem: typequal/attribspec-list-rename-fn-of-typequal/attribspec-list-fix-typequal/attribspec-list

(defthm
 typequal/attribspec-list-rename-fn-of-typequal/attribspec-list-fix-typequal/attribspec-list
 (equal
  (typequal/attribspec-list-rename-fn
     (c$::typequal/attribspec-list-fix c$::typequal/attribspec-list)
     uid new-fn)
  (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                      uid new-fn)))

Theorem: typequal/attribspec-list-rename-fn-of-uid-fix-uid

(defthm typequal/attribspec-list-rename-fn-of-uid-fix-uid
 (equal
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        (c$::uid-fix uid)
                                        new-fn)
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid new-fn)))

Theorem: typequal/attribspec-list-rename-fn-of-ident-fix-new-fn

(defthm typequal/attribspec-list-rename-fn-of-ident-fix-new-fn
 (equal
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid (ident-fix new-fn))
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid new-fn)))

Theorem: typequal/attribspec-list-list-rename-fn-of-typequal/attribspec-list-list-fix-typequal/attribspec-list-list

(defthm
 typequal/attribspec-list-list-rename-fn-of-typequal/attribspec-list-list-fix-typequal/attribspec-list-list
 (equal (typequal/attribspec-list-list-rename-fn
             (c$::typequal/attribspec-list-list-fix
                  c$::typequal/attribspec-list-list)
             uid new-fn)
        (typequal/attribspec-list-list-rename-fn
             c$::typequal/attribspec-list-list
             uid new-fn)))

Theorem: typequal/attribspec-list-list-rename-fn-of-uid-fix-uid

(defthm typequal/attribspec-list-list-rename-fn-of-uid-fix-uid
  (equal (typequal/attribspec-list-list-rename-fn
              c$::typequal/attribspec-list-list
              (c$::uid-fix uid)
              new-fn)
         (typequal/attribspec-list-list-rename-fn
              c$::typequal/attribspec-list-list
              uid new-fn)))

Theorem: typequal/attribspec-list-list-rename-fn-of-ident-fix-new-fn

(defthm typequal/attribspec-list-list-rename-fn-of-ident-fix-new-fn
  (equal (typequal/attribspec-list-list-rename-fn
              c$::typequal/attribspec-list-list
              uid (ident-fix new-fn))
         (typequal/attribspec-list-list-rename-fn
              c$::typequal/attribspec-list-list
              uid new-fn)))

Theorem: initer-rename-fn-of-initer-fix-initer

(defthm initer-rename-fn-of-initer-fix-initer
  (equal (initer-rename-fn (initer-fix c$::initer)
                           uid new-fn)
         (initer-rename-fn c$::initer uid new-fn)))

Theorem: initer-rename-fn-of-uid-fix-uid

(defthm initer-rename-fn-of-uid-fix-uid
  (equal (initer-rename-fn c$::initer (c$::uid-fix uid)
                           new-fn)
         (initer-rename-fn c$::initer uid new-fn)))

Theorem: initer-rename-fn-of-ident-fix-new-fn

(defthm initer-rename-fn-of-ident-fix-new-fn
  (equal (initer-rename-fn c$::initer uid (ident-fix new-fn))
         (initer-rename-fn c$::initer uid new-fn)))

Theorem: initer-option-rename-fn-of-initer-option-fix-initer-option

(defthm initer-option-rename-fn-of-initer-option-fix-initer-option
 (equal
      (initer-option-rename-fn (initer-option-fix c$::initer-option)
                               uid new-fn)
      (initer-option-rename-fn c$::initer-option uid new-fn)))

Theorem: initer-option-rename-fn-of-uid-fix-uid

(defthm initer-option-rename-fn-of-uid-fix-uid
 (equal (initer-option-rename-fn c$::initer-option (c$::uid-fix uid)
                                 new-fn)
        (initer-option-rename-fn c$::initer-option uid new-fn)))

Theorem: initer-option-rename-fn-of-ident-fix-new-fn

(defthm initer-option-rename-fn-of-ident-fix-new-fn
  (equal (initer-option-rename-fn c$::initer-option
                                  uid (ident-fix new-fn))
         (initer-option-rename-fn c$::initer-option uid new-fn)))

Theorem: desiniter-rename-fn-of-desiniter-fix-desiniter

(defthm desiniter-rename-fn-of-desiniter-fix-desiniter
  (equal (desiniter-rename-fn (desiniter-fix desiniter)
                              uid new-fn)
         (desiniter-rename-fn desiniter uid new-fn)))

Theorem: desiniter-rename-fn-of-uid-fix-uid

(defthm desiniter-rename-fn-of-uid-fix-uid
  (equal (desiniter-rename-fn desiniter (c$::uid-fix uid)
                              new-fn)
         (desiniter-rename-fn desiniter uid new-fn)))

Theorem: desiniter-rename-fn-of-ident-fix-new-fn

(defthm desiniter-rename-fn-of-ident-fix-new-fn
  (equal (desiniter-rename-fn desiniter uid (ident-fix new-fn))
         (desiniter-rename-fn desiniter uid new-fn)))

Theorem: desiniter-list-rename-fn-of-desiniter-list-fix-desiniter-list

(defthm
      desiniter-list-rename-fn-of-desiniter-list-fix-desiniter-list
 (equal
   (desiniter-list-rename-fn (desiniter-list-fix c$::desiniter-list)
                             uid new-fn)
   (desiniter-list-rename-fn c$::desiniter-list uid new-fn)))

Theorem: desiniter-list-rename-fn-of-uid-fix-uid

(defthm desiniter-list-rename-fn-of-uid-fix-uid
 (equal
      (desiniter-list-rename-fn c$::desiniter-list (c$::uid-fix uid)
                                new-fn)
      (desiniter-list-rename-fn c$::desiniter-list uid new-fn)))

Theorem: desiniter-list-rename-fn-of-ident-fix-new-fn

(defthm desiniter-list-rename-fn-of-ident-fix-new-fn
  (equal (desiniter-list-rename-fn c$::desiniter-list
                                   uid (ident-fix new-fn))
         (desiniter-list-rename-fn c$::desiniter-list uid new-fn)))

Theorem: designor-rename-fn-of-designor-fix-designor

(defthm designor-rename-fn-of-designor-fix-designor
  (equal (designor-rename-fn (designor-fix c$::designor)
                             uid new-fn)
         (designor-rename-fn c$::designor uid new-fn)))

Theorem: designor-rename-fn-of-uid-fix-uid

(defthm designor-rename-fn-of-uid-fix-uid
  (equal (designor-rename-fn c$::designor (c$::uid-fix uid)
                             new-fn)
         (designor-rename-fn c$::designor uid new-fn)))

Theorem: designor-rename-fn-of-ident-fix-new-fn

(defthm designor-rename-fn-of-ident-fix-new-fn
  (equal (designor-rename-fn c$::designor uid (ident-fix new-fn))
         (designor-rename-fn c$::designor uid new-fn)))

Theorem: designor-list-rename-fn-of-designor-list-fix-designor-list

(defthm designor-list-rename-fn-of-designor-list-fix-designor-list
 (equal
      (designor-list-rename-fn (designor-list-fix c$::designor-list)
                               uid new-fn)
      (designor-list-rename-fn c$::designor-list uid new-fn)))

Theorem: designor-list-rename-fn-of-uid-fix-uid

(defthm designor-list-rename-fn-of-uid-fix-uid
 (equal (designor-list-rename-fn c$::designor-list (c$::uid-fix uid)
                                 new-fn)
        (designor-list-rename-fn c$::designor-list uid new-fn)))

Theorem: designor-list-rename-fn-of-ident-fix-new-fn

(defthm designor-list-rename-fn-of-ident-fix-new-fn
  (equal (designor-list-rename-fn c$::designor-list
                                  uid (ident-fix new-fn))
         (designor-list-rename-fn c$::designor-list uid new-fn)))

Theorem: declor-rename-fn-of-declor-fix-declor

(defthm declor-rename-fn-of-declor-fix-declor
  (equal (declor-rename-fn (declor-fix declor)
                           uid new-fn)
         (declor-rename-fn declor uid new-fn)))

Theorem: declor-rename-fn-of-uid-fix-uid

(defthm declor-rename-fn-of-uid-fix-uid
  (equal (declor-rename-fn declor (c$::uid-fix uid)
                           new-fn)
         (declor-rename-fn declor uid new-fn)))

Theorem: declor-rename-fn-of-ident-fix-new-fn

(defthm declor-rename-fn-of-ident-fix-new-fn
  (equal (declor-rename-fn declor uid (ident-fix new-fn))
         (declor-rename-fn declor uid new-fn)))

Theorem: declor-option-rename-fn-of-declor-option-fix-declor-option

(defthm declor-option-rename-fn-of-declor-option-fix-declor-option
 (equal
      (declor-option-rename-fn (declor-option-fix c$::declor-option)
                               uid new-fn)
      (declor-option-rename-fn c$::declor-option uid new-fn)))

Theorem: declor-option-rename-fn-of-uid-fix-uid

(defthm declor-option-rename-fn-of-uid-fix-uid
 (equal (declor-option-rename-fn c$::declor-option (c$::uid-fix uid)
                                 new-fn)
        (declor-option-rename-fn c$::declor-option uid new-fn)))

Theorem: declor-option-rename-fn-of-ident-fix-new-fn

(defthm declor-option-rename-fn-of-ident-fix-new-fn
  (equal (declor-option-rename-fn c$::declor-option
                                  uid (ident-fix new-fn))
         (declor-option-rename-fn c$::declor-option uid new-fn)))

Theorem: dirdeclor-rename-fn-of-dirdeclor-fix-dirdeclor

(defthm dirdeclor-rename-fn-of-dirdeclor-fix-dirdeclor
  (equal (dirdeclor-rename-fn (dirdeclor-fix dirdeclor)
                              uid new-fn)
         (dirdeclor-rename-fn dirdeclor uid new-fn)))

Theorem: dirdeclor-rename-fn-of-uid-fix-uid

(defthm dirdeclor-rename-fn-of-uid-fix-uid
  (equal (dirdeclor-rename-fn dirdeclor (c$::uid-fix uid)
                              new-fn)
         (dirdeclor-rename-fn dirdeclor uid new-fn)))

Theorem: dirdeclor-rename-fn-of-ident-fix-new-fn

(defthm dirdeclor-rename-fn-of-ident-fix-new-fn
  (equal (dirdeclor-rename-fn dirdeclor uid (ident-fix new-fn))
         (dirdeclor-rename-fn dirdeclor uid new-fn)))

Theorem: absdeclor-rename-fn-of-absdeclor-fix-absdeclor

(defthm absdeclor-rename-fn-of-absdeclor-fix-absdeclor
  (equal (absdeclor-rename-fn (absdeclor-fix absdeclor)
                              uid new-fn)
         (absdeclor-rename-fn absdeclor uid new-fn)))

Theorem: absdeclor-rename-fn-of-uid-fix-uid

(defthm absdeclor-rename-fn-of-uid-fix-uid
  (equal (absdeclor-rename-fn absdeclor (c$::uid-fix uid)
                              new-fn)
         (absdeclor-rename-fn absdeclor uid new-fn)))

Theorem: absdeclor-rename-fn-of-ident-fix-new-fn

(defthm absdeclor-rename-fn-of-ident-fix-new-fn
  (equal (absdeclor-rename-fn absdeclor uid (ident-fix new-fn))
         (absdeclor-rename-fn absdeclor uid new-fn)))

Theorem: absdeclor-option-rename-fn-of-absdeclor-option-fix-absdeclor-option

(defthm
 absdeclor-option-rename-fn-of-absdeclor-option-fix-absdeclor-option
 (equal
      (absdeclor-option-rename-fn
           (absdeclor-option-fix c$::absdeclor-option)
           uid new-fn)
      (absdeclor-option-rename-fn c$::absdeclor-option uid new-fn)))

Theorem: absdeclor-option-rename-fn-of-uid-fix-uid

(defthm absdeclor-option-rename-fn-of-uid-fix-uid
 (equal
  (absdeclor-option-rename-fn c$::absdeclor-option (c$::uid-fix uid)
                              new-fn)
  (absdeclor-option-rename-fn c$::absdeclor-option uid new-fn)))

Theorem: absdeclor-option-rename-fn-of-ident-fix-new-fn

(defthm absdeclor-option-rename-fn-of-ident-fix-new-fn
 (equal
      (absdeclor-option-rename-fn c$::absdeclor-option
                                  uid (ident-fix new-fn))
      (absdeclor-option-rename-fn c$::absdeclor-option uid new-fn)))

Theorem: dirabsdeclor-rename-fn-of-dirabsdeclor-fix-dirabsdeclor

(defthm dirabsdeclor-rename-fn-of-dirabsdeclor-fix-dirabsdeclor
  (equal (dirabsdeclor-rename-fn (dirabsdeclor-fix c$::dirabsdeclor)
                                 uid new-fn)
         (dirabsdeclor-rename-fn c$::dirabsdeclor uid new-fn)))

Theorem: dirabsdeclor-rename-fn-of-uid-fix-uid

(defthm dirabsdeclor-rename-fn-of-uid-fix-uid
  (equal (dirabsdeclor-rename-fn c$::dirabsdeclor (c$::uid-fix uid)
                                 new-fn)
         (dirabsdeclor-rename-fn c$::dirabsdeclor uid new-fn)))

Theorem: dirabsdeclor-rename-fn-of-ident-fix-new-fn

(defthm dirabsdeclor-rename-fn-of-ident-fix-new-fn
 (equal
    (dirabsdeclor-rename-fn c$::dirabsdeclor uid (ident-fix new-fn))
    (dirabsdeclor-rename-fn c$::dirabsdeclor uid new-fn)))

Theorem: dirabsdeclor-option-rename-fn-of-dirabsdeclor-option-fix-dirabsdeclor-option

(defthm
 dirabsdeclor-option-rename-fn-of-dirabsdeclor-option-fix-dirabsdeclor-option
 (equal (dirabsdeclor-option-rename-fn
             (dirabsdeclor-option-fix c$::dirabsdeclor-option)
             uid new-fn)
        (dirabsdeclor-option-rename-fn
             c$::dirabsdeclor-option uid new-fn)))

Theorem: dirabsdeclor-option-rename-fn-of-uid-fix-uid

(defthm dirabsdeclor-option-rename-fn-of-uid-fix-uid
  (equal (dirabsdeclor-option-rename-fn c$::dirabsdeclor-option
                                        (c$::uid-fix uid)
                                        new-fn)
         (dirabsdeclor-option-rename-fn
              c$::dirabsdeclor-option uid new-fn)))

Theorem: dirabsdeclor-option-rename-fn-of-ident-fix-new-fn

(defthm dirabsdeclor-option-rename-fn-of-ident-fix-new-fn
  (equal (dirabsdeclor-option-rename-fn c$::dirabsdeclor-option
                                        uid (ident-fix new-fn))
         (dirabsdeclor-option-rename-fn
              c$::dirabsdeclor-option uid new-fn)))

Theorem: param-declon-rename-fn-of-param-declon-fix-param-declon

(defthm param-declon-rename-fn-of-param-declon-fix-param-declon
  (equal (param-declon-rename-fn (param-declon-fix param-declon)
                                 uid new-fn)
         (param-declon-rename-fn param-declon uid new-fn)))

Theorem: param-declon-rename-fn-of-uid-fix-uid

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

Theorem: param-declon-rename-fn-of-ident-fix-new-fn

(defthm param-declon-rename-fn-of-ident-fix-new-fn
 (equal (param-declon-rename-fn param-declon uid (ident-fix new-fn))
        (param-declon-rename-fn param-declon uid new-fn)))

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

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

Theorem: param-declon-list-rename-fn-of-uid-fix-uid

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

Theorem: param-declon-list-rename-fn-of-ident-fix-new-fn

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

Theorem: param-declor-rename-fn-of-param-declor-fix-param-declor

(defthm param-declor-rename-fn-of-param-declor-fix-param-declor
  (equal (param-declor-rename-fn (param-declor-fix c$::param-declor)
                                 uid new-fn)
         (param-declor-rename-fn c$::param-declor uid new-fn)))

Theorem: param-declor-rename-fn-of-uid-fix-uid

(defthm param-declor-rename-fn-of-uid-fix-uid
  (equal (param-declor-rename-fn c$::param-declor (c$::uid-fix uid)
                                 new-fn)
         (param-declor-rename-fn c$::param-declor uid new-fn)))

Theorem: param-declor-rename-fn-of-ident-fix-new-fn

(defthm param-declor-rename-fn-of-ident-fix-new-fn
 (equal
    (param-declor-rename-fn c$::param-declor uid (ident-fix new-fn))
    (param-declor-rename-fn c$::param-declor uid new-fn)))

Theorem: tyname-rename-fn-of-tyname-fix-tyname

(defthm tyname-rename-fn-of-tyname-fix-tyname
  (equal (tyname-rename-fn (tyname-fix tyname)
                           uid new-fn)
         (tyname-rename-fn tyname uid new-fn)))

Theorem: tyname-rename-fn-of-uid-fix-uid

(defthm tyname-rename-fn-of-uid-fix-uid
  (equal (tyname-rename-fn tyname (c$::uid-fix uid)
                           new-fn)
         (tyname-rename-fn tyname uid new-fn)))

Theorem: tyname-rename-fn-of-ident-fix-new-fn

(defthm tyname-rename-fn-of-ident-fix-new-fn
  (equal (tyname-rename-fn tyname uid (ident-fix new-fn))
         (tyname-rename-fn tyname uid new-fn)))

Theorem: struni-spec-rename-fn-of-struni-spec-fix-struni-spec

(defthm struni-spec-rename-fn-of-struni-spec-fix-struni-spec
  (equal (struni-spec-rename-fn (struni-spec-fix struni-spec)
                                uid new-fn)
         (struni-spec-rename-fn struni-spec uid new-fn)))

Theorem: struni-spec-rename-fn-of-uid-fix-uid

(defthm struni-spec-rename-fn-of-uid-fix-uid
  (equal (struni-spec-rename-fn struni-spec (c$::uid-fix uid)
                                new-fn)
         (struni-spec-rename-fn struni-spec uid new-fn)))

Theorem: struni-spec-rename-fn-of-ident-fix-new-fn

(defthm struni-spec-rename-fn-of-ident-fix-new-fn
  (equal (struni-spec-rename-fn struni-spec uid (ident-fix new-fn))
         (struni-spec-rename-fn struni-spec uid new-fn)))

Theorem: struct-declon-rename-fn-of-struct-declon-fix-struct-declon

(defthm struct-declon-rename-fn-of-struct-declon-fix-struct-declon
 (equal
      (struct-declon-rename-fn (struct-declon-fix c$::struct-declon)
                               uid new-fn)
      (struct-declon-rename-fn c$::struct-declon uid new-fn)))

Theorem: struct-declon-rename-fn-of-uid-fix-uid

(defthm struct-declon-rename-fn-of-uid-fix-uid
 (equal (struct-declon-rename-fn c$::struct-declon (c$::uid-fix uid)
                                 new-fn)
        (struct-declon-rename-fn c$::struct-declon uid new-fn)))

Theorem: struct-declon-rename-fn-of-ident-fix-new-fn

(defthm struct-declon-rename-fn-of-ident-fix-new-fn
  (equal (struct-declon-rename-fn c$::struct-declon
                                  uid (ident-fix new-fn))
         (struct-declon-rename-fn c$::struct-declon uid new-fn)))

Theorem: struct-declon-list-rename-fn-of-struct-declon-list-fix-struct-declon-list

(defthm
 struct-declon-list-rename-fn-of-struct-declon-list-fix-struct-declon-list
 (equal
  (struct-declon-list-rename-fn
       (struct-declon-list-fix c$::struct-declon-list)
       uid new-fn)
  (struct-declon-list-rename-fn c$::struct-declon-list uid new-fn)))

Theorem: struct-declon-list-rename-fn-of-uid-fix-uid

(defthm struct-declon-list-rename-fn-of-uid-fix-uid
 (equal
  (struct-declon-list-rename-fn
       c$::struct-declon-list (c$::uid-fix uid)
       new-fn)
  (struct-declon-list-rename-fn c$::struct-declon-list uid new-fn)))

Theorem: struct-declon-list-rename-fn-of-ident-fix-new-fn

(defthm struct-declon-list-rename-fn-of-ident-fix-new-fn
 (equal
  (struct-declon-list-rename-fn c$::struct-declon-list
                                uid (ident-fix new-fn))
  (struct-declon-list-rename-fn c$::struct-declon-list uid new-fn)))

Theorem: struct-declor-rename-fn-of-struct-declor-fix-struct-declor

(defthm struct-declor-rename-fn-of-struct-declor-fix-struct-declor
  (equal (struct-declor-rename-fn (struct-declor-fix struct-declor)
                                  uid new-fn)
         (struct-declor-rename-fn struct-declor uid new-fn)))

Theorem: struct-declor-rename-fn-of-uid-fix-uid

(defthm struct-declor-rename-fn-of-uid-fix-uid
  (equal (struct-declor-rename-fn struct-declor (c$::uid-fix uid)
                                  new-fn)
         (struct-declor-rename-fn struct-declor uid new-fn)))

Theorem: struct-declor-rename-fn-of-ident-fix-new-fn

(defthm struct-declor-rename-fn-of-ident-fix-new-fn
 (equal
      (struct-declor-rename-fn struct-declor uid (ident-fix new-fn))
      (struct-declor-rename-fn struct-declor uid new-fn)))

Theorem: struct-declor-list-rename-fn-of-struct-declor-list-fix-struct-declor-list

(defthm
 struct-declor-list-rename-fn-of-struct-declor-list-fix-struct-declor-list
 (equal
  (struct-declor-list-rename-fn
       (struct-declor-list-fix c$::struct-declor-list)
       uid new-fn)
  (struct-declor-list-rename-fn c$::struct-declor-list uid new-fn)))

Theorem: struct-declor-list-rename-fn-of-uid-fix-uid

(defthm struct-declor-list-rename-fn-of-uid-fix-uid
 (equal
  (struct-declor-list-rename-fn
       c$::struct-declor-list (c$::uid-fix uid)
       new-fn)
  (struct-declor-list-rename-fn c$::struct-declor-list uid new-fn)))

Theorem: struct-declor-list-rename-fn-of-ident-fix-new-fn

(defthm struct-declor-list-rename-fn-of-ident-fix-new-fn
 (equal
  (struct-declor-list-rename-fn c$::struct-declor-list
                                uid (ident-fix new-fn))
  (struct-declor-list-rename-fn c$::struct-declor-list uid new-fn)))

Theorem: enum-spec-rename-fn-of-enum-spec-fix-enum-spec

(defthm enum-spec-rename-fn-of-enum-spec-fix-enum-spec
  (equal (enum-spec-rename-fn (enum-spec-fix enum-spec)
                              uid new-fn)
         (enum-spec-rename-fn enum-spec uid new-fn)))

Theorem: enum-spec-rename-fn-of-uid-fix-uid

(defthm enum-spec-rename-fn-of-uid-fix-uid
  (equal (enum-spec-rename-fn enum-spec (c$::uid-fix uid)
                              new-fn)
         (enum-spec-rename-fn enum-spec uid new-fn)))

Theorem: enum-spec-rename-fn-of-ident-fix-new-fn

(defthm enum-spec-rename-fn-of-ident-fix-new-fn
  (equal (enum-spec-rename-fn enum-spec uid (ident-fix new-fn))
         (enum-spec-rename-fn enum-spec uid new-fn)))

Theorem: enumer-rename-fn-of-enumer-fix-enumer

(defthm enumer-rename-fn-of-enumer-fix-enumer
  (equal (enumer-rename-fn (enumer-fix enumer)
                           uid new-fn)
         (enumer-rename-fn enumer uid new-fn)))

Theorem: enumer-rename-fn-of-uid-fix-uid

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

Theorem: enumer-rename-fn-of-ident-fix-new-fn

(defthm enumer-rename-fn-of-ident-fix-new-fn
  (equal (enumer-rename-fn enumer uid (ident-fix new-fn))
         (enumer-rename-fn enumer uid new-fn)))

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

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

Theorem: enumer-list-rename-fn-of-uid-fix-uid

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

Theorem: enumer-list-rename-fn-of-ident-fix-new-fn

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

Theorem: statassert-rename-fn-of-statassert-fix-statassert

(defthm statassert-rename-fn-of-statassert-fix-statassert
  (equal (statassert-rename-fn (statassert-fix statassert)
                               uid new-fn)
         (statassert-rename-fn statassert uid new-fn)))

Theorem: statassert-rename-fn-of-uid-fix-uid

(defthm statassert-rename-fn-of-uid-fix-uid
  (equal (statassert-rename-fn statassert (c$::uid-fix uid)
                               new-fn)
         (statassert-rename-fn statassert uid new-fn)))

Theorem: statassert-rename-fn-of-ident-fix-new-fn

(defthm statassert-rename-fn-of-ident-fix-new-fn
  (equal (statassert-rename-fn statassert uid (ident-fix new-fn))
         (statassert-rename-fn statassert uid new-fn)))

Theorem: attrib-rename-fn-of-attrib-fix-attrib

(defthm attrib-rename-fn-of-attrib-fix-attrib
  (equal (attrib-rename-fn (c$::attrib-fix c$::attrib)
                           uid new-fn)
         (attrib-rename-fn c$::attrib uid new-fn)))

Theorem: attrib-rename-fn-of-uid-fix-uid

(defthm attrib-rename-fn-of-uid-fix-uid
  (equal (attrib-rename-fn c$::attrib (c$::uid-fix uid)
                           new-fn)
         (attrib-rename-fn c$::attrib uid new-fn)))

Theorem: attrib-rename-fn-of-ident-fix-new-fn

(defthm attrib-rename-fn-of-ident-fix-new-fn
  (equal (attrib-rename-fn c$::attrib uid (ident-fix new-fn))
         (attrib-rename-fn c$::attrib uid new-fn)))

Theorem: attrib-list-rename-fn-of-attrib-list-fix-attrib-list

(defthm attrib-list-rename-fn-of-attrib-list-fix-attrib-list
 (equal (attrib-list-rename-fn (c$::attrib-list-fix c$::attrib-list)
                               uid new-fn)
        (attrib-list-rename-fn c$::attrib-list uid new-fn)))

Theorem: attrib-list-rename-fn-of-uid-fix-uid

(defthm attrib-list-rename-fn-of-uid-fix-uid
  (equal (attrib-list-rename-fn c$::attrib-list (c$::uid-fix uid)
                                new-fn)
         (attrib-list-rename-fn c$::attrib-list uid new-fn)))

Theorem: attrib-list-rename-fn-of-ident-fix-new-fn

(defthm attrib-list-rename-fn-of-ident-fix-new-fn
 (equal
      (attrib-list-rename-fn c$::attrib-list uid (ident-fix new-fn))
      (attrib-list-rename-fn c$::attrib-list uid new-fn)))

Theorem: attrib-spec-rename-fn-of-attrib-spec-fix-attrib-spec

(defthm attrib-spec-rename-fn-of-attrib-spec-fix-attrib-spec
 (equal (attrib-spec-rename-fn (c$::attrib-spec-fix c$::attrib-spec)
                               uid new-fn)
        (attrib-spec-rename-fn c$::attrib-spec uid new-fn)))

Theorem: attrib-spec-rename-fn-of-uid-fix-uid

(defthm attrib-spec-rename-fn-of-uid-fix-uid
  (equal (attrib-spec-rename-fn c$::attrib-spec (c$::uid-fix uid)
                                new-fn)
         (attrib-spec-rename-fn c$::attrib-spec uid new-fn)))

Theorem: attrib-spec-rename-fn-of-ident-fix-new-fn

(defthm attrib-spec-rename-fn-of-ident-fix-new-fn
 (equal
      (attrib-spec-rename-fn c$::attrib-spec uid (ident-fix new-fn))
      (attrib-spec-rename-fn c$::attrib-spec uid new-fn)))

Theorem: attrib-spec-list-rename-fn-of-attrib-spec-list-fix-attrib-spec-list

(defthm
 attrib-spec-list-rename-fn-of-attrib-spec-list-fix-attrib-spec-list
 (equal
      (attrib-spec-list-rename-fn
           (c$::attrib-spec-list-fix c$::attrib-spec-list)
           uid new-fn)
      (attrib-spec-list-rename-fn c$::attrib-spec-list uid new-fn)))

Theorem: attrib-spec-list-rename-fn-of-uid-fix-uid

(defthm attrib-spec-list-rename-fn-of-uid-fix-uid
 (equal
  (attrib-spec-list-rename-fn c$::attrib-spec-list (c$::uid-fix uid)
                              new-fn)
  (attrib-spec-list-rename-fn c$::attrib-spec-list uid new-fn)))

Theorem: attrib-spec-list-rename-fn-of-ident-fix-new-fn

(defthm attrib-spec-list-rename-fn-of-ident-fix-new-fn
 (equal
      (attrib-spec-list-rename-fn c$::attrib-spec-list
                                  uid (ident-fix new-fn))
      (attrib-spec-list-rename-fn c$::attrib-spec-list uid new-fn)))

Theorem: initdeclor-rename-fn-of-initdeclor-fix-initdeclor

(defthm initdeclor-rename-fn-of-initdeclor-fix-initdeclor
  (equal (initdeclor-rename-fn (initdeclor-fix initdeclor)
                               uid new-fn)
         (initdeclor-rename-fn initdeclor uid new-fn)))

Theorem: initdeclor-rename-fn-of-uid-fix-uid

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

Theorem: initdeclor-rename-fn-of-ident-fix-new-fn

(defthm initdeclor-rename-fn-of-ident-fix-new-fn
  (equal (initdeclor-rename-fn initdeclor uid (ident-fix new-fn))
         (initdeclor-rename-fn initdeclor uid new-fn)))

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

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

Theorem: initdeclor-list-rename-fn-of-uid-fix-uid

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

Theorem: initdeclor-list-rename-fn-of-ident-fix-new-fn

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

Theorem: decl-rename-fn-of-decl-fix-decl

(defthm decl-rename-fn-of-decl-fix-decl
  (equal (decl-rename-fn (decl-fix decl)
                         uid new-fn)
         (decl-rename-fn decl uid new-fn)))

Theorem: decl-rename-fn-of-uid-fix-uid

(defthm decl-rename-fn-of-uid-fix-uid
  (equal (decl-rename-fn decl (c$::uid-fix uid)
                         new-fn)
         (decl-rename-fn decl uid new-fn)))

Theorem: decl-rename-fn-of-ident-fix-new-fn

(defthm decl-rename-fn-of-ident-fix-new-fn
  (equal (decl-rename-fn decl uid (ident-fix new-fn))
         (decl-rename-fn decl uid new-fn)))

Theorem: decl-list-rename-fn-of-decl-list-fix-decl-list

(defthm decl-list-rename-fn-of-decl-list-fix-decl-list
  (equal (decl-list-rename-fn (c$::decl-list-fix c$::decl-list)
                              uid new-fn)
         (decl-list-rename-fn c$::decl-list uid new-fn)))

Theorem: decl-list-rename-fn-of-uid-fix-uid

(defthm decl-list-rename-fn-of-uid-fix-uid
  (equal (decl-list-rename-fn c$::decl-list (c$::uid-fix uid)
                              new-fn)
         (decl-list-rename-fn c$::decl-list uid new-fn)))

Theorem: decl-list-rename-fn-of-ident-fix-new-fn

(defthm decl-list-rename-fn-of-ident-fix-new-fn
  (equal (decl-list-rename-fn c$::decl-list uid (ident-fix new-fn))
         (decl-list-rename-fn c$::decl-list uid new-fn)))

Theorem: label-rename-fn-of-label-fix-label

(defthm label-rename-fn-of-label-fix-label
  (equal (label-rename-fn (label-fix c$::label)
                          uid new-fn)
         (label-rename-fn c$::label uid new-fn)))

Theorem: label-rename-fn-of-uid-fix-uid

(defthm label-rename-fn-of-uid-fix-uid
  (equal (label-rename-fn c$::label (c$::uid-fix uid)
                          new-fn)
         (label-rename-fn c$::label uid new-fn)))

Theorem: label-rename-fn-of-ident-fix-new-fn

(defthm label-rename-fn-of-ident-fix-new-fn
  (equal (label-rename-fn c$::label uid (ident-fix new-fn))
         (label-rename-fn c$::label uid new-fn)))

Theorem: asm-output-rename-fn-of-asm-output-fix-asm-output

(defthm asm-output-rename-fn-of-asm-output-fix-asm-output
  (equal (asm-output-rename-fn (c$::asm-output-fix c$::asm-output)
                               uid new-fn)
         (asm-output-rename-fn c$::asm-output uid new-fn)))

Theorem: asm-output-rename-fn-of-uid-fix-uid

(defthm asm-output-rename-fn-of-uid-fix-uid
  (equal (asm-output-rename-fn c$::asm-output (c$::uid-fix uid)
                               new-fn)
         (asm-output-rename-fn c$::asm-output uid new-fn)))

Theorem: asm-output-rename-fn-of-ident-fix-new-fn

(defthm asm-output-rename-fn-of-ident-fix-new-fn
 (equal (asm-output-rename-fn c$::asm-output uid (ident-fix new-fn))
        (asm-output-rename-fn c$::asm-output uid new-fn)))

Theorem: asm-output-list-rename-fn-of-asm-output-list-fix-asm-output-list

(defthm
   asm-output-list-rename-fn-of-asm-output-list-fix-asm-output-list
 (equal (asm-output-list-rename-fn
             (c$::asm-output-list-fix c$::asm-output-list)
             uid new-fn)
        (asm-output-list-rename-fn c$::asm-output-list uid new-fn)))

Theorem: asm-output-list-rename-fn-of-uid-fix-uid

(defthm asm-output-list-rename-fn-of-uid-fix-uid
 (equal
    (asm-output-list-rename-fn c$::asm-output-list (c$::uid-fix uid)
                               new-fn)
    (asm-output-list-rename-fn c$::asm-output-list uid new-fn)))

Theorem: asm-output-list-rename-fn-of-ident-fix-new-fn

(defthm asm-output-list-rename-fn-of-ident-fix-new-fn
 (equal (asm-output-list-rename-fn c$::asm-output-list
                                   uid (ident-fix new-fn))
        (asm-output-list-rename-fn c$::asm-output-list uid new-fn)))

Theorem: asm-input-rename-fn-of-asm-input-fix-asm-input

(defthm asm-input-rename-fn-of-asm-input-fix-asm-input
  (equal (asm-input-rename-fn (c$::asm-input-fix c$::asm-input)
                              uid new-fn)
         (asm-input-rename-fn c$::asm-input uid new-fn)))

Theorem: asm-input-rename-fn-of-uid-fix-uid

(defthm asm-input-rename-fn-of-uid-fix-uid
  (equal (asm-input-rename-fn c$::asm-input (c$::uid-fix uid)
                              new-fn)
         (asm-input-rename-fn c$::asm-input uid new-fn)))

Theorem: asm-input-rename-fn-of-ident-fix-new-fn

(defthm asm-input-rename-fn-of-ident-fix-new-fn
  (equal (asm-input-rename-fn c$::asm-input uid (ident-fix new-fn))
         (asm-input-rename-fn c$::asm-input uid new-fn)))

Theorem: asm-input-list-rename-fn-of-asm-input-list-fix-asm-input-list

(defthm
      asm-input-list-rename-fn-of-asm-input-list-fix-asm-input-list
  (equal (asm-input-list-rename-fn
              (c$::asm-input-list-fix c$::asm-input-list)
              uid new-fn)
         (asm-input-list-rename-fn c$::asm-input-list uid new-fn)))

Theorem: asm-input-list-rename-fn-of-uid-fix-uid

(defthm asm-input-list-rename-fn-of-uid-fix-uid
 (equal
      (asm-input-list-rename-fn c$::asm-input-list (c$::uid-fix uid)
                                new-fn)
      (asm-input-list-rename-fn c$::asm-input-list uid new-fn)))

Theorem: asm-input-list-rename-fn-of-ident-fix-new-fn

(defthm asm-input-list-rename-fn-of-ident-fix-new-fn
  (equal (asm-input-list-rename-fn c$::asm-input-list
                                   uid (ident-fix new-fn))
         (asm-input-list-rename-fn c$::asm-input-list uid new-fn)))

Theorem: asm-stmt-rename-fn-of-asm-stmt-fix-asm-stmt

(defthm asm-stmt-rename-fn-of-asm-stmt-fix-asm-stmt
  (equal (asm-stmt-rename-fn (c$::asm-stmt-fix c$::asm-stmt)
                             uid new-fn)
         (asm-stmt-rename-fn c$::asm-stmt uid new-fn)))

Theorem: asm-stmt-rename-fn-of-uid-fix-uid

(defthm asm-stmt-rename-fn-of-uid-fix-uid
  (equal (asm-stmt-rename-fn c$::asm-stmt (c$::uid-fix uid)
                             new-fn)
         (asm-stmt-rename-fn c$::asm-stmt uid new-fn)))

Theorem: asm-stmt-rename-fn-of-ident-fix-new-fn

(defthm asm-stmt-rename-fn-of-ident-fix-new-fn
  (equal (asm-stmt-rename-fn c$::asm-stmt uid (ident-fix new-fn))
         (asm-stmt-rename-fn c$::asm-stmt uid new-fn)))

Theorem: stmt-rename-fn-of-stmt-fix-stmt

(defthm stmt-rename-fn-of-stmt-fix-stmt
  (equal (stmt-rename-fn (stmt-fix c$::stmt)
                         uid new-fn)
         (stmt-rename-fn c$::stmt uid new-fn)))

Theorem: stmt-rename-fn-of-uid-fix-uid

(defthm stmt-rename-fn-of-uid-fix-uid
  (equal (stmt-rename-fn c$::stmt (c$::uid-fix uid)
                         new-fn)
         (stmt-rename-fn c$::stmt uid new-fn)))

Theorem: stmt-rename-fn-of-ident-fix-new-fn

(defthm stmt-rename-fn-of-ident-fix-new-fn
  (equal (stmt-rename-fn c$::stmt uid (ident-fix new-fn))
         (stmt-rename-fn c$::stmt uid new-fn)))

Theorem: comp-stmt-rename-fn-of-comp-stmt-fix-comp-stmt

(defthm comp-stmt-rename-fn-of-comp-stmt-fix-comp-stmt
  (equal (comp-stmt-rename-fn (c$::comp-stmt-fix comp-stmt)
                              uid new-fn)
         (comp-stmt-rename-fn comp-stmt uid new-fn)))

Theorem: comp-stmt-rename-fn-of-uid-fix-uid

(defthm comp-stmt-rename-fn-of-uid-fix-uid
  (equal (comp-stmt-rename-fn comp-stmt (c$::uid-fix uid)
                              new-fn)
         (comp-stmt-rename-fn comp-stmt uid new-fn)))

Theorem: comp-stmt-rename-fn-of-ident-fix-new-fn

(defthm comp-stmt-rename-fn-of-ident-fix-new-fn
  (equal (comp-stmt-rename-fn comp-stmt uid (ident-fix new-fn))
         (comp-stmt-rename-fn comp-stmt uid new-fn)))

Theorem: block-item-rename-fn-of-block-item-fix-block-item

(defthm block-item-rename-fn-of-block-item-fix-block-item
  (equal (block-item-rename-fn (block-item-fix c$::block-item)
                               uid new-fn)
         (block-item-rename-fn c$::block-item uid new-fn)))

Theorem: block-item-rename-fn-of-uid-fix-uid

(defthm block-item-rename-fn-of-uid-fix-uid
  (equal (block-item-rename-fn c$::block-item (c$::uid-fix uid)
                               new-fn)
         (block-item-rename-fn c$::block-item uid new-fn)))

Theorem: block-item-rename-fn-of-ident-fix-new-fn

(defthm block-item-rename-fn-of-ident-fix-new-fn
 (equal (block-item-rename-fn c$::block-item uid (ident-fix new-fn))
        (block-item-rename-fn c$::block-item uid new-fn)))

Theorem: block-item-list-rename-fn-of-block-item-list-fix-block-item-list

(defthm
   block-item-list-rename-fn-of-block-item-list-fix-block-item-list
 (equal (block-item-list-rename-fn
             (block-item-list-fix c$::block-item-list)
             uid new-fn)
        (block-item-list-rename-fn c$::block-item-list uid new-fn)))

Theorem: block-item-list-rename-fn-of-uid-fix-uid

(defthm block-item-list-rename-fn-of-uid-fix-uid
 (equal
    (block-item-list-rename-fn c$::block-item-list (c$::uid-fix uid)
                               new-fn)
    (block-item-list-rename-fn c$::block-item-list uid new-fn)))

Theorem: block-item-list-rename-fn-of-ident-fix-new-fn

(defthm block-item-list-rename-fn-of-ident-fix-new-fn
 (equal (block-item-list-rename-fn c$::block-item-list
                                   uid (ident-fix new-fn))
        (block-item-list-rename-fn c$::block-item-list uid new-fn)))

Theorem: amb-expr/tyname-rename-fn-of-amb-expr/tyname-fix-amb-expr/tyname

(defthm
   amb-expr/tyname-rename-fn-of-amb-expr/tyname-fix-amb-expr/tyname
 (equal (amb-expr/tyname-rename-fn
             (c$::amb-expr/tyname-fix c$::amb-expr/tyname)
             uid new-fn)
        (amb-expr/tyname-rename-fn c$::amb-expr/tyname uid new-fn)))

Theorem: amb-expr/tyname-rename-fn-of-uid-fix-uid

(defthm amb-expr/tyname-rename-fn-of-uid-fix-uid
 (equal
    (amb-expr/tyname-rename-fn c$::amb-expr/tyname (c$::uid-fix uid)
                               new-fn)
    (amb-expr/tyname-rename-fn c$::amb-expr/tyname uid new-fn)))

Theorem: amb-expr/tyname-rename-fn-of-ident-fix-new-fn

(defthm amb-expr/tyname-rename-fn-of-ident-fix-new-fn
 (equal (amb-expr/tyname-rename-fn c$::amb-expr/tyname
                                   uid (ident-fix new-fn))
        (amb-expr/tyname-rename-fn c$::amb-expr/tyname uid new-fn)))

Theorem: amb-declor/absdeclor-rename-fn-of-amb-declor/absdeclor-fix-amb-declor/absdeclor

(defthm
 amb-declor/absdeclor-rename-fn-of-amb-declor/absdeclor-fix-amb-declor/absdeclor
 (equal (amb-declor/absdeclor-rename-fn
             (c$::amb-declor/absdeclor-fix c$::amb-declor/absdeclor)
             uid new-fn)
        (amb-declor/absdeclor-rename-fn
             c$::amb-declor/absdeclor uid new-fn)))

Theorem: amb-declor/absdeclor-rename-fn-of-uid-fix-uid

(defthm amb-declor/absdeclor-rename-fn-of-uid-fix-uid
  (equal (amb-declor/absdeclor-rename-fn c$::amb-declor/absdeclor
                                         (c$::uid-fix uid)
                                         new-fn)
         (amb-declor/absdeclor-rename-fn
              c$::amb-declor/absdeclor uid new-fn)))

Theorem: amb-declor/absdeclor-rename-fn-of-ident-fix-new-fn

(defthm amb-declor/absdeclor-rename-fn-of-ident-fix-new-fn
  (equal (amb-declor/absdeclor-rename-fn c$::amb-declor/absdeclor
                                         uid (ident-fix new-fn))
         (amb-declor/absdeclor-rename-fn
              c$::amb-declor/absdeclor uid new-fn)))

Theorem: amb-decl/stmt-rename-fn-of-amb-decl/stmt-fix-amb-decl/stmt

(defthm amb-decl/stmt-rename-fn-of-amb-decl/stmt-fix-amb-decl/stmt
 (equal
  (amb-decl/stmt-rename-fn (c$::amb-decl/stmt-fix c$::amb-decl/stmt)
                           uid new-fn)
  (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid new-fn)))

Theorem: amb-decl/stmt-rename-fn-of-uid-fix-uid

(defthm amb-decl/stmt-rename-fn-of-uid-fix-uid
 (equal (amb-decl/stmt-rename-fn c$::amb-decl/stmt (c$::uid-fix uid)
                                 new-fn)
        (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid new-fn)))

Theorem: amb-decl/stmt-rename-fn-of-ident-fix-new-fn

(defthm amb-decl/stmt-rename-fn-of-ident-fix-new-fn
  (equal (amb-decl/stmt-rename-fn c$::amb-decl/stmt
                                  uid (ident-fix new-fn))
         (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid new-fn)))

Theorem: expr-rename-fn-expr-equiv-congruence-on-expr

(defthm expr-rename-fn-expr-equiv-congruence-on-expr
  (implies (c$::expr-equiv c$::expr expr-equiv)
           (equal (expr-rename-fn c$::expr uid new-fn)
                  (expr-rename-fn expr-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: expr-rename-fn-uid-equiv-congruence-on-uid

(defthm expr-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (expr-rename-fn c$::expr uid new-fn)
                  (expr-rename-fn c$::expr uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: expr-rename-fn-ident-equiv-congruence-on-new-fn

(defthm expr-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (expr-rename-fn c$::expr uid new-fn)
                  (expr-rename-fn c$::expr uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: expr-list-rename-fn-expr-list-equiv-congruence-on-expr-list

(defthm expr-list-rename-fn-expr-list-equiv-congruence-on-expr-list
  (implies (c$::expr-list-equiv c$::expr-list expr-list-equiv)
           (equal (expr-list-rename-fn c$::expr-list uid new-fn)
                  (expr-list-rename-fn expr-list-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: expr-list-rename-fn-uid-equiv-congruence-on-uid

(defthm expr-list-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (expr-list-rename-fn c$::expr-list uid new-fn)
              (expr-list-rename-fn c$::expr-list uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: expr-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm expr-list-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (expr-list-rename-fn c$::expr-list uid new-fn)
              (expr-list-rename-fn c$::expr-list uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: expr-option-rename-fn-expr-option-equiv-congruence-on-expr-option

(defthm
  expr-option-rename-fn-expr-option-equiv-congruence-on-expr-option
  (implies
       (c$::expr-option-equiv c$::expr-option expr-option-equiv)
       (equal (expr-option-rename-fn c$::expr-option uid new-fn)
              (expr-option-rename-fn expr-option-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: expr-option-rename-fn-uid-equiv-congruence-on-uid

(defthm expr-option-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (expr-option-rename-fn c$::expr-option uid new-fn)
          (expr-option-rename-fn c$::expr-option uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: expr-option-rename-fn-ident-equiv-congruence-on-new-fn

(defthm expr-option-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (expr-option-rename-fn c$::expr-option uid new-fn)
          (expr-option-rename-fn c$::expr-option uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: const-expr-rename-fn-const-expr-equiv-congruence-on-const-expr

(defthm
     const-expr-rename-fn-const-expr-equiv-congruence-on-const-expr
  (implies
       (c$::const-expr-equiv const-expr const-expr-equiv)
       (equal (const-expr-rename-fn const-expr uid new-fn)
              (const-expr-rename-fn const-expr-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: const-expr-rename-fn-uid-equiv-congruence-on-uid

(defthm const-expr-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (const-expr-rename-fn const-expr uid new-fn)
              (const-expr-rename-fn const-expr uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: const-expr-rename-fn-ident-equiv-congruence-on-new-fn

(defthm const-expr-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (const-expr-rename-fn const-expr uid new-fn)
              (const-expr-rename-fn const-expr uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: const-expr-option-rename-fn-const-expr-option-equiv-congruence-on-const-expr-option

(defthm
 const-expr-option-rename-fn-const-expr-option-equiv-congruence-on-const-expr-option
 (implies
  (c$::const-expr-option-equiv c$::const-expr-option
                               const-expr-option-equiv)
  (equal
      (const-expr-option-rename-fn c$::const-expr-option uid new-fn)
      (const-expr-option-rename-fn
           const-expr-option-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: const-expr-option-rename-fn-uid-equiv-congruence-on-uid

(defthm const-expr-option-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
      (const-expr-option-rename-fn c$::const-expr-option uid new-fn)
      (const-expr-option-rename-fn c$::const-expr-option
                                   uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: const-expr-option-rename-fn-ident-equiv-congruence-on-new-fn

(defthm const-expr-option-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
      (const-expr-option-rename-fn c$::const-expr-option uid new-fn)
      (const-expr-option-rename-fn c$::const-expr-option
                                   uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: genassoc-rename-fn-genassoc-equiv-congruence-on-genassoc

(defthm genassoc-rename-fn-genassoc-equiv-congruence-on-genassoc
  (implies (c$::genassoc-equiv c$::genassoc genassoc-equiv)
           (equal (genassoc-rename-fn c$::genassoc uid new-fn)
                  (genassoc-rename-fn genassoc-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: genassoc-rename-fn-uid-equiv-congruence-on-uid

(defthm genassoc-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (genassoc-rename-fn c$::genassoc uid new-fn)
              (genassoc-rename-fn c$::genassoc uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: genassoc-rename-fn-ident-equiv-congruence-on-new-fn

(defthm genassoc-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (genassoc-rename-fn c$::genassoc uid new-fn)
              (genassoc-rename-fn c$::genassoc uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: genassoc-list-rename-fn-genassoc-list-equiv-congruence-on-genassoc-list

(defthm
 genassoc-list-rename-fn-genassoc-list-equiv-congruence-on-genassoc-list
 (implies
   (c$::genassoc-list-equiv c$::genassoc-list genassoc-list-equiv)
   (equal (genassoc-list-rename-fn c$::genassoc-list uid new-fn)
          (genassoc-list-rename-fn genassoc-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: genassoc-list-rename-fn-uid-equiv-congruence-on-uid

(defthm genassoc-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
      (genassoc-list-rename-fn c$::genassoc-list uid new-fn)
      (genassoc-list-rename-fn c$::genassoc-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: genassoc-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm genassoc-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
      (genassoc-list-rename-fn c$::genassoc-list uid new-fn)
      (genassoc-list-rename-fn c$::genassoc-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: member-designor-rename-fn-member-designor-equiv-congruence-on-member-designor

(defthm
 member-designor-rename-fn-member-designor-equiv-congruence-on-member-designor
 (implies
  (c$::member-designor-equiv c$::member-designor
                             member-designor-equiv)
  (equal
      (member-designor-rename-fn c$::member-designor uid new-fn)
      (member-designor-rename-fn member-designor-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: member-designor-rename-fn-uid-equiv-congruence-on-uid

(defthm member-designor-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (member-designor-rename-fn c$::member-designor uid new-fn)
          (member-designor-rename-fn
               c$::member-designor uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: member-designor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm member-designor-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (member-designor-rename-fn c$::member-designor uid new-fn)
          (member-designor-rename-fn
               c$::member-designor uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: type-spec-rename-fn-type-spec-equiv-congruence-on-type-spec

(defthm type-spec-rename-fn-type-spec-equiv-congruence-on-type-spec
  (implies (c$::type-spec-equiv c$::type-spec type-spec-equiv)
           (equal (type-spec-rename-fn c$::type-spec uid new-fn)
                  (type-spec-rename-fn type-spec-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: type-spec-rename-fn-uid-equiv-congruence-on-uid

(defthm type-spec-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (type-spec-rename-fn c$::type-spec uid new-fn)
              (type-spec-rename-fn c$::type-spec uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: type-spec-rename-fn-ident-equiv-congruence-on-new-fn

(defthm type-spec-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (type-spec-rename-fn c$::type-spec uid new-fn)
              (type-spec-rename-fn c$::type-spec uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: spec/qual-rename-fn-spec/qual-equiv-congruence-on-spec/qual

(defthm spec/qual-rename-fn-spec/qual-equiv-congruence-on-spec/qual
  (implies (c$::spec/qual-equiv c$::spec/qual spec/qual-equiv)
           (equal (spec/qual-rename-fn c$::spec/qual uid new-fn)
                  (spec/qual-rename-fn spec/qual-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: spec/qual-rename-fn-uid-equiv-congruence-on-uid

(defthm spec/qual-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (spec/qual-rename-fn c$::spec/qual uid new-fn)
              (spec/qual-rename-fn c$::spec/qual uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: spec/qual-rename-fn-ident-equiv-congruence-on-new-fn

(defthm spec/qual-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (spec/qual-rename-fn c$::spec/qual uid new-fn)
              (spec/qual-rename-fn c$::spec/qual uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: spec/qual-list-rename-fn-spec/qual-list-equiv-congruence-on-spec/qual-list

(defthm
 spec/qual-list-rename-fn-spec/qual-list-equiv-congruence-on-spec/qual-list
 (implies
  (c$::spec/qual-list-equiv c$::spec/qual-list spec/qual-list-equiv)
  (equal
       (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn)
       (spec/qual-list-rename-fn spec/qual-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: spec/qual-list-rename-fn-uid-equiv-congruence-on-uid

(defthm spec/qual-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
    (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn)
    (spec/qual-list-rename-fn c$::spec/qual-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: spec/qual-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm spec/qual-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
    (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn)
    (spec/qual-list-rename-fn c$::spec/qual-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: align-spec-rename-fn-align-spec-equiv-congruence-on-align-spec

(defthm
     align-spec-rename-fn-align-spec-equiv-congruence-on-align-spec
  (implies
       (c$::align-spec-equiv c$::align-spec align-spec-equiv)
       (equal (align-spec-rename-fn c$::align-spec uid new-fn)
              (align-spec-rename-fn align-spec-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: align-spec-rename-fn-uid-equiv-congruence-on-uid

(defthm align-spec-rename-fn-uid-equiv-congruence-on-uid
 (implies
     (c$::uid-equiv uid uid-equiv)
     (equal (align-spec-rename-fn c$::align-spec uid new-fn)
            (align-spec-rename-fn c$::align-spec uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: align-spec-rename-fn-ident-equiv-congruence-on-new-fn

(defthm align-spec-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
     (c$::ident-equiv new-fn new-fn-equiv)
     (equal (align-spec-rename-fn c$::align-spec uid new-fn)
            (align-spec-rename-fn c$::align-spec uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: decl-spec-rename-fn-decl-spec-equiv-congruence-on-decl-spec

(defthm decl-spec-rename-fn-decl-spec-equiv-congruence-on-decl-spec
  (implies (c$::decl-spec-equiv c$::decl-spec decl-spec-equiv)
           (equal (decl-spec-rename-fn c$::decl-spec uid new-fn)
                  (decl-spec-rename-fn decl-spec-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: decl-spec-rename-fn-uid-equiv-congruence-on-uid

(defthm decl-spec-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (decl-spec-rename-fn c$::decl-spec uid new-fn)
              (decl-spec-rename-fn c$::decl-spec uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: decl-spec-rename-fn-ident-equiv-congruence-on-new-fn

(defthm decl-spec-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (decl-spec-rename-fn c$::decl-spec uid new-fn)
              (decl-spec-rename-fn c$::decl-spec uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: decl-spec-list-rename-fn-decl-spec-list-equiv-congruence-on-decl-spec-list

(defthm
 decl-spec-list-rename-fn-decl-spec-list-equiv-congruence-on-decl-spec-list
 (implies
  (c$::decl-spec-list-equiv c$::decl-spec-list decl-spec-list-equiv)
  (equal
       (decl-spec-list-rename-fn c$::decl-spec-list uid new-fn)
       (decl-spec-list-rename-fn decl-spec-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: decl-spec-list-rename-fn-uid-equiv-congruence-on-uid

(defthm decl-spec-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
    (decl-spec-list-rename-fn c$::decl-spec-list uid new-fn)
    (decl-spec-list-rename-fn c$::decl-spec-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: decl-spec-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm decl-spec-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
    (decl-spec-list-rename-fn c$::decl-spec-list uid new-fn)
    (decl-spec-list-rename-fn c$::decl-spec-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-rename-fn-typequal/attribspec-equiv-congruence-on-typequal/attribspec

(defthm
 typequal/attribspec-rename-fn-typequal/attribspec-equiv-congruence-on-typequal/attribspec
 (implies (c$::typequal/attribspec-equiv c$::typequal/attribspec
                                         typequal/attribspec-equiv)
          (equal (typequal/attribspec-rename-fn
                      c$::typequal/attribspec uid new-fn)
                 (typequal/attribspec-rename-fn
                      typequal/attribspec-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-rename-fn-uid-equiv-congruence-on-uid

(defthm typequal/attribspec-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (typequal/attribspec-rename-fn
                   c$::typequal/attribspec uid new-fn)
              (typequal/attribspec-rename-fn c$::typequal/attribspec
                                             uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: typequal/attribspec-rename-fn-ident-equiv-congruence-on-new-fn

(defthm
     typequal/attribspec-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (typequal/attribspec-rename-fn
                   c$::typequal/attribspec uid new-fn)
              (typequal/attribspec-rename-fn c$::typequal/attribspec
                                             uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: typequal/attribspec-list-rename-fn-typequal/attribspec-list-equiv-congruence-on-typequal/attribspec-list

(defthm
 typequal/attribspec-list-rename-fn-typequal/attribspec-list-equiv-congruence-on-typequal/attribspec-list
 (implies (c$::typequal/attribspec-list-equiv
               c$::typequal/attribspec-list
               typequal/attribspec-list-equiv)
          (equal (typequal/attribspec-list-rename-fn
                      c$::typequal/attribspec-list uid new-fn)
                 (typequal/attribspec-list-rename-fn
                      typequal/attribspec-list-equiv
                      uid new-fn)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-rename-fn-uid-equiv-congruence-on-uid

(defthm
     typequal/attribspec-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
    (typequal/attribspec-list-rename-fn
         c$::typequal/attribspec-list uid new-fn)
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm
 typequal/attribspec-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
    (typequal/attribspec-list-rename-fn
         c$::typequal/attribspec-list uid new-fn)
    (typequal/attribspec-list-rename-fn c$::typequal/attribspec-list
                                        uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-list-rename-fn-typequal/attribspec-list-list-equiv-congruence-on-typequal/attribspec-list-list

(defthm
 typequal/attribspec-list-list-rename-fn-typequal/attribspec-list-list-equiv-congruence-on-typequal/attribspec-list-list
 (implies (c$::typequal/attribspec-list-list-equiv
               c$::typequal/attribspec-list-list
               typequal/attribspec-list-list-equiv)
          (equal (typequal/attribspec-list-list-rename-fn
                      c$::typequal/attribspec-list-list
                      uid new-fn)
                 (typequal/attribspec-list-list-rename-fn
                      typequal/attribspec-list-list-equiv
                      uid new-fn)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-list-rename-fn-uid-equiv-congruence-on-uid

(defthm
 typequal/attribspec-list-list-rename-fn-uid-equiv-congruence-on-uid
 (implies (c$::uid-equiv uid uid-equiv)
          (equal (typequal/attribspec-list-list-rename-fn
                      c$::typequal/attribspec-list-list
                      uid new-fn)
                 (typequal/attribspec-list-list-rename-fn
                      c$::typequal/attribspec-list-list
                      uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm
 typequal/attribspec-list-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies (c$::ident-equiv new-fn new-fn-equiv)
          (equal (typequal/attribspec-list-list-rename-fn
                      c$::typequal/attribspec-list-list
                      uid new-fn)
                 (typequal/attribspec-list-list-rename-fn
                      c$::typequal/attribspec-list-list
                      uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: initer-rename-fn-initer-equiv-congruence-on-initer

(defthm initer-rename-fn-initer-equiv-congruence-on-initer
  (implies (c$::initer-equiv c$::initer initer-equiv)
           (equal (initer-rename-fn c$::initer uid new-fn)
                  (initer-rename-fn initer-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: initer-rename-fn-uid-equiv-congruence-on-uid

(defthm initer-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (initer-rename-fn c$::initer uid new-fn)
                  (initer-rename-fn c$::initer uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: initer-rename-fn-ident-equiv-congruence-on-new-fn

(defthm initer-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (initer-rename-fn c$::initer uid new-fn)
                  (initer-rename-fn c$::initer uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: initer-option-rename-fn-initer-option-equiv-congruence-on-initer-option

(defthm
 initer-option-rename-fn-initer-option-equiv-congruence-on-initer-option
 (implies
   (c$::initer-option-equiv c$::initer-option initer-option-equiv)
   (equal (initer-option-rename-fn c$::initer-option uid new-fn)
          (initer-option-rename-fn initer-option-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: initer-option-rename-fn-uid-equiv-congruence-on-uid

(defthm initer-option-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
      (initer-option-rename-fn c$::initer-option uid new-fn)
      (initer-option-rename-fn c$::initer-option uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: initer-option-rename-fn-ident-equiv-congruence-on-new-fn

(defthm initer-option-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
      (initer-option-rename-fn c$::initer-option uid new-fn)
      (initer-option-rename-fn c$::initer-option uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: desiniter-rename-fn-desiniter-equiv-congruence-on-desiniter

(defthm desiniter-rename-fn-desiniter-equiv-congruence-on-desiniter
  (implies (c$::desiniter-equiv desiniter desiniter-equiv)
           (equal (desiniter-rename-fn desiniter uid new-fn)
                  (desiniter-rename-fn desiniter-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: desiniter-rename-fn-uid-equiv-congruence-on-uid

(defthm desiniter-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (desiniter-rename-fn desiniter uid new-fn)
                  (desiniter-rename-fn desiniter uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: desiniter-rename-fn-ident-equiv-congruence-on-new-fn

(defthm desiniter-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (desiniter-rename-fn desiniter uid new-fn)
                  (desiniter-rename-fn desiniter uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: desiniter-list-rename-fn-desiniter-list-equiv-congruence-on-desiniter-list

(defthm
 desiniter-list-rename-fn-desiniter-list-equiv-congruence-on-desiniter-list
 (implies
  (c$::desiniter-list-equiv c$::desiniter-list desiniter-list-equiv)
  (equal
       (desiniter-list-rename-fn c$::desiniter-list uid new-fn)
       (desiniter-list-rename-fn desiniter-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: desiniter-list-rename-fn-uid-equiv-congruence-on-uid

(defthm desiniter-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
    (desiniter-list-rename-fn c$::desiniter-list uid new-fn)
    (desiniter-list-rename-fn c$::desiniter-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: desiniter-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm desiniter-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
    (desiniter-list-rename-fn c$::desiniter-list uid new-fn)
    (desiniter-list-rename-fn c$::desiniter-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: designor-rename-fn-designor-equiv-congruence-on-designor

(defthm designor-rename-fn-designor-equiv-congruence-on-designor
  (implies (c$::designor-equiv c$::designor designor-equiv)
           (equal (designor-rename-fn c$::designor uid new-fn)
                  (designor-rename-fn designor-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: designor-rename-fn-uid-equiv-congruence-on-uid

(defthm designor-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (designor-rename-fn c$::designor uid new-fn)
              (designor-rename-fn c$::designor uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: designor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm designor-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (designor-rename-fn c$::designor uid new-fn)
              (designor-rename-fn c$::designor uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: designor-list-rename-fn-designor-list-equiv-congruence-on-designor-list

(defthm
 designor-list-rename-fn-designor-list-equiv-congruence-on-designor-list
 (implies
   (c$::designor-list-equiv c$::designor-list designor-list-equiv)
   (equal (designor-list-rename-fn c$::designor-list uid new-fn)
          (designor-list-rename-fn designor-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: designor-list-rename-fn-uid-equiv-congruence-on-uid

(defthm designor-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
      (designor-list-rename-fn c$::designor-list uid new-fn)
      (designor-list-rename-fn c$::designor-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: designor-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm designor-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
      (designor-list-rename-fn c$::designor-list uid new-fn)
      (designor-list-rename-fn c$::designor-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: declor-rename-fn-declor-equiv-congruence-on-declor

(defthm declor-rename-fn-declor-equiv-congruence-on-declor
  (implies (c$::declor-equiv declor declor-equiv)
           (equal (declor-rename-fn declor uid new-fn)
                  (declor-rename-fn declor-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: declor-rename-fn-uid-equiv-congruence-on-uid

(defthm declor-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (declor-rename-fn declor uid new-fn)
                  (declor-rename-fn declor uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: declor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm declor-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (declor-rename-fn declor uid new-fn)
                  (declor-rename-fn declor uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: declor-option-rename-fn-declor-option-equiv-congruence-on-declor-option

(defthm
 declor-option-rename-fn-declor-option-equiv-congruence-on-declor-option
 (implies
   (c$::declor-option-equiv c$::declor-option declor-option-equiv)
   (equal (declor-option-rename-fn c$::declor-option uid new-fn)
          (declor-option-rename-fn declor-option-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: declor-option-rename-fn-uid-equiv-congruence-on-uid

(defthm declor-option-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
      (declor-option-rename-fn c$::declor-option uid new-fn)
      (declor-option-rename-fn c$::declor-option uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: declor-option-rename-fn-ident-equiv-congruence-on-new-fn

(defthm declor-option-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
      (declor-option-rename-fn c$::declor-option uid new-fn)
      (declor-option-rename-fn c$::declor-option uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: dirdeclor-rename-fn-dirdeclor-equiv-congruence-on-dirdeclor

(defthm dirdeclor-rename-fn-dirdeclor-equiv-congruence-on-dirdeclor
  (implies (c$::dirdeclor-equiv dirdeclor dirdeclor-equiv)
           (equal (dirdeclor-rename-fn dirdeclor uid new-fn)
                  (dirdeclor-rename-fn dirdeclor-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: dirdeclor-rename-fn-uid-equiv-congruence-on-uid

(defthm dirdeclor-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (dirdeclor-rename-fn dirdeclor uid new-fn)
                  (dirdeclor-rename-fn dirdeclor uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: dirdeclor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm dirdeclor-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (dirdeclor-rename-fn dirdeclor uid new-fn)
                  (dirdeclor-rename-fn dirdeclor uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: absdeclor-rename-fn-absdeclor-equiv-congruence-on-absdeclor

(defthm absdeclor-rename-fn-absdeclor-equiv-congruence-on-absdeclor
  (implies (c$::absdeclor-equiv absdeclor absdeclor-equiv)
           (equal (absdeclor-rename-fn absdeclor uid new-fn)
                  (absdeclor-rename-fn absdeclor-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: absdeclor-rename-fn-uid-equiv-congruence-on-uid

(defthm absdeclor-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (absdeclor-rename-fn absdeclor uid new-fn)
                  (absdeclor-rename-fn absdeclor uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: absdeclor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm absdeclor-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (absdeclor-rename-fn absdeclor uid new-fn)
                  (absdeclor-rename-fn absdeclor uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: absdeclor-option-rename-fn-absdeclor-option-equiv-congruence-on-absdeclor-option

(defthm
 absdeclor-option-rename-fn-absdeclor-option-equiv-congruence-on-absdeclor-option
 (implies
  (c$::absdeclor-option-equiv c$::absdeclor-option
                              absdeclor-option-equiv)
  (equal
    (absdeclor-option-rename-fn c$::absdeclor-option uid new-fn)
    (absdeclor-option-rename-fn absdeclor-option-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: absdeclor-option-rename-fn-uid-equiv-congruence-on-uid

(defthm absdeclor-option-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal
        (absdeclor-option-rename-fn c$::absdeclor-option uid new-fn)
        (absdeclor-option-rename-fn
             c$::absdeclor-option uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: absdeclor-option-rename-fn-ident-equiv-congruence-on-new-fn

(defthm absdeclor-option-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal
        (absdeclor-option-rename-fn c$::absdeclor-option uid new-fn)
        (absdeclor-option-rename-fn
             c$::absdeclor-option uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-rename-fn-dirabsdeclor-equiv-congruence-on-dirabsdeclor

(defthm
 dirabsdeclor-rename-fn-dirabsdeclor-equiv-congruence-on-dirabsdeclor
 (implies
     (c$::dirabsdeclor-equiv c$::dirabsdeclor dirabsdeclor-equiv)
     (equal (dirabsdeclor-rename-fn c$::dirabsdeclor uid new-fn)
            (dirabsdeclor-rename-fn dirabsdeclor-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-rename-fn-uid-equiv-congruence-on-uid

(defthm dirabsdeclor-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal
        (dirabsdeclor-rename-fn c$::dirabsdeclor uid new-fn)
        (dirabsdeclor-rename-fn c$::dirabsdeclor uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm dirabsdeclor-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal
        (dirabsdeclor-rename-fn c$::dirabsdeclor uid new-fn)
        (dirabsdeclor-rename-fn c$::dirabsdeclor uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-option-rename-fn-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor-option

(defthm
 dirabsdeclor-option-rename-fn-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor-option
 (implies (c$::dirabsdeclor-option-equiv c$::dirabsdeclor-option
                                         dirabsdeclor-option-equiv)
          (equal (dirabsdeclor-option-rename-fn
                      c$::dirabsdeclor-option uid new-fn)
                 (dirabsdeclor-option-rename-fn
                      dirabsdeclor-option-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-option-rename-fn-uid-equiv-congruence-on-uid

(defthm dirabsdeclor-option-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (dirabsdeclor-option-rename-fn
                   c$::dirabsdeclor-option uid new-fn)
              (dirabsdeclor-option-rename-fn c$::dirabsdeclor-option
                                             uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: dirabsdeclor-option-rename-fn-ident-equiv-congruence-on-new-fn

(defthm
     dirabsdeclor-option-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (dirabsdeclor-option-rename-fn
                   c$::dirabsdeclor-option uid new-fn)
              (dirabsdeclor-option-rename-fn c$::dirabsdeclor-option
                                             uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: param-declon-rename-fn-param-declon-equiv-congruence-on-param-declon

(defthm
 param-declon-rename-fn-param-declon-equiv-congruence-on-param-declon
 (implies
     (c$::param-declon-equiv param-declon param-declon-equiv)
     (equal (param-declon-rename-fn param-declon uid new-fn)
            (param-declon-rename-fn param-declon-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: param-declon-rename-fn-uid-equiv-congruence-on-uid

(defthm param-declon-rename-fn-uid-equiv-congruence-on-uid
 (implies
     (c$::uid-equiv uid uid-equiv)
     (equal (param-declon-rename-fn param-declon uid new-fn)
            (param-declon-rename-fn param-declon uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: param-declon-rename-fn-ident-equiv-congruence-on-new-fn

(defthm param-declon-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
     (c$::ident-equiv new-fn new-fn-equiv)
     (equal (param-declon-rename-fn param-declon uid new-fn)
            (param-declon-rename-fn param-declon uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: param-declon-list-rename-fn-param-declon-list-equiv-congruence-on-param-declon-list

(defthm
 param-declon-list-rename-fn-param-declon-list-equiv-congruence-on-param-declon-list
 (implies
  (c$::param-declon-list-equiv c$::param-declon-list
                               param-declon-list-equiv)
  (equal
      (param-declon-list-rename-fn c$::param-declon-list uid new-fn)
      (param-declon-list-rename-fn
           param-declon-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: param-declon-list-rename-fn-uid-equiv-congruence-on-uid

(defthm param-declon-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
      (param-declon-list-rename-fn c$::param-declon-list uid new-fn)
      (param-declon-list-rename-fn c$::param-declon-list
                                   uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: param-declon-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm param-declon-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
      (param-declon-list-rename-fn c$::param-declon-list uid new-fn)
      (param-declon-list-rename-fn c$::param-declon-list
                                   uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: param-declor-rename-fn-param-declor-equiv-congruence-on-param-declor

(defthm
 param-declor-rename-fn-param-declor-equiv-congruence-on-param-declor
 (implies
     (c$::param-declor-equiv c$::param-declor param-declor-equiv)
     (equal (param-declor-rename-fn c$::param-declor uid new-fn)
            (param-declor-rename-fn param-declor-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: param-declor-rename-fn-uid-equiv-congruence-on-uid

(defthm param-declor-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal
        (param-declor-rename-fn c$::param-declor uid new-fn)
        (param-declor-rename-fn c$::param-declor uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: param-declor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm param-declor-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal
        (param-declor-rename-fn c$::param-declor uid new-fn)
        (param-declor-rename-fn c$::param-declor uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: tyname-rename-fn-tyname-equiv-congruence-on-tyname

(defthm tyname-rename-fn-tyname-equiv-congruence-on-tyname
  (implies (c$::tyname-equiv tyname tyname-equiv)
           (equal (tyname-rename-fn tyname uid new-fn)
                  (tyname-rename-fn tyname-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: tyname-rename-fn-uid-equiv-congruence-on-uid

(defthm tyname-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (tyname-rename-fn tyname uid new-fn)
                  (tyname-rename-fn tyname uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: tyname-rename-fn-ident-equiv-congruence-on-new-fn

(defthm tyname-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (tyname-rename-fn tyname uid new-fn)
                  (tyname-rename-fn tyname uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: struni-spec-rename-fn-struni-spec-equiv-congruence-on-struni-spec

(defthm
  struni-spec-rename-fn-struni-spec-equiv-congruence-on-struni-spec
  (implies
       (c$::struni-spec-equiv struni-spec struni-spec-equiv)
       (equal (struni-spec-rename-fn struni-spec uid new-fn)
              (struni-spec-rename-fn struni-spec-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: struni-spec-rename-fn-uid-equiv-congruence-on-uid

(defthm struni-spec-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (struni-spec-rename-fn struni-spec uid new-fn)
              (struni-spec-rename-fn struni-spec uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: struni-spec-rename-fn-ident-equiv-congruence-on-new-fn

(defthm struni-spec-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (struni-spec-rename-fn struni-spec uid new-fn)
              (struni-spec-rename-fn struni-spec uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: struct-declon-rename-fn-struct-declon-equiv-congruence-on-struct-declon

(defthm
 struct-declon-rename-fn-struct-declon-equiv-congruence-on-struct-declon
 (implies
   (c$::struct-declon-equiv c$::struct-declon struct-declon-equiv)
   (equal (struct-declon-rename-fn c$::struct-declon uid new-fn)
          (struct-declon-rename-fn struct-declon-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: struct-declon-rename-fn-uid-equiv-congruence-on-uid

(defthm struct-declon-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
      (struct-declon-rename-fn c$::struct-declon uid new-fn)
      (struct-declon-rename-fn c$::struct-declon uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: struct-declon-rename-fn-ident-equiv-congruence-on-new-fn

(defthm struct-declon-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
      (struct-declon-rename-fn c$::struct-declon uid new-fn)
      (struct-declon-rename-fn c$::struct-declon uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: struct-declon-list-rename-fn-struct-declon-list-equiv-congruence-on-struct-declon-list

(defthm
 struct-declon-list-rename-fn-struct-declon-list-equiv-congruence-on-struct-declon-list
 (implies
  (c$::struct-declon-list-equiv c$::struct-declon-list
                                struct-declon-list-equiv)
  (equal
    (struct-declon-list-rename-fn c$::struct-declon-list uid new-fn)
    (struct-declon-list-rename-fn
         struct-declon-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: struct-declon-list-rename-fn-uid-equiv-congruence-on-uid

(defthm struct-declon-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
    (struct-declon-list-rename-fn c$::struct-declon-list uid new-fn)
    (struct-declon-list-rename-fn c$::struct-declon-list
                                  uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: struct-declon-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm
      struct-declon-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
    (struct-declon-list-rename-fn c$::struct-declon-list uid new-fn)
    (struct-declon-list-rename-fn c$::struct-declon-list
                                  uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: struct-declor-rename-fn-struct-declor-equiv-congruence-on-struct-declor

(defthm
 struct-declor-rename-fn-struct-declor-equiv-congruence-on-struct-declor
 (implies
   (c$::struct-declor-equiv struct-declor struct-declor-equiv)
   (equal (struct-declor-rename-fn struct-declor uid new-fn)
          (struct-declor-rename-fn struct-declor-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: struct-declor-rename-fn-uid-equiv-congruence-on-uid

(defthm struct-declor-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (struct-declor-rename-fn struct-declor uid new-fn)
          (struct-declor-rename-fn struct-declor uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: struct-declor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm struct-declor-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (struct-declor-rename-fn struct-declor uid new-fn)
          (struct-declor-rename-fn struct-declor uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: struct-declor-list-rename-fn-struct-declor-list-equiv-congruence-on-struct-declor-list

(defthm
 struct-declor-list-rename-fn-struct-declor-list-equiv-congruence-on-struct-declor-list
 (implies
  (c$::struct-declor-list-equiv c$::struct-declor-list
                                struct-declor-list-equiv)
  (equal
    (struct-declor-list-rename-fn c$::struct-declor-list uid new-fn)
    (struct-declor-list-rename-fn
         struct-declor-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: struct-declor-list-rename-fn-uid-equiv-congruence-on-uid

(defthm struct-declor-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
    (struct-declor-list-rename-fn c$::struct-declor-list uid new-fn)
    (struct-declor-list-rename-fn c$::struct-declor-list
                                  uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: struct-declor-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm
      struct-declor-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
    (struct-declor-list-rename-fn c$::struct-declor-list uid new-fn)
    (struct-declor-list-rename-fn c$::struct-declor-list
                                  uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: enum-spec-rename-fn-enum-spec-equiv-congruence-on-enum-spec

(defthm enum-spec-rename-fn-enum-spec-equiv-congruence-on-enum-spec
  (implies (c$::enum-spec-equiv enum-spec enum-spec-equiv)
           (equal (enum-spec-rename-fn enum-spec uid new-fn)
                  (enum-spec-rename-fn enum-spec-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: enum-spec-rename-fn-uid-equiv-congruence-on-uid

(defthm enum-spec-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (enum-spec-rename-fn enum-spec uid new-fn)
                  (enum-spec-rename-fn enum-spec uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: enum-spec-rename-fn-ident-equiv-congruence-on-new-fn

(defthm enum-spec-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (enum-spec-rename-fn enum-spec uid new-fn)
                  (enum-spec-rename-fn enum-spec uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: enumer-rename-fn-enumer-equiv-congruence-on-enumer

(defthm enumer-rename-fn-enumer-equiv-congruence-on-enumer
  (implies (c$::enumer-equiv enumer enumer-equiv)
           (equal (enumer-rename-fn enumer uid new-fn)
                  (enumer-rename-fn enumer-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: enumer-rename-fn-uid-equiv-congruence-on-uid

(defthm enumer-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (enumer-rename-fn enumer uid new-fn)
                  (enumer-rename-fn enumer uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: enumer-rename-fn-ident-equiv-congruence-on-new-fn

(defthm enumer-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (enumer-rename-fn enumer uid new-fn)
                  (enumer-rename-fn enumer uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: enumer-list-rename-fn-enumer-list-equiv-congruence-on-enumer-list

(defthm
  enumer-list-rename-fn-enumer-list-equiv-congruence-on-enumer-list
  (implies
       (c$::enumer-list-equiv c$::enumer-list enumer-list-equiv)
       (equal (enumer-list-rename-fn c$::enumer-list uid new-fn)
              (enumer-list-rename-fn enumer-list-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: enumer-list-rename-fn-uid-equiv-congruence-on-uid

(defthm enumer-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (enumer-list-rename-fn c$::enumer-list uid new-fn)
          (enumer-list-rename-fn c$::enumer-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: enumer-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm enumer-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (enumer-list-rename-fn c$::enumer-list uid new-fn)
          (enumer-list-rename-fn c$::enumer-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: statassert-rename-fn-statassert-equiv-congruence-on-statassert

(defthm
     statassert-rename-fn-statassert-equiv-congruence-on-statassert
  (implies
       (c$::statassert-equiv statassert statassert-equiv)
       (equal (statassert-rename-fn statassert uid new-fn)
              (statassert-rename-fn statassert-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: statassert-rename-fn-uid-equiv-congruence-on-uid

(defthm statassert-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (statassert-rename-fn statassert uid new-fn)
              (statassert-rename-fn statassert uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: statassert-rename-fn-ident-equiv-congruence-on-new-fn

(defthm statassert-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (statassert-rename-fn statassert uid new-fn)
              (statassert-rename-fn statassert uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: attrib-rename-fn-attrib-equiv-congruence-on-attrib

(defthm attrib-rename-fn-attrib-equiv-congruence-on-attrib
  (implies (c$::attrib-equiv c$::attrib attrib-equiv)
           (equal (attrib-rename-fn c$::attrib uid new-fn)
                  (attrib-rename-fn attrib-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: attrib-rename-fn-uid-equiv-congruence-on-uid

(defthm attrib-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (attrib-rename-fn c$::attrib uid new-fn)
                  (attrib-rename-fn c$::attrib uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: attrib-rename-fn-ident-equiv-congruence-on-new-fn

(defthm attrib-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (attrib-rename-fn c$::attrib uid new-fn)
                  (attrib-rename-fn c$::attrib uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: attrib-list-rename-fn-attrib-list-equiv-congruence-on-attrib-list

(defthm
  attrib-list-rename-fn-attrib-list-equiv-congruence-on-attrib-list
  (implies
       (c$::attrib-list-equiv c$::attrib-list attrib-list-equiv)
       (equal (attrib-list-rename-fn c$::attrib-list uid new-fn)
              (attrib-list-rename-fn attrib-list-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: attrib-list-rename-fn-uid-equiv-congruence-on-uid

(defthm attrib-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (attrib-list-rename-fn c$::attrib-list uid new-fn)
          (attrib-list-rename-fn c$::attrib-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: attrib-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm attrib-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (attrib-list-rename-fn c$::attrib-list uid new-fn)
          (attrib-list-rename-fn c$::attrib-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: attrib-spec-rename-fn-attrib-spec-equiv-congruence-on-attrib-spec

(defthm
  attrib-spec-rename-fn-attrib-spec-equiv-congruence-on-attrib-spec
  (implies
       (c$::attrib-spec-equiv c$::attrib-spec attrib-spec-equiv)
       (equal (attrib-spec-rename-fn c$::attrib-spec uid new-fn)
              (attrib-spec-rename-fn attrib-spec-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: attrib-spec-rename-fn-uid-equiv-congruence-on-uid

(defthm attrib-spec-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (attrib-spec-rename-fn c$::attrib-spec uid new-fn)
          (attrib-spec-rename-fn c$::attrib-spec uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: attrib-spec-rename-fn-ident-equiv-congruence-on-new-fn

(defthm attrib-spec-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (attrib-spec-rename-fn c$::attrib-spec uid new-fn)
          (attrib-spec-rename-fn c$::attrib-spec uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: attrib-spec-list-rename-fn-attrib-spec-list-equiv-congruence-on-attrib-spec-list

(defthm
 attrib-spec-list-rename-fn-attrib-spec-list-equiv-congruence-on-attrib-spec-list
 (implies
  (c$::attrib-spec-list-equiv c$::attrib-spec-list
                              attrib-spec-list-equiv)
  (equal
    (attrib-spec-list-rename-fn c$::attrib-spec-list uid new-fn)
    (attrib-spec-list-rename-fn attrib-spec-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: attrib-spec-list-rename-fn-uid-equiv-congruence-on-uid

(defthm attrib-spec-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal
        (attrib-spec-list-rename-fn c$::attrib-spec-list uid new-fn)
        (attrib-spec-list-rename-fn
             c$::attrib-spec-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: attrib-spec-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm attrib-spec-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal
        (attrib-spec-list-rename-fn c$::attrib-spec-list uid new-fn)
        (attrib-spec-list-rename-fn
             c$::attrib-spec-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: initdeclor-rename-fn-initdeclor-equiv-congruence-on-initdeclor

(defthm
     initdeclor-rename-fn-initdeclor-equiv-congruence-on-initdeclor
  (implies
       (c$::initdeclor-equiv initdeclor initdeclor-equiv)
       (equal (initdeclor-rename-fn initdeclor uid new-fn)
              (initdeclor-rename-fn initdeclor-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: initdeclor-rename-fn-uid-equiv-congruence-on-uid

(defthm initdeclor-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (initdeclor-rename-fn initdeclor uid new-fn)
              (initdeclor-rename-fn initdeclor uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: initdeclor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm initdeclor-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (initdeclor-rename-fn initdeclor uid new-fn)
              (initdeclor-rename-fn initdeclor uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: initdeclor-list-rename-fn-initdeclor-list-equiv-congruence-on-initdeclor-list

(defthm
 initdeclor-list-rename-fn-initdeclor-list-equiv-congruence-on-initdeclor-list
 (implies
  (c$::initdeclor-list-equiv c$::initdeclor-list
                             initdeclor-list-equiv)
  (equal
      (initdeclor-list-rename-fn c$::initdeclor-list uid new-fn)
      (initdeclor-list-rename-fn initdeclor-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: initdeclor-list-rename-fn-uid-equiv-congruence-on-uid

(defthm initdeclor-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (initdeclor-list-rename-fn c$::initdeclor-list uid new-fn)
          (initdeclor-list-rename-fn
               c$::initdeclor-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: initdeclor-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm initdeclor-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (initdeclor-list-rename-fn c$::initdeclor-list uid new-fn)
          (initdeclor-list-rename-fn
               c$::initdeclor-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: decl-rename-fn-decl-equiv-congruence-on-decl

(defthm decl-rename-fn-decl-equiv-congruence-on-decl
  (implies (c$::decl-equiv decl decl-equiv)
           (equal (decl-rename-fn decl uid new-fn)
                  (decl-rename-fn decl-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: decl-rename-fn-uid-equiv-congruence-on-uid

(defthm decl-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (decl-rename-fn decl uid new-fn)
                  (decl-rename-fn decl uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: decl-rename-fn-ident-equiv-congruence-on-new-fn

(defthm decl-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (decl-rename-fn decl uid new-fn)
                  (decl-rename-fn decl uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: decl-list-rename-fn-decl-list-equiv-congruence-on-decl-list

(defthm decl-list-rename-fn-decl-list-equiv-congruence-on-decl-list
  (implies (c$::decl-list-equiv c$::decl-list decl-list-equiv)
           (equal (decl-list-rename-fn c$::decl-list uid new-fn)
                  (decl-list-rename-fn decl-list-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: decl-list-rename-fn-uid-equiv-congruence-on-uid

(defthm decl-list-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (decl-list-rename-fn c$::decl-list uid new-fn)
              (decl-list-rename-fn c$::decl-list uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: decl-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm decl-list-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (decl-list-rename-fn c$::decl-list uid new-fn)
              (decl-list-rename-fn c$::decl-list uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: label-rename-fn-label-equiv-congruence-on-label

(defthm label-rename-fn-label-equiv-congruence-on-label
  (implies (c$::label-equiv c$::label label-equiv)
           (equal (label-rename-fn c$::label uid new-fn)
                  (label-rename-fn label-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: label-rename-fn-uid-equiv-congruence-on-uid

(defthm label-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (label-rename-fn c$::label uid new-fn)
                  (label-rename-fn c$::label uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: label-rename-fn-ident-equiv-congruence-on-new-fn

(defthm label-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (label-rename-fn c$::label uid new-fn)
                  (label-rename-fn c$::label uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: asm-output-rename-fn-asm-output-equiv-congruence-on-asm-output

(defthm
     asm-output-rename-fn-asm-output-equiv-congruence-on-asm-output
  (implies
       (c$::asm-output-equiv c$::asm-output asm-output-equiv)
       (equal (asm-output-rename-fn c$::asm-output uid new-fn)
              (asm-output-rename-fn asm-output-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: asm-output-rename-fn-uid-equiv-congruence-on-uid

(defthm asm-output-rename-fn-uid-equiv-congruence-on-uid
 (implies
     (c$::uid-equiv uid uid-equiv)
     (equal (asm-output-rename-fn c$::asm-output uid new-fn)
            (asm-output-rename-fn c$::asm-output uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: asm-output-rename-fn-ident-equiv-congruence-on-new-fn

(defthm asm-output-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
     (c$::ident-equiv new-fn new-fn-equiv)
     (equal (asm-output-rename-fn c$::asm-output uid new-fn)
            (asm-output-rename-fn c$::asm-output uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: asm-output-list-rename-fn-asm-output-list-equiv-congruence-on-asm-output-list

(defthm
 asm-output-list-rename-fn-asm-output-list-equiv-congruence-on-asm-output-list
 (implies
  (c$::asm-output-list-equiv c$::asm-output-list
                             asm-output-list-equiv)
  (equal
      (asm-output-list-rename-fn c$::asm-output-list uid new-fn)
      (asm-output-list-rename-fn asm-output-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: asm-output-list-rename-fn-uid-equiv-congruence-on-uid

(defthm asm-output-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (asm-output-list-rename-fn c$::asm-output-list uid new-fn)
          (asm-output-list-rename-fn
               c$::asm-output-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: asm-output-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm asm-output-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (asm-output-list-rename-fn c$::asm-output-list uid new-fn)
          (asm-output-list-rename-fn
               c$::asm-output-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: asm-input-rename-fn-asm-input-equiv-congruence-on-asm-input

(defthm asm-input-rename-fn-asm-input-equiv-congruence-on-asm-input
  (implies (c$::asm-input-equiv c$::asm-input asm-input-equiv)
           (equal (asm-input-rename-fn c$::asm-input uid new-fn)
                  (asm-input-rename-fn asm-input-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: asm-input-rename-fn-uid-equiv-congruence-on-uid

(defthm asm-input-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (asm-input-rename-fn c$::asm-input uid new-fn)
              (asm-input-rename-fn c$::asm-input uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: asm-input-rename-fn-ident-equiv-congruence-on-new-fn

(defthm asm-input-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (asm-input-rename-fn c$::asm-input uid new-fn)
              (asm-input-rename-fn c$::asm-input uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: asm-input-list-rename-fn-asm-input-list-equiv-congruence-on-asm-input-list

(defthm
 asm-input-list-rename-fn-asm-input-list-equiv-congruence-on-asm-input-list
 (implies
  (c$::asm-input-list-equiv c$::asm-input-list asm-input-list-equiv)
  (equal
       (asm-input-list-rename-fn c$::asm-input-list uid new-fn)
       (asm-input-list-rename-fn asm-input-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: asm-input-list-rename-fn-uid-equiv-congruence-on-uid

(defthm asm-input-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
    (asm-input-list-rename-fn c$::asm-input-list uid new-fn)
    (asm-input-list-rename-fn c$::asm-input-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: asm-input-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm asm-input-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
    (asm-input-list-rename-fn c$::asm-input-list uid new-fn)
    (asm-input-list-rename-fn c$::asm-input-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: asm-stmt-rename-fn-asm-stmt-equiv-congruence-on-asm-stmt

(defthm asm-stmt-rename-fn-asm-stmt-equiv-congruence-on-asm-stmt
  (implies (c$::asm-stmt-equiv c$::asm-stmt asm-stmt-equiv)
           (equal (asm-stmt-rename-fn c$::asm-stmt uid new-fn)
                  (asm-stmt-rename-fn asm-stmt-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: asm-stmt-rename-fn-uid-equiv-congruence-on-uid

(defthm asm-stmt-rename-fn-uid-equiv-congruence-on-uid
  (implies
       (c$::uid-equiv uid uid-equiv)
       (equal (asm-stmt-rename-fn c$::asm-stmt uid new-fn)
              (asm-stmt-rename-fn c$::asm-stmt uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: asm-stmt-rename-fn-ident-equiv-congruence-on-new-fn

(defthm asm-stmt-rename-fn-ident-equiv-congruence-on-new-fn
  (implies
       (c$::ident-equiv new-fn new-fn-equiv)
       (equal (asm-stmt-rename-fn c$::asm-stmt uid new-fn)
              (asm-stmt-rename-fn c$::asm-stmt uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: stmt-rename-fn-stmt-equiv-congruence-on-stmt

(defthm stmt-rename-fn-stmt-equiv-congruence-on-stmt
  (implies (c$::stmt-equiv c$::stmt stmt-equiv)
           (equal (stmt-rename-fn c$::stmt uid new-fn)
                  (stmt-rename-fn stmt-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: stmt-rename-fn-uid-equiv-congruence-on-uid

(defthm stmt-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (stmt-rename-fn c$::stmt uid new-fn)
                  (stmt-rename-fn c$::stmt uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: stmt-rename-fn-ident-equiv-congruence-on-new-fn

(defthm stmt-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (stmt-rename-fn c$::stmt uid new-fn)
                  (stmt-rename-fn c$::stmt uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: comp-stmt-rename-fn-comp-stmt-equiv-congruence-on-comp-stmt

(defthm comp-stmt-rename-fn-comp-stmt-equiv-congruence-on-comp-stmt
  (implies (c$::comp-stmt-equiv comp-stmt comp-stmt-equiv)
           (equal (comp-stmt-rename-fn comp-stmt uid new-fn)
                  (comp-stmt-rename-fn comp-stmt-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: comp-stmt-rename-fn-uid-equiv-congruence-on-uid

(defthm comp-stmt-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (comp-stmt-rename-fn comp-stmt uid new-fn)
                  (comp-stmt-rename-fn comp-stmt uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: comp-stmt-rename-fn-ident-equiv-congruence-on-new-fn

(defthm comp-stmt-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (comp-stmt-rename-fn comp-stmt uid new-fn)
                  (comp-stmt-rename-fn comp-stmt uid new-fn-equiv)))
  :rule-classes :congruence)

Theorem: block-item-rename-fn-block-item-equiv-congruence-on-block-item

(defthm
     block-item-rename-fn-block-item-equiv-congruence-on-block-item
  (implies
       (c$::block-item-equiv c$::block-item block-item-equiv)
       (equal (block-item-rename-fn c$::block-item uid new-fn)
              (block-item-rename-fn block-item-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: block-item-rename-fn-uid-equiv-congruence-on-uid

(defthm block-item-rename-fn-uid-equiv-congruence-on-uid
 (implies
     (c$::uid-equiv uid uid-equiv)
     (equal (block-item-rename-fn c$::block-item uid new-fn)
            (block-item-rename-fn c$::block-item uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: block-item-rename-fn-ident-equiv-congruence-on-new-fn

(defthm block-item-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
     (c$::ident-equiv new-fn new-fn-equiv)
     (equal (block-item-rename-fn c$::block-item uid new-fn)
            (block-item-rename-fn c$::block-item uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: block-item-list-rename-fn-block-item-list-equiv-congruence-on-block-item-list

(defthm
 block-item-list-rename-fn-block-item-list-equiv-congruence-on-block-item-list
 (implies
  (c$::block-item-list-equiv c$::block-item-list
                             block-item-list-equiv)
  (equal
      (block-item-list-rename-fn c$::block-item-list uid new-fn)
      (block-item-list-rename-fn block-item-list-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: block-item-list-rename-fn-uid-equiv-congruence-on-uid

(defthm block-item-list-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (block-item-list-rename-fn c$::block-item-list uid new-fn)
          (block-item-list-rename-fn
               c$::block-item-list uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: block-item-list-rename-fn-ident-equiv-congruence-on-new-fn

(defthm block-item-list-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (block-item-list-rename-fn c$::block-item-list uid new-fn)
          (block-item-list-rename-fn
               c$::block-item-list uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: amb-expr/tyname-rename-fn-amb-expr/tyname-equiv-congruence-on-amb-expr/tyname

(defthm
 amb-expr/tyname-rename-fn-amb-expr/tyname-equiv-congruence-on-amb-expr/tyname
 (implies
  (c$::amb-expr/tyname-equiv c$::amb-expr/tyname
                             amb-expr/tyname-equiv)
  (equal
      (amb-expr/tyname-rename-fn c$::amb-expr/tyname uid new-fn)
      (amb-expr/tyname-rename-fn amb-expr/tyname-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: amb-expr/tyname-rename-fn-uid-equiv-congruence-on-uid

(defthm amb-expr/tyname-rename-fn-uid-equiv-congruence-on-uid
 (implies
   (c$::uid-equiv uid uid-equiv)
   (equal (amb-expr/tyname-rename-fn c$::amb-expr/tyname uid new-fn)
          (amb-expr/tyname-rename-fn
               c$::amb-expr/tyname uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: amb-expr/tyname-rename-fn-ident-equiv-congruence-on-new-fn

(defthm amb-expr/tyname-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
   (c$::ident-equiv new-fn new-fn-equiv)
   (equal (amb-expr/tyname-rename-fn c$::amb-expr/tyname uid new-fn)
          (amb-expr/tyname-rename-fn
               c$::amb-expr/tyname uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: amb-declor/absdeclor-rename-fn-amb-declor/absdeclor-equiv-congruence-on-amb-declor/absdeclor

(defthm
 amb-declor/absdeclor-rename-fn-amb-declor/absdeclor-equiv-congruence-on-amb-declor/absdeclor
 (implies
      (c$::amb-declor/absdeclor-equiv c$::amb-declor/absdeclor
                                      amb-declor/absdeclor-equiv)
      (equal (amb-declor/absdeclor-rename-fn
                  c$::amb-declor/absdeclor uid new-fn)
             (amb-declor/absdeclor-rename-fn
                  amb-declor/absdeclor-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: amb-declor/absdeclor-rename-fn-uid-equiv-congruence-on-uid

(defthm amb-declor/absdeclor-rename-fn-uid-equiv-congruence-on-uid
 (implies
     (c$::uid-equiv uid uid-equiv)
     (equal (amb-declor/absdeclor-rename-fn
                 c$::amb-declor/absdeclor uid new-fn)
            (amb-declor/absdeclor-rename-fn c$::amb-declor/absdeclor
                                            uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: amb-declor/absdeclor-rename-fn-ident-equiv-congruence-on-new-fn

(defthm
    amb-declor/absdeclor-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
     (c$::ident-equiv new-fn new-fn-equiv)
     (equal (amb-declor/absdeclor-rename-fn
                 c$::amb-declor/absdeclor uid new-fn)
            (amb-declor/absdeclor-rename-fn c$::amb-declor/absdeclor
                                            uid new-fn-equiv)))
 :rule-classes :congruence)

Theorem: amb-decl/stmt-rename-fn-amb-decl/stmt-equiv-congruence-on-amb-decl/stmt

(defthm
 amb-decl/stmt-rename-fn-amb-decl/stmt-equiv-congruence-on-amb-decl/stmt
 (implies
   (c$::amb-decl/stmt-equiv c$::amb-decl/stmt amb-decl/stmt-equiv)
   (equal (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid new-fn)
          (amb-decl/stmt-rename-fn amb-decl/stmt-equiv uid new-fn)))
 :rule-classes :congruence)

Theorem: amb-decl/stmt-rename-fn-uid-equiv-congruence-on-uid

(defthm amb-decl/stmt-rename-fn-uid-equiv-congruence-on-uid
 (implies
  (c$::uid-equiv uid uid-equiv)
  (equal
      (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid new-fn)
      (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid-equiv new-fn)))
 :rule-classes :congruence)

Theorem: amb-decl/stmt-rename-fn-ident-equiv-congruence-on-new-fn

(defthm amb-decl/stmt-rename-fn-ident-equiv-congruence-on-new-fn
 (implies
  (c$::ident-equiv new-fn new-fn-equiv)
  (equal
      (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid new-fn)
      (amb-decl/stmt-rename-fn c$::amb-decl/stmt uid new-fn-equiv)))
 :rule-classes :congruence)