		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Exprs/decls/stmts-rename

Definitions and Theorems

Function: expr-rename

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

Function: expr-list-rename

(defun expr-list-rename (c$::expr-list subst)
  (declare (xargs :guard (and (expr-listp c$::expr-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'expr-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::expr-list)
        nil
      (cons (expr-rename (car c$::expr-list) subst)
            (expr-list-rename (cdr c$::expr-list)
                              subst)))))

Function: expr-option-rename

(defun expr-option-rename (c$::expr-option subst)
 (declare (xargs :guard (and (expr-optionp c$::expr-option)
                             (ident-ident-alistp subst))))
 (let ((__function__ 'expr-option-rename))
  (declare (ignorable __function__))
  (expr-option-case
       c$::expr-option
       :some
       (expr-fix
            (expr-rename (c$::expr-option-some->val c$::expr-option)
                         subst))
       :none nil)))

Function: const-expr-rename

(defun const-expr-rename (const-expr subst)
  (declare (xargs :guard (and (const-exprp const-expr)
                              (ident-ident-alistp subst))))
  (declare (ignorable const-expr subst))
  (let ((__function__ 'const-expr-rename))
    (declare (ignorable __function__))
    (const-expr (expr-rename (const-expr->expr const-expr)
                             subst))))

Function: const-expr-option-rename

(defun const-expr-option-rename (c$::const-expr-option subst)
 (declare
      (xargs :guard (and (const-expr-optionp c$::const-expr-option)
                         (ident-ident-alistp subst))))
 (let ((__function__ 'const-expr-option-rename))
  (declare (ignorable __function__))
  (const-expr-option-case
   c$::const-expr-option
   :some
   (c$::const-expr-fix
        (const-expr-rename
             (c$::const-expr-option-some->val c$::const-expr-option)
             subst))
   :none nil)))

Function: genassoc-rename

(defun genassoc-rename (c$::genassoc subst)
 (declare (xargs :guard (and (genassocp c$::genassoc)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::genassoc subst))
 (let ((__function__ 'genassoc-rename))
  (declare (ignorable __function__))
  (genassoc-case
    c$::genassoc
    :type (c$::genassoc-type
               (tyname-rename (c$::genassoc-type->type c$::genassoc)
                              subst)
               (expr-rename (c$::genassoc-type->expr c$::genassoc)
                            subst))
    :default
    (genassoc-default
         (expr-rename (c$::genassoc-default->expr c$::genassoc)
                      subst)))))

Function: genassoc-list-rename

(defun genassoc-list-rename (c$::genassoc-list subst)
  (declare (xargs :guard (and (genassoc-listp c$::genassoc-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'genassoc-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::genassoc-list)
        nil
      (cons (genassoc-rename (car c$::genassoc-list)
                             subst)
            (genassoc-list-rename (cdr c$::genassoc-list)
                                  subst)))))

Function: member-designor-rename

(defun member-designor-rename (c$::member-designor subst)
 (declare (xargs :guard (and (member-designorp c$::member-designor)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::member-designor subst))
 (let ((__function__ 'member-designor-rename))
  (declare (ignorable __function__))
  (member-designor-case
    c$::member-designor
    :ident
    (c$::member-designor-ident
         (ident-rename
              (c$::member-designor-ident->ident c$::member-designor)
              subst))
    :dot
    (c$::member-designor-dot
         (member-designor-rename
              (c$::member-designor-dot->member c$::member-designor)
              subst)
         (ident-rename
              (c$::member-designor-dot->name c$::member-designor)
              subst))
    :sub
    (c$::member-designor-sub
         (member-designor-rename
              (c$::member-designor-sub->member c$::member-designor)
              subst)
         (expr-rename
              (c$::member-designor-sub->index c$::member-designor)
              subst)))))

Function: type-spec-rename

(defun type-spec-rename (c$::type-spec subst)
 (declare (xargs :guard (and (type-specp c$::type-spec)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::type-spec subst))
 (let ((__function__ 'type-spec-rename))
  (declare (ignorable __function__))
  (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 (c$::type-spec-atomic->type c$::type-spec)
                       subst))
   :struct
   (type-spec-struct
      (struni-spec-rename (c$::type-spec-struct->spec c$::type-spec)
                          subst))
   :union
   (type-spec-union
       (struni-spec-rename (c$::type-spec-union->spec c$::type-spec)
                           subst))
   :enum
   (type-spec-enum
        (enum-spec-rename (c$::type-spec-enum->spec c$::type-spec)
                          subst))
   :typedef
   (c$::type-spec-typedef
        (ident-rename (c$::type-spec-typedef->name c$::type-spec)
                      subst))
   :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
             (c$::type-spec-struct-empty->attribs c$::type-spec)
             subst)
        (ident-option-rename
             (c$::type-spec-struct-empty->name? c$::type-spec)
             subst))
   :typeof-expr
   (c$::type-spec-typeof-expr
        (expr-rename (c$::type-spec-typeof-expr->expr c$::type-spec)
                     subst)
        (c$::type-spec-typeof-expr->uscores c$::type-spec))
   :typeof-type
   (c$::type-spec-typeof-type
      (tyname-rename (c$::type-spec-typeof-type->type c$::type-spec)
                     subst)
      (c$::type-spec-typeof-type->uscores c$::type-spec))
   :typeof-ambig
   (c$::type-spec-typeof-ambig
        (amb-expr/tyname-rename
             (c$::type-spec-typeof-ambig->expr/type c$::type-spec)
             subst)
        (c$::type-spec-typeof-ambig->uscores c$::type-spec))
   :auto-type (type-spec-fix c$::type-spec))))

Function: spec/qual-rename

(defun spec/qual-rename (c$::spec/qual subst)
 (declare (xargs :guard (and (spec/qual-p c$::spec/qual)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::spec/qual subst))
 (let ((__function__ 'spec/qual-rename))
  (declare (ignorable __function__))
  (spec/qual-case
   c$::spec/qual
   :typespec
   (spec/qual-typespec
      (type-spec-rename (c$::spec/qual-typespec->spec c$::spec/qual)
                        subst))
   :typequal (spec/qual-fix c$::spec/qual)
   :align
   (spec/qual-align
        (align-spec-rename (c$::spec/qual-align->spec c$::spec/qual)
                           subst))
   :attrib
   (spec/qual-attrib
      (attrib-spec-rename (c$::spec/qual-attrib->spec c$::spec/qual)
                          subst)))))

Function: spec/qual-list-rename

(defun spec/qual-list-rename (c$::spec/qual-list subst)
  (declare (xargs :guard (and (spec/qual-listp c$::spec/qual-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'spec/qual-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::spec/qual-list)
        nil
      (cons (spec/qual-rename (car c$::spec/qual-list)
                              subst)
            (spec/qual-list-rename (cdr c$::spec/qual-list)
                                   subst)))))

Function: align-spec-rename

(defun align-spec-rename (c$::align-spec subst)
 (declare (xargs :guard (and (align-specp c$::align-spec)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::align-spec subst))
 (let ((__function__ 'align-spec-rename))
  (declare (ignorable __function__))
  (align-spec-case
   c$::align-spec
   :alignas-type
   (align-spec-alignas-type
        (tyname-rename
             (c$::align-spec-alignas-type->type c$::align-spec)
             subst))
   :alignas-expr
   (align-spec-alignas-expr
        (const-expr-rename
             (c$::align-spec-alignas-expr->expr c$::align-spec)
             subst))
   :alignas-ambig
   (c$::align-spec-alignas-ambig
       (amb-expr/tyname-rename
            (c$::align-spec-alignas-ambig->expr/type c$::align-spec)
            subst)))))

Function: decl-spec-rename

(defun decl-spec-rename (c$::decl-spec subst)
 (declare (xargs :guard (and (decl-specp c$::decl-spec)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::decl-spec subst))
 (let ((__function__ 'decl-spec-rename))
  (declare (ignorable __function__))
  (decl-spec-case
   c$::decl-spec
   :stoclass (decl-spec-fix c$::decl-spec)
   :typespec
   (decl-spec-typespec
      (type-spec-rename (c$::decl-spec-typespec->spec c$::decl-spec)
                        subst))
   :typequal (decl-spec-fix c$::decl-spec)
   :function (decl-spec-fix c$::decl-spec)
   :align
   (decl-spec-align
        (align-spec-rename (c$::decl-spec-align->spec c$::decl-spec)
                           subst))
   :attrib
   (decl-spec-attrib
      (attrib-spec-rename (c$::decl-spec-attrib->spec c$::decl-spec)
                          subst))
   :stdcall (decl-spec-fix c$::decl-spec)
   :declspec
   (c$::decl-spec-declspec
        (ident-rename (c$::decl-spec-declspec->arg c$::decl-spec)
                      subst)))))

Function: decl-spec-list-rename

(defun decl-spec-list-rename (c$::decl-spec-list subst)
  (declare (xargs :guard (and (decl-spec-listp c$::decl-spec-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'decl-spec-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::decl-spec-list)
        nil
      (cons (decl-spec-rename (car c$::decl-spec-list)
                              subst)
            (decl-spec-list-rename (cdr c$::decl-spec-list)
                                   subst)))))

Function: typequal/attribspec-rename

(defun typequal/attribspec-rename (c$::typequal/attribspec subst)
 (declare
  (xargs
     :guard (and (c$::typequal/attribspec-p c$::typequal/attribspec)
                 (ident-ident-alistp subst))))
 (declare (ignorable c$::typequal/attribspec subst))
 (let ((__function__ 'typequal/attribspec-rename))
  (declare (ignorable __function__))
  (c$::typequal/attribspec-case
   c$::typequal/attribspec
   :type (c$::typequal/attribspec-fix c$::typequal/attribspec)
   :attrib
   (c$::typequal/attribspec-attrib
    (attrib-spec-rename
      (c$::typequal/attribspec-attrib->spec c$::typequal/attribspec)
      subst)))))

Function: typequal/attribspec-list-rename

(defun typequal/attribspec-list-rename
       (c$::typequal/attribspec-list subst)
 (declare
  (xargs
   :guard
   (and (c$::typequal/attribspec-listp c$::typequal/attribspec-list)
        (ident-ident-alistp subst))))
 (let ((__function__ 'typequal/attribspec-list-rename))
  (declare (ignorable __function__))
  (if (endp c$::typequal/attribspec-list)
      nil
   (cons
      (typequal/attribspec-rename (car c$::typequal/attribspec-list)
                                  subst)
      (typequal/attribspec-list-rename
           (cdr c$::typequal/attribspec-list)
           subst)))))

Function: typequal/attribspec-list-list-rename

(defun typequal/attribspec-list-list-rename
       (c$::typequal/attribspec-list-list subst)
 (declare (xargs :guard (and (typequal/attribspec-list-listp
                                  c$::typequal/attribspec-list-list)
                             (ident-ident-alistp subst))))
 (let ((__function__ 'typequal/attribspec-list-list-rename))
   (declare (ignorable __function__))
   (if (endp c$::typequal/attribspec-list-list)
       nil
     (cons (typequal/attribspec-list-rename
                (car c$::typequal/attribspec-list-list)
                subst)
           (typequal/attribspec-list-list-rename
                (cdr c$::typequal/attribspec-list-list)
                subst)))))

Function: initer-rename

(defun initer-rename (c$::initer subst)
 (declare (xargs :guard (and (initerp c$::initer)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::initer subst))
 (let ((__function__ 'initer-rename))
  (declare (ignorable __function__))
  (initer-case
    c$::initer
    :single
    (initer-single (expr-rename (c$::initer-single->expr c$::initer)
                                subst))
    :list
    (c$::initer-list
         (desiniter-list-rename (c$::initer-list->elems c$::initer)
                                subst)
         (c$::initer-list->final-comma c$::initer)))))

Function: initer-option-rename

(defun initer-option-rename (c$::initer-option subst)
 (declare (xargs :guard (and (initer-optionp c$::initer-option)
                             (ident-ident-alistp subst))))
 (let ((__function__ 'initer-option-rename))
  (declare (ignorable __function__))
  (initer-option-case
   c$::initer-option
   :some
   (initer-fix
      (initer-rename (c$::initer-option-some->val c$::initer-option)
                     subst))
   :none nil)))

Function: desiniter-rename

(defun desiniter-rename (desiniter subst)
  (declare (xargs :guard (and (desiniterp desiniter)
                              (ident-ident-alistp subst))))
  (declare (ignorable desiniter subst))
  (let ((__function__ 'desiniter-rename))
    (declare (ignorable __function__))
    (desiniter
         (designor-list-rename (c$::desiniter->designors desiniter)
                               subst)
         (initer-rename (c$::desiniter->initer desiniter)
                        subst))))

Function: desiniter-list-rename

(defun desiniter-list-rename (c$::desiniter-list subst)
  (declare (xargs :guard (and (desiniter-listp c$::desiniter-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'desiniter-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::desiniter-list)
        nil
      (cons (desiniter-rename (car c$::desiniter-list)
                              subst)
            (desiniter-list-rename (cdr c$::desiniter-list)
                                   subst)))))

Function: designor-rename

(defun designor-rename (c$::designor subst)
 (declare (xargs :guard (and (designorp c$::designor)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::designor subst))
 (let ((__function__ 'designor-rename))
  (declare (ignorable __function__))
  (designor-case
      c$::designor
      :sub
      (c$::designor-sub
           (const-expr-rename (c$::designor-sub->index c$::designor)
                              subst)
           (const-expr-option-rename
                (c$::designor-sub->range? c$::designor)
                subst))
      :dot (c$::designor-dot
                (ident-rename (c$::designor-dot->name c$::designor)
                              subst)))))

Function: designor-list-rename

(defun designor-list-rename (c$::designor-list subst)
  (declare (xargs :guard (and (designor-listp c$::designor-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'designor-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::designor-list)
        nil
      (cons (designor-rename (car c$::designor-list)
                             subst)
            (designor-list-rename (cdr c$::designor-list)
                                  subst)))))

Function: declor-rename

(defun declor-rename (declor subst)
  (declare (xargs :guard (and (declorp declor)
                              (ident-ident-alistp subst))))
  (declare (ignorable declor subst))
  (let ((__function__ 'declor-rename))
    (declare (ignorable __function__))
    (declor (typequal/attribspec-list-list-rename
                 (c$::declor->pointers declor)
                 subst)
            (dirdeclor-rename (declor->direct declor)
                              subst))))

Function: declor-option-rename

(defun declor-option-rename (c$::declor-option subst)
 (declare (xargs :guard (and (declor-optionp c$::declor-option)
                             (ident-ident-alistp subst))))
 (let ((__function__ 'declor-option-rename))
  (declare (ignorable __function__))
  (declor-option-case
   c$::declor-option
   :some
   (declor-fix
      (declor-rename (c$::declor-option-some->val c$::declor-option)
                     subst))
   :none nil)))

Function: dirdeclor-rename

(defun dirdeclor-rename (dirdeclor subst)
 (declare (xargs :guard (and (dirdeclorp dirdeclor)
                             (ident-ident-alistp subst))))
 (declare (ignorable dirdeclor subst))
 (let ((__function__ 'dirdeclor-rename))
  (declare (ignorable __function__))
  (dirdeclor-case
   dirdeclor
   :ident
   (dirdeclor-ident (ident-rename (dirdeclor-ident->ident dirdeclor)
                                  subst))
   :paren (dirdeclor-paren
               (declor-rename (c$::dirdeclor-paren->inner dirdeclor)
                              subst))
   :array
   (c$::dirdeclor-array
        (dirdeclor-rename (c$::dirdeclor-array->declor dirdeclor)
                          subst)
        (typequal/attribspec-list-rename
             (c$::dirdeclor-array->qualspecs dirdeclor)
             subst)
        (expr-option-rename (c$::dirdeclor-array->size? dirdeclor)
                            subst))
   :array-static1
   (c$::dirdeclor-array-static1
        (dirdeclor-rename
             (c$::dirdeclor-array-static1->declor dirdeclor)
             subst)
        (typequal/attribspec-list-rename
             (c$::dirdeclor-array-static1->qualspecs dirdeclor)
             subst)
        (expr-rename (c$::dirdeclor-array-static1->size dirdeclor)
                     subst))
   :array-static2
   (c$::dirdeclor-array-static2
        (dirdeclor-rename
             (c$::dirdeclor-array-static2->declor dirdeclor)
             subst)
        (typequal/attribspec-list-rename
             (c$::dirdeclor-array-static2->qualspecs dirdeclor)
             subst)
        (expr-rename (c$::dirdeclor-array-static2->size dirdeclor)
                     subst))
   :array-star
   (c$::dirdeclor-array-star
      (dirdeclor-rename (c$::dirdeclor-array-star->declor dirdeclor)
                        subst)
      (typequal/attribspec-list-rename
           (c$::dirdeclor-array-star->qualspecs dirdeclor)
           subst))
   :function-params
   (c$::dirdeclor-function-params
     (dirdeclor-rename (dirdeclor-function-params->declor dirdeclor)
                       subst)
     (param-declon-list-rename
          (dirdeclor-function-params->params dirdeclor)
          subst)
     (c$::dirdeclor-function-params->ellipsis dirdeclor))
   :function-names
   (c$::dirdeclor-function-names
      (dirdeclor-rename
           (c$::dirdeclor-function-names->declor dirdeclor)
           subst)
      (ident-list-rename (dirdeclor-function-names->names dirdeclor)
                         subst)))))

Function: absdeclor-rename

(defun absdeclor-rename (absdeclor subst)
 (declare (xargs :guard (and (absdeclorp absdeclor)
                             (ident-ident-alistp subst))))
 (declare (ignorable absdeclor subst))
 (let ((__function__ 'absdeclor-rename))
  (declare (ignorable __function__))
  (absdeclor
      (typequal/attribspec-list-list-rename
           (c$::absdeclor->pointers absdeclor)
           subst)
      (dirabsdeclor-option-rename (c$::absdeclor->direct? absdeclor)
                                  subst))))

Function: absdeclor-option-rename

(defun absdeclor-option-rename (c$::absdeclor-option subst)
 (declare
      (xargs :guard (and (absdeclor-optionp c$::absdeclor-option)
                         (ident-ident-alistp subst))))
 (let ((__function__ 'absdeclor-option-rename))
  (declare (ignorable __function__))
  (absdeclor-option-case
     c$::absdeclor-option
     :some
     (absdeclor-fix
          (absdeclor-rename
               (c$::absdeclor-option-some->val c$::absdeclor-option)
               subst))
     :none nil)))

Function: dirabsdeclor-rename

(defun dirabsdeclor-rename (c$::dirabsdeclor subst)
 (declare (xargs :guard (and (dirabsdeclorp c$::dirabsdeclor)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::dirabsdeclor subst))
 (let ((__function__ 'dirabsdeclor-rename))
  (declare (ignorable __function__))
  (dirabsdeclor-case
   c$::dirabsdeclor
   :dummy-base (dirabsdeclor-fix c$::dirabsdeclor)
   :paren (dirabsdeclor-paren
               (absdeclor-rename
                    (c$::dirabsdeclor-paren->inner c$::dirabsdeclor)
                    subst))
   :array
   (c$::dirabsdeclor-array
        (dirabsdeclor-option-rename
             (c$::dirabsdeclor-array->declor? c$::dirabsdeclor)
             subst)
        (typequal/attribspec-list-rename
             (c$::dirabsdeclor-array->qualspecs c$::dirabsdeclor)
             subst)
        (expr-option-rename
             (c$::dirabsdeclor-array->size? c$::dirabsdeclor)
             subst))
   :array-static1
   (c$::dirabsdeclor-array-static1
    (dirabsdeclor-option-rename
         (c$::dirabsdeclor-array-static1->declor? c$::dirabsdeclor)
         subst)
    (typequal/attribspec-list-rename
        (c$::dirabsdeclor-array-static1->qualspecs c$::dirabsdeclor)
        subst)
    (expr-rename
         (c$::dirabsdeclor-array-static1->size c$::dirabsdeclor)
         subst))
   :array-static2
   (c$::dirabsdeclor-array-static2
    (dirabsdeclor-option-rename
         (c$::dirabsdeclor-array-static2->declor? c$::dirabsdeclor)
         subst)
    (typequal/attribspec-list-rename
        (c$::dirabsdeclor-array-static2->qualspecs c$::dirabsdeclor)
        subst)
    (expr-rename
         (c$::dirabsdeclor-array-static2->size c$::dirabsdeclor)
         subst))
   :array-star
   (dirabsdeclor-array-star
        (dirabsdeclor-option-rename
             (c$::dirabsdeclor-array-star->declor? c$::dirabsdeclor)
             subst))
   :function
   (c$::dirabsdeclor-function
        (dirabsdeclor-option-rename
             (c$::dirabsdeclor-function->declor? c$::dirabsdeclor)
             subst)
        (param-declon-list-rename
             (c$::dirabsdeclor-function->params c$::dirabsdeclor)
             subst)
        (c$::dirabsdeclor-function->ellipsis c$::dirabsdeclor)))))

Function: dirabsdeclor-option-rename

(defun dirabsdeclor-option-rename (c$::dirabsdeclor-option subst)
 (declare
   (xargs :guard (and (dirabsdeclor-optionp c$::dirabsdeclor-option)
                      (ident-ident-alistp subst))))
 (let ((__function__ 'dirabsdeclor-option-rename))
  (declare (ignorable __function__))
  (dirabsdeclor-option-case
   c$::dirabsdeclor-option
   :some
   (dirabsdeclor-fix
    (dirabsdeclor-rename
         (c$::dirabsdeclor-option-some->val c$::dirabsdeclor-option)
         subst))
   :none nil)))

Function: param-declon-rename

(defun param-declon-rename (param-declon subst)
 (declare (xargs :guard (and (param-declonp param-declon)
                             (ident-ident-alistp subst))))
 (declare (ignorable param-declon subst))
 (let ((__function__ 'param-declon-rename))
  (declare (ignorable __function__))
  (param-declon
   (decl-spec-list-rename (c$::param-declon->specs param-declon)
                          subst)
   (param-declor-rename (c$::param-declon->declor param-declon)
                        subst)
   (attrib-spec-list-rename (c$::param-declon->attribs param-declon)
                            subst))))

Function: param-declon-list-rename

(defun param-declon-list-rename (c$::param-declon-list subst)
  (declare
       (xargs :guard (and (param-declon-listp c$::param-declon-list)
                          (ident-ident-alistp subst))))
  (let ((__function__ 'param-declon-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::param-declon-list)
        nil
      (cons (param-declon-rename (car c$::param-declon-list)
                                 subst)
            (param-declon-list-rename (cdr c$::param-declon-list)
                                      subst)))))

Function: param-declor-rename

(defun param-declor-rename (c$::param-declor subst)
 (declare (xargs :guard (and (param-declorp c$::param-declor)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::param-declor subst))
 (let ((__function__ 'param-declor-rename))
  (declare (ignorable __function__))
  (param-declor-case
      c$::param-declor
      :nonabstract
      (c$::param-declor-nonabstract
           (declor-rename
                (param-declor-nonabstract->declor c$::param-declor)
                subst)
           (c$::param-declor-nonabstract->info c$::param-declor))
      :abstract
      (param-declor-abstract
           (absdeclor-rename
                (c$::param-declor-abstract->declor c$::param-declor)
                subst))
      :none (param-declor-fix c$::param-declor)
      :ambig
      (c$::param-declor-ambig
           (amb-declor/absdeclor-rename
                (c$::param-declor-ambig->declor c$::param-declor)
                subst)))))

Function: tyname-rename

(defun tyname-rename (tyname subst)
  (declare (xargs :guard (and (tynamep tyname)
                              (ident-ident-alistp subst))))
  (declare (ignorable tyname subst))
  (let ((__function__ 'tyname-rename))
    (declare (ignorable __function__))
    (tyname (spec/qual-list-rename (c$::tyname->specquals tyname)
                                   subst)
            (absdeclor-option-rename (c$::tyname->declor? tyname)
                                     subst)
            (tyname->info tyname))))

Function: struni-spec-rename

(defun struni-spec-rename (struni-spec subst)
 (declare (xargs :guard (and (struni-specp struni-spec)
                             (ident-ident-alistp subst))))
 (declare (ignorable struni-spec subst))
 (let ((__function__ 'struni-spec-rename))
  (declare (ignorable __function__))
  (struni-spec
   (attrib-spec-list-rename (c$::struni-spec->attribs struni-spec)
                            subst)
   (ident-option-rename (c$::struni-spec->name? struni-spec)
                        subst)
   (struct-declon-list-rename (c$::struni-spec->members struni-spec)
                              subst))))

Function: struct-declon-rename

(defun struct-declon-rename (c$::struct-declon subst)
 (declare (xargs :guard (and (struct-declonp c$::struct-declon)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::struct-declon subst))
 (let ((__function__ 'struct-declon-rename))
  (declare (ignorable __function__))
  (struct-declon-case
   c$::struct-declon
   :member
   (c$::struct-declon-member
        (c$::struct-declon-member->extension c$::struct-declon)
        (spec/qual-list-rename
             (c$::struct-declon-member->specquals c$::struct-declon)
             subst)
        (struct-declor-list-rename
             (c$::struct-declon-member->declors c$::struct-declon)
             subst)
        (attrib-spec-list-rename
             (c$::struct-declon-member->attribs c$::struct-declon)
             subst))
   :statassert
   (struct-declon-statassert
    (statassert-rename
        (c$::struct-declon-statassert->statassert c$::struct-declon)
        subst))
   :empty (struct-declon-fix c$::struct-declon))))

Function: struct-declon-list-rename

(defun struct-declon-list-rename (c$::struct-declon-list subst)
 (declare
     (xargs :guard (and (struct-declon-listp c$::struct-declon-list)
                        (ident-ident-alistp subst))))
 (let ((__function__ 'struct-declon-list-rename))
   (declare (ignorable __function__))
   (if (endp c$::struct-declon-list)
       nil
     (cons (struct-declon-rename (car c$::struct-declon-list)
                                 subst)
           (struct-declon-list-rename (cdr c$::struct-declon-list)
                                      subst)))))

Function: struct-declor-rename

(defun struct-declor-rename (struct-declor subst)
 (declare (xargs :guard (and (struct-declorp struct-declor)
                             (ident-ident-alistp subst))))
 (declare (ignorable struct-declor subst))
 (let ((__function__ 'struct-declor-rename))
  (declare (ignorable __function__))
  (struct-declor
    (declor-option-rename (c$::struct-declor->declor? struct-declor)
                          subst)
    (const-expr-option-rename
         (c$::struct-declor->expr? struct-declor)
         subst))))

Function: struct-declor-list-rename

(defun struct-declor-list-rename (c$::struct-declor-list subst)
 (declare
     (xargs :guard (and (struct-declor-listp c$::struct-declor-list)
                        (ident-ident-alistp subst))))
 (let ((__function__ 'struct-declor-list-rename))
   (declare (ignorable __function__))
   (if (endp c$::struct-declor-list)
       nil
     (cons (struct-declor-rename (car c$::struct-declor-list)
                                 subst)
           (struct-declor-list-rename (cdr c$::struct-declor-list)
                                      subst)))))

Function: enum-spec-rename

(defun enum-spec-rename (enum-spec subst)
 (declare (xargs :guard (and (enum-specp enum-spec)
                             (ident-ident-alistp subst))))
 (declare (ignorable enum-spec subst))
 (let ((__function__ 'enum-spec-rename))
   (declare (ignorable __function__))
   (enum-spec (ident-option-rename (c$::enum-spec->name? enum-spec)
                                   subst)
              (enumer-list-rename (c$::enum-spec->enumers enum-spec)
                                  subst)
              (c$::enum-spec->final-comma enum-spec))))

Function: enumer-rename

(defun enumer-rename (enumer subst)
  (declare (xargs :guard (and (enumerp enumer)
                              (ident-ident-alistp subst))))
  (declare (ignorable enumer subst))
  (let ((__function__ 'enumer-rename))
    (declare (ignorable __function__))
    (enumer (ident-rename (c$::enumer->name enumer)
                          subst)
            (const-expr-option-rename (c$::enumer->value? enumer)
                                      subst))))

Function: enumer-list-rename

(defun enumer-list-rename (c$::enumer-list subst)
  (declare (xargs :guard (and (enumer-listp c$::enumer-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'enumer-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::enumer-list)
        nil
      (cons (enumer-rename (car c$::enumer-list)
                           subst)
            (enumer-list-rename (cdr c$::enumer-list)
                                subst)))))

Function: statassert-rename

(defun statassert-rename (statassert subst)
  (declare (xargs :guard (and (statassertp statassert)
                              (ident-ident-alistp subst))))
  (declare (ignorable statassert subst))
  (let ((__function__ 'statassert-rename))
    (declare (ignorable __function__))
    (statassert (const-expr-rename (c$::statassert->test statassert)
                                   subst)
                (c$::statassert->message statassert))))

Function: attrib-rename

(defun attrib-rename (c$::attrib subst)
 (declare (xargs :guard (and (c$::attribp c$::attrib)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::attrib subst))
 (let ((__function__ 'attrib-rename))
  (declare (ignorable __function__))
  (c$::attrib-case
   c$::attrib
   :name (c$::attrib-name
              (attrib-name-rename (c$::attrib-name->name c$::attrib)
                                  subst))
   :name-params
   (c$::attrib-name-params
       (attrib-name-rename (c$::attrib-name-params->name c$::attrib)
                           subst)
       (expr-list-rename (c$::attrib-name-params->params c$::attrib)
                         subst)))))

Function: attrib-list-rename

(defun attrib-list-rename (c$::attrib-list subst)
  (declare (xargs :guard (and (c$::attrib-listp c$::attrib-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'attrib-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::attrib-list)
        nil
      (cons (attrib-rename (car c$::attrib-list)
                           subst)
            (attrib-list-rename (cdr c$::attrib-list)
                                subst)))))

Function: attrib-spec-rename

(defun attrib-spec-rename (c$::attrib-spec subst)
 (declare (xargs :guard (and (c$::attrib-specp c$::attrib-spec)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::attrib-spec subst))
 (let ((__function__ 'attrib-spec-rename))
  (declare (ignorable __function__))
  (c$::attrib-spec
      (c$::attrib-spec->uscores c$::attrib-spec)
      (attrib-list-rename (c$::attrib-spec->attribs c$::attrib-spec)
                          subst))))

Function: attrib-spec-list-rename

(defun attrib-spec-list-rename (c$::attrib-spec-list subst)
  (declare
       (xargs :guard (and (attrib-spec-listp c$::attrib-spec-list)
                          (ident-ident-alistp subst))))
  (let ((__function__ 'attrib-spec-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::attrib-spec-list)
        nil
      (cons (attrib-spec-rename (car c$::attrib-spec-list)
                                subst)
            (attrib-spec-list-rename (cdr c$::attrib-spec-list)
                                     subst)))))

Function: init-declor-rename

(defun init-declor-rename (init-declor subst)
 (declare (xargs :guard (and (init-declorp init-declor)
                             (ident-ident-alistp subst))))
 (declare (ignorable init-declor subst))
 (let ((__function__ 'init-declor-rename))
  (declare (ignorable __function__))
  (init-declor
     (declor-rename (init-declor->declor init-declor)
                    subst)
     (c$::init-declor->asm? init-declor)
     (attrib-spec-list-rename (c$::init-declor->attribs init-declor)
                              subst)
     (initer-option-rename (init-declor->initer? init-declor)
                           subst)
     (c$::init-declor->info init-declor))))

Function: init-declor-list-rename

(defun init-declor-list-rename (c$::init-declor-list subst)
  (declare
       (xargs :guard (and (init-declor-listp c$::init-declor-list)
                          (ident-ident-alistp subst))))
  (let ((__function__ 'init-declor-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::init-declor-list)
        nil
      (cons (init-declor-rename (car c$::init-declor-list)
                                subst)
            (init-declor-list-rename (cdr c$::init-declor-list)
                                     subst)))))

Function: declon-rename

(defun declon-rename (declon subst)
 (declare (xargs :guard (and (declonp declon)
                             (ident-ident-alistp subst))))
 (declare (ignorable declon subst))
 (let ((__function__ 'declon-rename))
  (declare (ignorable __function__))
  (declon-case
   declon
   :declon
   (c$::declon-declon
        (declon-declon->extension declon)
        (decl-spec-list-rename (declon-declon->specs declon)
                               subst)
        (init-declor-list-rename (declon-declon->declors declon)
                                 subst))
   :statassert
   (declon-statassert
       (statassert-rename (c$::declon-statassert->statassert declon)
                          subst)))))

Function: declon-list-rename

(defun declon-list-rename (c$::declon-list subst)
  (declare (xargs :guard (and (declon-listp c$::declon-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'declon-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::declon-list)
        nil
      (cons (declon-rename (car c$::declon-list)
                           subst)
            (declon-list-rename (cdr c$::declon-list)
                                subst)))))

Function: label-rename

(defun label-rename (c$::label subst)
 (declare (xargs :guard (and (labelp c$::label)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::label subst))
 (let ((__function__ 'label-rename))
  (declare (ignorable __function__))
  (label-case
   c$::label
   :name
   (c$::label-name
        (ident-rename (c$::label-name->name c$::label)
                      subst)
        (attrib-spec-list-rename (c$::label-name->attribs c$::label)
                                 subst))
   :casexpr
   (c$::label-casexpr
     (const-expr-rename (c$::label-casexpr->expr c$::label)
                        subst)
     (const-expr-option-rename (c$::label-casexpr->range? c$::label)
                               subst))
   :default (label-fix c$::label))))

Function: asm-output-rename

(defun asm-output-rename (c$::asm-output subst)
  (declare (xargs :guard (and (c$::asm-outputp c$::asm-output)
                              (ident-ident-alistp subst))))
  (declare (ignorable c$::asm-output subst))
  (let ((__function__ 'asm-output-rename))
    (declare (ignorable __function__))
    (c$::asm-output
         (ident-option-rename (c$::asm-output->name? c$::asm-output)
                              subst)
         (c$::asm-output->constraint c$::asm-output)
         (expr-rename (c$::asm-output->lvalue c$::asm-output)
                      subst))))

Function: asm-output-list-rename

(defun asm-output-list-rename (c$::asm-output-list subst)
  (declare
       (xargs :guard (and (c$::asm-output-listp c$::asm-output-list)
                          (ident-ident-alistp subst))))
  (let ((__function__ 'asm-output-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::asm-output-list)
        nil
      (cons (asm-output-rename (car c$::asm-output-list)
                               subst)
            (asm-output-list-rename (cdr c$::asm-output-list)
                                    subst)))))

Function: asm-input-rename

(defun asm-input-rename (c$::asm-input subst)
  (declare (xargs :guard (and (c$::asm-inputp c$::asm-input)
                              (ident-ident-alistp subst))))
  (declare (ignorable c$::asm-input subst))
  (let ((__function__ 'asm-input-rename))
    (declare (ignorable __function__))
    (c$::asm-input
         (ident-option-rename (c$::asm-input->name? c$::asm-input)
                              subst)
         (c$::asm-input->constraint c$::asm-input)
         (expr-rename (c$::asm-input->rvalue c$::asm-input)
                      subst))))

Function: asm-input-list-rename

(defun asm-input-list-rename (c$::asm-input-list subst)
  (declare
       (xargs :guard (and (c$::asm-input-listp c$::asm-input-list)
                          (ident-ident-alistp subst))))
  (let ((__function__ 'asm-input-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::asm-input-list)
        nil
      (cons (asm-input-rename (car c$::asm-input-list)
                              subst)
            (asm-input-list-rename (cdr c$::asm-input-list)
                                   subst)))))

Function: asm-stmt-rename

(defun asm-stmt-rename (c$::asm-stmt subst)
 (declare (xargs :guard (and (c$::asm-stmtp c$::asm-stmt)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::asm-stmt subst))
 (let ((__function__ 'asm-stmt-rename))
   (declare (ignorable __function__))
   (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 (c$::asm-stmt->outputs c$::asm-stmt)
                                subst)
        (asm-input-list-rename (c$::asm-stmt->inputs c$::asm-stmt)
                               subst)
        (c$::asm-stmt->clobbers c$::asm-stmt)
        (ident-list-rename (c$::asm-stmt->labels c$::asm-stmt)
                           subst))))

Function: stmt-rename

(defun stmt-rename (c$::stmt subst)
 (declare (xargs :guard (and (stmtp c$::stmt)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::stmt subst))
 (let ((__function__ 'stmt-rename))
  (declare (ignorable __function__))
  (stmt-case
   c$::stmt
   :labeled (c$::stmt-labeled
                 (label-rename (c$::stmt-labeled->label c$::stmt)
                               subst)
                 (stmt-rename (c$::stmt-labeled->stmt c$::stmt)
                              subst))
   :compound
   (stmt-compound (comp-stmt-rename (stmt-compound->stmt c$::stmt)
                                    subst))
   :expr (c$::stmt-expr
              (expr-option-rename (c$::stmt-expr->expr? c$::stmt)
                                  subst)
              (c$::stmt-expr->info c$::stmt))
   :if (c$::stmt-if (expr-rename (c$::stmt-if->test c$::stmt)
                                 subst)
                    (stmt-rename (c$::stmt-if->then c$::stmt)
                                 subst))
   :ifelse
   (c$::stmt-ifelse (expr-rename (c$::stmt-ifelse->test c$::stmt)
                                 subst)
                    (stmt-rename (c$::stmt-ifelse->then c$::stmt)
                                 subst)
                    (stmt-rename (c$::stmt-ifelse->else c$::stmt)
                                 subst))
   :switch
   (c$::stmt-switch (expr-rename (c$::stmt-switch->target c$::stmt)
                                 subst)
                    (stmt-rename (c$::stmt-switch->body c$::stmt)
                                 subst))
   :while
   (c$::stmt-while (expr-rename (c$::stmt-while->test c$::stmt)
                                subst)
                   (stmt-rename (c$::stmt-while->body c$::stmt)
                                subst))
   :dowhile
   (c$::stmt-dowhile (stmt-rename (c$::stmt-dowhile->body c$::stmt)
                                  subst)
                     (expr-rename (c$::stmt-dowhile->test c$::stmt)
                                  subst))
   :for-expr
   (c$::stmt-for-expr
        (expr-option-rename (c$::stmt-for-expr->init c$::stmt)
                            subst)
        (expr-option-rename (c$::stmt-for-expr->test c$::stmt)
                            subst)
        (expr-option-rename (c$::stmt-for-expr->next c$::stmt)
                            subst)
        (stmt-rename (c$::stmt-for-expr->body c$::stmt)
                     subst))
   :for-declon
   (c$::stmt-for-declon
        (declon-rename (c$::stmt-for-declon->init c$::stmt)
                       subst)
        (expr-option-rename (c$::stmt-for-declon->test c$::stmt)
                            subst)
        (expr-option-rename (c$::stmt-for-declon->next c$::stmt)
                            subst)
        (stmt-rename (c$::stmt-for-declon->body c$::stmt)
                     subst))
   :for-ambig
   (c$::stmt-for-ambig
        (amb-declon/stmt-rename (c$::stmt-for-ambig->init c$::stmt)
                                subst)
        (expr-option-rename (c$::stmt-for-ambig->test c$::stmt)
                            subst)
        (expr-option-rename (c$::stmt-for-ambig->next c$::stmt)
                            subst)
        (stmt-rename (c$::stmt-for-ambig->body c$::stmt)
                     subst))
   :goto
   (c$::stmt-goto (ident-rename (c$::stmt-goto->label c$::stmt)
                                subst))
   :gotoe (stmt-gotoe (expr-rename (c$::stmt-gotoe->label c$::stmt)
                                   subst))
   :continue (stmt-fix c$::stmt)
   :break (stmt-fix c$::stmt)
   :return
   (c$::stmt-return
        (expr-option-rename (c$::stmt-return->expr? c$::stmt)
                            subst)
        (c$::stmt-return->info c$::stmt))
   :asm (c$::stmt-asm (asm-stmt-rename (c$::stmt-asm->stmt c$::stmt)
                                       subst)))))

Function: comp-stmt-rename

(defun comp-stmt-rename (comp-stmt subst)
  (declare (xargs :guard (and (comp-stmtp comp-stmt)
                              (ident-ident-alistp subst))))
  (declare (ignorable comp-stmt subst))
  (let ((__function__ 'comp-stmt-rename))
    (declare (ignorable __function__))
    (comp-stmt (comp-stmt->labels comp-stmt)
               (block-item-list-rename (comp-stmt->items comp-stmt)
                                       subst))))

Function: block-item-rename

(defun block-item-rename (c$::block-item subst)
 (declare (xargs :guard (and (block-itemp c$::block-item)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::block-item subst))
 (let ((__function__ 'block-item-rename))
  (declare (ignorable __function__))
  (block-item-case
   c$::block-item
   :declon
   (c$::block-item-declon
       (declon-rename (c$::block-item-declon->declon c$::block-item)
                      subst)
       (c$::block-item-declon->info c$::block-item))
   :stmt
   (c$::block-item-stmt
        (stmt-rename (c$::block-item-stmt->stmt c$::block-item)
                     subst)
        (c$::block-item-stmt->info c$::block-item))
   :ambig
   (c$::block-item-ambig
        (amb-declon/stmt-rename
             (c$::block-item-ambig->declon/stmt c$::block-item)
             subst)))))

Function: block-item-list-rename

(defun block-item-list-rename (c$::block-item-list subst)
  (declare (xargs :guard (and (block-item-listp c$::block-item-list)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'block-item-list-rename))
    (declare (ignorable __function__))
    (if (endp c$::block-item-list)
        nil
      (cons (block-item-rename (car c$::block-item-list)
                               subst)
            (block-item-list-rename (cdr c$::block-item-list)
                                    subst)))))

Function: amb-expr/tyname-rename

(defun amb-expr/tyname-rename (c$::amb-expr/tyname subst)
 (declare
      (xargs :guard (and (c$::amb-expr/tyname-p c$::amb-expr/tyname)
                         (ident-ident-alistp subst))))
 (declare (ignorable c$::amb-expr/tyname subst))
 (let ((__function__ 'amb-expr/tyname-rename))
  (declare (ignorable __function__))
  (c$::amb-expr/tyname
    (expr-rename (c$::amb-expr/tyname->expr c$::amb-expr/tyname)
                 subst)
    (tyname-rename (c$::amb-expr/tyname->tyname c$::amb-expr/tyname)
                   subst))))

Function: amb-declor/absdeclor-rename

(defun amb-declor/absdeclor-rename (c$::amb-declor/absdeclor subst)
 (declare
  (xargs
   :guard (and (c$::amb-declor/absdeclor-p c$::amb-declor/absdeclor)
               (ident-ident-alistp subst))))
 (declare (ignorable c$::amb-declor/absdeclor subst))
 (let ((__function__ 'amb-declor/absdeclor-rename))
  (declare (ignorable __function__))
  (c$::amb-declor/absdeclor
   (declor-rename
        (c$::amb-declor/absdeclor->declor c$::amb-declor/absdeclor)
        subst)
   (absdeclor-rename
      (c$::amb-declor/absdeclor->absdeclor c$::amb-declor/absdeclor)
      subst))))

Function: amb-declon/stmt-rename

(defun amb-declon/stmt-rename (c$::amb-declon/stmt subst)
 (declare
      (xargs :guard (and (c$::amb-declon/stmt-p c$::amb-declon/stmt)
                         (ident-ident-alistp subst))))
 (declare (ignorable c$::amb-declon/stmt subst))
 (let ((__function__ 'amb-declon/stmt-rename))
  (declare (ignorable __function__))
  (c$::amb-declon/stmt
    (declon-rename (c$::amb-declon/stmt->declon c$::amb-declon/stmt)
                   subst)
    (expr-rename (c$::amb-declon/stmt->expr c$::amb-declon/stmt)
                 subst))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: return-type-of-init-declor-list-rename.result

(defthm return-type-of-init-declor-list-rename.result
  (b* ((fty::?result
            (init-declor-list-rename c$::init-declor-list subst)))
    (init-declor-listp fty::result))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: expr-list-rename-type-prescription

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

Theorem: expr-list-rename-when-atom

(defthm expr-list-rename-when-atom
  (implies (atom c$::expr-list)
           (equal (expr-list-rename c$::expr-list subst)
                  nil)))

Theorem: expr-list-rename-of-cons

(defthm expr-list-rename-of-cons
  (equal (expr-list-rename (cons c$::expr c$::expr-list)
                           subst)
         (cons (expr-rename c$::expr subst)
               (expr-list-rename c$::expr-list subst))))

Theorem: expr-list-rename-of-append

(defthm expr-list-rename-of-append
  (equal (expr-list-rename (append acl2::x acl2::y)
                           subst)
         (append (expr-list-rename acl2::x subst)
                 (expr-list-rename acl2::y subst))))

Theorem: consp-of-expr-list-rename

(defthm consp-of-expr-list-rename
  (equal (consp (expr-list-rename c$::expr-list subst))
         (consp c$::expr-list)))

Theorem: len-of-expr-list-rename

(defthm len-of-expr-list-rename
  (equal (len (expr-list-rename c$::expr-list subst))
         (len c$::expr-list)))

Theorem: nth-of-expr-list-rename

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

Theorem: expr-list-rename-of-revappend

(defthm expr-list-rename-of-revappend
  (equal (expr-list-rename (revappend acl2::x acl2::y)
                           subst)
         (revappend (expr-list-rename acl2::x subst)
                    (expr-list-rename acl2::y subst))))

Theorem: expr-list-rename-of-reverse

(defthm expr-list-rename-of-reverse
  (equal (expr-list-rename (reverse c$::expr-list)
                           subst)
         (reverse (expr-list-rename c$::expr-list subst))))

Theorem: expr-option-rename-under-iff

(defthm expr-option-rename-under-iff
  (iff (expr-option-rename c$::expr-option subst)
       c$::expr-option))

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

(defthm const-expr-option-rename-under-iff
  (iff (const-expr-option-rename c$::const-expr-option subst)
       c$::const-expr-option))

Theorem: genassoc-list-rename-type-prescription

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

Theorem: genassoc-list-rename-when-atom

(defthm genassoc-list-rename-when-atom
  (implies (atom c$::genassoc-list)
           (equal (genassoc-list-rename c$::genassoc-list subst)
                  nil)))

Theorem: genassoc-list-rename-of-cons

(defthm genassoc-list-rename-of-cons
  (equal (genassoc-list-rename (cons c$::genassoc c$::genassoc-list)
                               subst)
         (cons (genassoc-rename c$::genassoc subst)
               (genassoc-list-rename c$::genassoc-list subst))))

Theorem: genassoc-list-rename-of-append

(defthm genassoc-list-rename-of-append
  (equal (genassoc-list-rename (append acl2::x acl2::y)
                               subst)
         (append (genassoc-list-rename acl2::x subst)
                 (genassoc-list-rename acl2::y subst))))

Theorem: consp-of-genassoc-list-rename

(defthm consp-of-genassoc-list-rename
  (equal (consp (genassoc-list-rename c$::genassoc-list subst))
         (consp c$::genassoc-list)))

Theorem: len-of-genassoc-list-rename

(defthm len-of-genassoc-list-rename
  (equal (len (genassoc-list-rename c$::genassoc-list subst))
         (len c$::genassoc-list)))

Theorem: nth-of-genassoc-list-rename

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

Theorem: genassoc-list-rename-of-revappend

(defthm genassoc-list-rename-of-revappend
  (equal (genassoc-list-rename (revappend acl2::x acl2::y)
                               subst)
         (revappend (genassoc-list-rename acl2::x subst)
                    (genassoc-list-rename acl2::y subst))))

Theorem: genassoc-list-rename-of-reverse

(defthm genassoc-list-rename-of-reverse
  (equal (genassoc-list-rename (reverse c$::genassoc-list)
                               subst)
         (reverse (genassoc-list-rename c$::genassoc-list subst))))

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

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

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

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

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

(defthm spec/qual-list-rename-of-cons
 (equal
      (spec/qual-list-rename (cons c$::spec/qual c$::spec/qual-list)
                             subst)
      (cons (spec/qual-rename c$::spec/qual subst)
            (spec/qual-list-rename c$::spec/qual-list subst))))

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

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

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

(defthm consp-of-spec/qual-list-rename
  (equal (consp (spec/qual-list-rename c$::spec/qual-list subst))
         (consp c$::spec/qual-list)))

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

(defthm len-of-spec/qual-list-rename
  (equal (len (spec/qual-list-rename c$::spec/qual-list subst))
         (len c$::spec/qual-list)))

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

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

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

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

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

(defthm spec/qual-list-rename-of-reverse
 (equal (spec/qual-list-rename (reverse c$::spec/qual-list)
                               subst)
        (reverse (spec/qual-list-rename c$::spec/qual-list subst))))

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

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

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

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

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

(defthm decl-spec-list-rename-of-cons
 (equal
      (decl-spec-list-rename (cons c$::decl-spec c$::decl-spec-list)
                             subst)
      (cons (decl-spec-rename c$::decl-spec subst)
            (decl-spec-list-rename c$::decl-spec-list subst))))

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

(defthm decl-spec-list-rename-of-append
  (equal (decl-spec-list-rename (append acl2::x acl2::y)
                                subst)
         (append (decl-spec-list-rename acl2::x subst)
                 (decl-spec-list-rename acl2::y subst))))

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

(defthm consp-of-decl-spec-list-rename
  (equal (consp (decl-spec-list-rename c$::decl-spec-list subst))
         (consp c$::decl-spec-list)))

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

(defthm len-of-decl-spec-list-rename
  (equal (len (decl-spec-list-rename c$::decl-spec-list subst))
         (len c$::decl-spec-list)))

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

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

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

(defthm decl-spec-list-rename-of-revappend
  (equal (decl-spec-list-rename (revappend acl2::x acl2::y)
                                subst)
         (revappend (decl-spec-list-rename acl2::x subst)
                    (decl-spec-list-rename acl2::y subst))))

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

(defthm decl-spec-list-rename-of-reverse
 (equal (decl-spec-list-rename (reverse c$::decl-spec-list)
                               subst)
        (reverse (decl-spec-list-rename c$::decl-spec-list subst))))

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

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

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

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

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

(defthm typequal/attribspec-list-rename-of-cons
 (equal
    (typequal/attribspec-list-rename
         (cons c$::typequal/attribspec
               c$::typequal/attribspec-list)
         subst)
    (cons (typequal/attribspec-rename c$::typequal/attribspec subst)
          (typequal/attribspec-list-rename
               c$::typequal/attribspec-list subst))))

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

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

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

(defthm consp-of-typequal/attribspec-list-rename
  (equal (consp (typequal/attribspec-list-rename
                     c$::typequal/attribspec-list subst))
         (consp c$::typequal/attribspec-list)))

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

(defthm len-of-typequal/attribspec-list-rename
  (equal (len (typequal/attribspec-list-rename
                   c$::typequal/attribspec-list subst))
         (len c$::typequal/attribspec-list)))

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

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

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

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

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

(defthm typequal/attribspec-list-rename-of-reverse
  (equal (typequal/attribspec-list-rename
              (reverse c$::typequal/attribspec-list)
              subst)
         (reverse (typequal/attribspec-list-rename
                       c$::typequal/attribspec-list subst))))

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

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

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

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

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

(defthm typequal/attribspec-list-list-rename-of-cons
  (equal (typequal/attribspec-list-list-rename
              (cons c$::typequal/attribspec-list
                    c$::typequal/attribspec-list-list)
              subst)
         (cons (typequal/attribspec-list-rename
                    c$::typequal/attribspec-list subst)
               (typequal/attribspec-list-list-rename
                    c$::typequal/attribspec-list-list
                    subst))))

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

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

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

(defthm consp-of-typequal/attribspec-list-list-rename
  (equal (consp (typequal/attribspec-list-list-rename
                     c$::typequal/attribspec-list-list
                     subst))
         (consp c$::typequal/attribspec-list-list)))

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

(defthm len-of-typequal/attribspec-list-list-rename
  (equal (len (typequal/attribspec-list-list-rename
                   c$::typequal/attribspec-list-list
                   subst))
         (len c$::typequal/attribspec-list-list)))

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

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

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

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

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

(defthm typequal/attribspec-list-list-rename-of-reverse
  (equal (typequal/attribspec-list-list-rename
              (reverse c$::typequal/attribspec-list-list)
              subst)
         (reverse (typequal/attribspec-list-list-rename
                       c$::typequal/attribspec-list-list
                       subst))))

Theorem: initer-option-rename-under-iff

(defthm initer-option-rename-under-iff
  (iff (initer-option-rename c$::initer-option subst)
       c$::initer-option))

Theorem: desiniter-list-rename-type-prescription

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

Theorem: desiniter-list-rename-when-atom

(defthm desiniter-list-rename-when-atom
  (implies (atom c$::desiniter-list)
           (equal (desiniter-list-rename c$::desiniter-list subst)
                  nil)))

Theorem: desiniter-list-rename-of-cons

(defthm desiniter-list-rename-of-cons
  (equal (desiniter-list-rename (cons desiniter c$::desiniter-list)
                                subst)
         (cons (desiniter-rename desiniter subst)
               (desiniter-list-rename c$::desiniter-list subst))))

Theorem: desiniter-list-rename-of-append

(defthm desiniter-list-rename-of-append
  (equal (desiniter-list-rename (append acl2::x acl2::y)
                                subst)
         (append (desiniter-list-rename acl2::x subst)
                 (desiniter-list-rename acl2::y subst))))

Theorem: consp-of-desiniter-list-rename

(defthm consp-of-desiniter-list-rename
  (equal (consp (desiniter-list-rename c$::desiniter-list subst))
         (consp c$::desiniter-list)))

Theorem: len-of-desiniter-list-rename

(defthm len-of-desiniter-list-rename
  (equal (len (desiniter-list-rename c$::desiniter-list subst))
         (len c$::desiniter-list)))

Theorem: nth-of-desiniter-list-rename

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

Theorem: desiniter-list-rename-of-revappend

(defthm desiniter-list-rename-of-revappend
  (equal (desiniter-list-rename (revappend acl2::x acl2::y)
                                subst)
         (revappend (desiniter-list-rename acl2::x subst)
                    (desiniter-list-rename acl2::y subst))))

Theorem: desiniter-list-rename-of-reverse

(defthm desiniter-list-rename-of-reverse
 (equal (desiniter-list-rename (reverse c$::desiniter-list)
                               subst)
        (reverse (desiniter-list-rename c$::desiniter-list subst))))

Theorem: designor-list-rename-type-prescription

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

Theorem: designor-list-rename-when-atom

(defthm designor-list-rename-when-atom
  (implies (atom c$::designor-list)
           (equal (designor-list-rename c$::designor-list subst)
                  nil)))

Theorem: designor-list-rename-of-cons

(defthm designor-list-rename-of-cons
  (equal (designor-list-rename (cons c$::designor c$::designor-list)
                               subst)
         (cons (designor-rename c$::designor subst)
               (designor-list-rename c$::designor-list subst))))

Theorem: designor-list-rename-of-append

(defthm designor-list-rename-of-append
  (equal (designor-list-rename (append acl2::x acl2::y)
                               subst)
         (append (designor-list-rename acl2::x subst)
                 (designor-list-rename acl2::y subst))))

Theorem: consp-of-designor-list-rename

(defthm consp-of-designor-list-rename
  (equal (consp (designor-list-rename c$::designor-list subst))
         (consp c$::designor-list)))

Theorem: len-of-designor-list-rename

(defthm len-of-designor-list-rename
  (equal (len (designor-list-rename c$::designor-list subst))
         (len c$::designor-list)))

Theorem: nth-of-designor-list-rename

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

Theorem: designor-list-rename-of-revappend

(defthm designor-list-rename-of-revappend
  (equal (designor-list-rename (revappend acl2::x acl2::y)
                               subst)
         (revappend (designor-list-rename acl2::x subst)
                    (designor-list-rename acl2::y subst))))

Theorem: designor-list-rename-of-reverse

(defthm designor-list-rename-of-reverse
  (equal (designor-list-rename (reverse c$::designor-list)
                               subst)
         (reverse (designor-list-rename c$::designor-list subst))))

Theorem: declor-option-rename-under-iff

(defthm declor-option-rename-under-iff
  (iff (declor-option-rename c$::declor-option subst)
       c$::declor-option))

Theorem: absdeclor-option-rename-under-iff

(defthm absdeclor-option-rename-under-iff
  (iff (absdeclor-option-rename c$::absdeclor-option subst)
       c$::absdeclor-option))

Theorem: dirabsdeclor-option-rename-under-iff

(defthm dirabsdeclor-option-rename-under-iff
  (iff (dirabsdeclor-option-rename c$::dirabsdeclor-option subst)
       c$::dirabsdeclor-option))

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

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

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

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

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

(defthm param-declon-list-rename-of-cons
 (equal
     (param-declon-list-rename
          (cons param-declon c$::param-declon-list)
          subst)
     (cons (param-declon-rename param-declon subst)
           (param-declon-list-rename c$::param-declon-list subst))))

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

(defthm param-declon-list-rename-of-append
  (equal (param-declon-list-rename (append acl2::x acl2::y)
                                   subst)
         (append (param-declon-list-rename acl2::x subst)
                 (param-declon-list-rename acl2::y subst))))

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

(defthm consp-of-param-declon-list-rename
 (equal
      (consp (param-declon-list-rename c$::param-declon-list subst))
      (consp c$::param-declon-list)))

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

(defthm len-of-param-declon-list-rename
 (equal (len (param-declon-list-rename c$::param-declon-list subst))
        (len c$::param-declon-list)))

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

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

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

(defthm param-declon-list-rename-of-revappend
  (equal (param-declon-list-rename (revappend acl2::x acl2::y)
                                   subst)
         (revappend (param-declon-list-rename acl2::x subst)
                    (param-declon-list-rename acl2::y subst))))

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

(defthm param-declon-list-rename-of-reverse
 (equal
  (param-declon-list-rename (reverse c$::param-declon-list)
                            subst)
  (reverse (param-declon-list-rename c$::param-declon-list subst))))

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

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

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

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

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

(defthm struct-declon-list-rename-of-cons
 (equal
   (struct-declon-list-rename (cons c$::struct-declon
                                    c$::struct-declon-list)
                              subst)
   (cons (struct-declon-rename c$::struct-declon subst)
         (struct-declon-list-rename c$::struct-declon-list subst))))

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

(defthm struct-declon-list-rename-of-append
  (equal (struct-declon-list-rename (append acl2::x acl2::y)
                                    subst)
         (append (struct-declon-list-rename acl2::x subst)
                 (struct-declon-list-rename acl2::y subst))))

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

(defthm consp-of-struct-declon-list-rename
 (equal
    (consp (struct-declon-list-rename c$::struct-declon-list subst))
    (consp c$::struct-declon-list)))

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

(defthm len-of-struct-declon-list-rename
 (equal
      (len (struct-declon-list-rename c$::struct-declon-list subst))
      (len c$::struct-declon-list)))

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

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

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

(defthm struct-declon-list-rename-of-revappend
  (equal (struct-declon-list-rename (revappend acl2::x acl2::y)
                                    subst)
         (revappend (struct-declon-list-rename acl2::x subst)
                    (struct-declon-list-rename acl2::y subst))))

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

(defthm struct-declon-list-rename-of-reverse
 (equal
    (struct-declon-list-rename (reverse c$::struct-declon-list)
                               subst)
    (reverse
         (struct-declon-list-rename c$::struct-declon-list subst))))

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

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

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

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

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

(defthm struct-declor-list-rename-of-cons
 (equal
   (struct-declor-list-rename
        (cons struct-declor c$::struct-declor-list)
        subst)
   (cons (struct-declor-rename struct-declor subst)
         (struct-declor-list-rename c$::struct-declor-list subst))))

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

(defthm struct-declor-list-rename-of-append
  (equal (struct-declor-list-rename (append acl2::x acl2::y)
                                    subst)
         (append (struct-declor-list-rename acl2::x subst)
                 (struct-declor-list-rename acl2::y subst))))

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

(defthm consp-of-struct-declor-list-rename
 (equal
    (consp (struct-declor-list-rename c$::struct-declor-list subst))
    (consp c$::struct-declor-list)))

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

(defthm len-of-struct-declor-list-rename
 (equal
      (len (struct-declor-list-rename c$::struct-declor-list subst))
      (len c$::struct-declor-list)))

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

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

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

(defthm struct-declor-list-rename-of-revappend
  (equal (struct-declor-list-rename (revappend acl2::x acl2::y)
                                    subst)
         (revappend (struct-declor-list-rename acl2::x subst)
                    (struct-declor-list-rename acl2::y subst))))

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

(defthm struct-declor-list-rename-of-reverse
 (equal
    (struct-declor-list-rename (reverse c$::struct-declor-list)
                               subst)
    (reverse
         (struct-declor-list-rename c$::struct-declor-list subst))))

Theorem: enumer-list-rename-type-prescription

(defthm enumer-list-rename-type-prescription
  (true-listp (enumer-list-rename c$::enumer-list subst))
  :rule-classes :type-prescription)

Theorem: enumer-list-rename-when-atom

(defthm enumer-list-rename-when-atom
  (implies (atom c$::enumer-list)
           (equal (enumer-list-rename c$::enumer-list subst)
                  nil)))

Theorem: enumer-list-rename-of-cons

(defthm enumer-list-rename-of-cons
  (equal (enumer-list-rename (cons enumer c$::enumer-list)
                             subst)
         (cons (enumer-rename enumer subst)
               (enumer-list-rename c$::enumer-list subst))))

Theorem: enumer-list-rename-of-append

(defthm enumer-list-rename-of-append
  (equal (enumer-list-rename (append acl2::x acl2::y)
                             subst)
         (append (enumer-list-rename acl2::x subst)
                 (enumer-list-rename acl2::y subst))))

Theorem: consp-of-enumer-list-rename

(defthm consp-of-enumer-list-rename
  (equal (consp (enumer-list-rename c$::enumer-list subst))
         (consp c$::enumer-list)))

Theorem: len-of-enumer-list-rename

(defthm len-of-enumer-list-rename
  (equal (len (enumer-list-rename c$::enumer-list subst))
         (len c$::enumer-list)))

Theorem: nth-of-enumer-list-rename

(defthm nth-of-enumer-list-rename
  (equal (nth acl2::n
              (enumer-list-rename c$::enumer-list subst))
         (if (< (nfix acl2::n) (len c$::enumer-list))
             (enumer-rename (nth acl2::n c$::enumer-list)
                            subst)
           nil)))

Theorem: enumer-list-rename-of-revappend

(defthm enumer-list-rename-of-revappend
  (equal (enumer-list-rename (revappend acl2::x acl2::y)
                             subst)
         (revappend (enumer-list-rename acl2::x subst)
                    (enumer-list-rename acl2::y subst))))

Theorem: enumer-list-rename-of-reverse

(defthm enumer-list-rename-of-reverse
  (equal (enumer-list-rename (reverse c$::enumer-list)
                             subst)
         (reverse (enumer-list-rename c$::enumer-list subst))))

Theorem: attrib-list-rename-type-prescription

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

Theorem: attrib-list-rename-when-atom

(defthm attrib-list-rename-when-atom
  (implies (atom c$::attrib-list)
           (equal (attrib-list-rename c$::attrib-list subst)
                  nil)))

Theorem: attrib-list-rename-of-cons

(defthm attrib-list-rename-of-cons
  (equal (attrib-list-rename (cons c$::attrib c$::attrib-list)
                             subst)
         (cons (attrib-rename c$::attrib subst)
               (attrib-list-rename c$::attrib-list subst))))

Theorem: attrib-list-rename-of-append

(defthm attrib-list-rename-of-append
  (equal (attrib-list-rename (append acl2::x acl2::y)
                             subst)
         (append (attrib-list-rename acl2::x subst)
                 (attrib-list-rename acl2::y subst))))

Theorem: consp-of-attrib-list-rename

(defthm consp-of-attrib-list-rename
  (equal (consp (attrib-list-rename c$::attrib-list subst))
         (consp c$::attrib-list)))

Theorem: len-of-attrib-list-rename

(defthm len-of-attrib-list-rename
  (equal (len (attrib-list-rename c$::attrib-list subst))
         (len c$::attrib-list)))

Theorem: nth-of-attrib-list-rename

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

Theorem: attrib-list-rename-of-revappend

(defthm attrib-list-rename-of-revappend
  (equal (attrib-list-rename (revappend acl2::x acl2::y)
                             subst)
         (revappend (attrib-list-rename acl2::x subst)
                    (attrib-list-rename acl2::y subst))))

Theorem: attrib-list-rename-of-reverse

(defthm attrib-list-rename-of-reverse
  (equal (attrib-list-rename (reverse c$::attrib-list)
                             subst)
         (reverse (attrib-list-rename c$::attrib-list subst))))

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

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

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

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

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

(defthm attrib-spec-list-rename-of-cons
  (equal
       (attrib-spec-list-rename
            (cons c$::attrib-spec c$::attrib-spec-list)
            subst)
       (cons (attrib-spec-rename c$::attrib-spec subst)
             (attrib-spec-list-rename c$::attrib-spec-list subst))))

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

(defthm attrib-spec-list-rename-of-append
  (equal (attrib-spec-list-rename (append acl2::x acl2::y)
                                  subst)
         (append (attrib-spec-list-rename acl2::x subst)
                 (attrib-spec-list-rename acl2::y subst))))

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

(defthm consp-of-attrib-spec-list-rename
 (equal (consp (attrib-spec-list-rename c$::attrib-spec-list subst))
        (consp c$::attrib-spec-list)))

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

(defthm len-of-attrib-spec-list-rename
  (equal (len (attrib-spec-list-rename c$::attrib-spec-list subst))
         (len c$::attrib-spec-list)))

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

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

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

(defthm attrib-spec-list-rename-of-revappend
  (equal (attrib-spec-list-rename (revappend acl2::x acl2::y)
                                  subst)
         (revappend (attrib-spec-list-rename acl2::x subst)
                    (attrib-spec-list-rename acl2::y subst))))

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

(defthm attrib-spec-list-rename-of-reverse
 (equal
    (attrib-spec-list-rename (reverse c$::attrib-spec-list)
                             subst)
    (reverse (attrib-spec-list-rename c$::attrib-spec-list subst))))

Theorem: init-declor-list-rename-type-prescription

(defthm init-declor-list-rename-type-prescription
  (true-listp (init-declor-list-rename c$::init-declor-list subst))
  :rule-classes :type-prescription)

Theorem: init-declor-list-rename-when-atom

(defthm init-declor-list-rename-when-atom
  (implies
       (atom c$::init-declor-list)
       (equal (init-declor-list-rename c$::init-declor-list subst)
              nil)))

Theorem: init-declor-list-rename-of-cons

(defthm init-declor-list-rename-of-cons
 (equal
    (init-declor-list-rename (cons init-declor c$::init-declor-list)
                             subst)
    (cons (init-declor-rename init-declor subst)
          (init-declor-list-rename c$::init-declor-list subst))))

Theorem: init-declor-list-rename-of-append

(defthm init-declor-list-rename-of-append
  (equal (init-declor-list-rename (append acl2::x acl2::y)
                                  subst)
         (append (init-declor-list-rename acl2::x subst)
                 (init-declor-list-rename acl2::y subst))))

Theorem: consp-of-init-declor-list-rename

(defthm consp-of-init-declor-list-rename
 (equal (consp (init-declor-list-rename c$::init-declor-list subst))
        (consp c$::init-declor-list)))

Theorem: len-of-init-declor-list-rename

(defthm len-of-init-declor-list-rename
  (equal (len (init-declor-list-rename c$::init-declor-list subst))
         (len c$::init-declor-list)))

Theorem: nth-of-init-declor-list-rename

(defthm nth-of-init-declor-list-rename
  (equal (nth acl2::n
              (init-declor-list-rename c$::init-declor-list subst))
         (if (< (nfix acl2::n)
                (len c$::init-declor-list))
             (init-declor-rename (nth acl2::n c$::init-declor-list)
                                 subst)
           nil)))

Theorem: init-declor-list-rename-of-revappend

(defthm init-declor-list-rename-of-revappend
  (equal (init-declor-list-rename (revappend acl2::x acl2::y)
                                  subst)
         (revappend (init-declor-list-rename acl2::x subst)
                    (init-declor-list-rename acl2::y subst))))

Theorem: init-declor-list-rename-of-reverse

(defthm init-declor-list-rename-of-reverse
 (equal
    (init-declor-list-rename (reverse c$::init-declor-list)
                             subst)
    (reverse (init-declor-list-rename c$::init-declor-list subst))))

Theorem: declon-list-rename-type-prescription

(defthm declon-list-rename-type-prescription
  (true-listp (declon-list-rename c$::declon-list subst))
  :rule-classes :type-prescription)

Theorem: declon-list-rename-when-atom

(defthm declon-list-rename-when-atom
  (implies (atom c$::declon-list)
           (equal (declon-list-rename c$::declon-list subst)
                  nil)))

Theorem: declon-list-rename-of-cons

(defthm declon-list-rename-of-cons
  (equal (declon-list-rename (cons declon c$::declon-list)
                             subst)
         (cons (declon-rename declon subst)
               (declon-list-rename c$::declon-list subst))))

Theorem: declon-list-rename-of-append

(defthm declon-list-rename-of-append
  (equal (declon-list-rename (append acl2::x acl2::y)
                             subst)
         (append (declon-list-rename acl2::x subst)
                 (declon-list-rename acl2::y subst))))

Theorem: consp-of-declon-list-rename

(defthm consp-of-declon-list-rename
  (equal (consp (declon-list-rename c$::declon-list subst))
         (consp c$::declon-list)))

Theorem: len-of-declon-list-rename

(defthm len-of-declon-list-rename
  (equal (len (declon-list-rename c$::declon-list subst))
         (len c$::declon-list)))

Theorem: nth-of-declon-list-rename

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

Theorem: declon-list-rename-of-revappend

(defthm declon-list-rename-of-revappend
  (equal (declon-list-rename (revappend acl2::x acl2::y)
                             subst)
         (revappend (declon-list-rename acl2::x subst)
                    (declon-list-rename acl2::y subst))))

Theorem: declon-list-rename-of-reverse

(defthm declon-list-rename-of-reverse
  (equal (declon-list-rename (reverse c$::declon-list)
                             subst)
         (reverse (declon-list-rename c$::declon-list subst))))

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

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

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

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

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

(defthm asm-output-list-rename-of-cons
 (equal
   (asm-output-list-rename (cons c$::asm-output c$::asm-output-list)
                           subst)
   (cons (asm-output-rename c$::asm-output subst)
         (asm-output-list-rename c$::asm-output-list subst))))

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

(defthm asm-output-list-rename-of-append
  (equal (asm-output-list-rename (append acl2::x acl2::y)
                                 subst)
         (append (asm-output-list-rename acl2::x subst)
                 (asm-output-list-rename acl2::y subst))))

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

(defthm consp-of-asm-output-list-rename
  (equal (consp (asm-output-list-rename c$::asm-output-list subst))
         (consp c$::asm-output-list)))

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

(defthm len-of-asm-output-list-rename
  (equal (len (asm-output-list-rename c$::asm-output-list subst))
         (len c$::asm-output-list)))

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

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

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

(defthm asm-output-list-rename-of-revappend
  (equal (asm-output-list-rename (revappend acl2::x acl2::y)
                                 subst)
         (revappend (asm-output-list-rename acl2::x subst)
                    (asm-output-list-rename acl2::y subst))))

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

(defthm asm-output-list-rename-of-reverse
 (equal
      (asm-output-list-rename (reverse c$::asm-output-list)
                              subst)
      (reverse (asm-output-list-rename c$::asm-output-list subst))))

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

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

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

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

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

(defthm asm-input-list-rename-of-cons
 (equal
      (asm-input-list-rename (cons c$::asm-input c$::asm-input-list)
                             subst)
      (cons (asm-input-rename c$::asm-input subst)
            (asm-input-list-rename c$::asm-input-list subst))))

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

(defthm asm-input-list-rename-of-append
  (equal (asm-input-list-rename (append acl2::x acl2::y)
                                subst)
         (append (asm-input-list-rename acl2::x subst)
                 (asm-input-list-rename acl2::y subst))))

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

(defthm consp-of-asm-input-list-rename
  (equal (consp (asm-input-list-rename c$::asm-input-list subst))
         (consp c$::asm-input-list)))

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

(defthm len-of-asm-input-list-rename
  (equal (len (asm-input-list-rename c$::asm-input-list subst))
         (len c$::asm-input-list)))

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

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

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

(defthm asm-input-list-rename-of-revappend
  (equal (asm-input-list-rename (revappend acl2::x acl2::y)
                                subst)
         (revappend (asm-input-list-rename acl2::x subst)
                    (asm-input-list-rename acl2::y subst))))

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

(defthm asm-input-list-rename-of-reverse
 (equal (asm-input-list-rename (reverse c$::asm-input-list)
                               subst)
        (reverse (asm-input-list-rename c$::asm-input-list subst))))

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

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

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

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

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

(defthm block-item-list-rename-of-cons
 (equal
   (block-item-list-rename (cons c$::block-item c$::block-item-list)
                           subst)
   (cons (block-item-rename c$::block-item subst)
         (block-item-list-rename c$::block-item-list subst))))

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

(defthm block-item-list-rename-of-append
  (equal (block-item-list-rename (append acl2::x acl2::y)
                                 subst)
         (append (block-item-list-rename acl2::x subst)
                 (block-item-list-rename acl2::y subst))))

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

(defthm consp-of-block-item-list-rename
  (equal (consp (block-item-list-rename c$::block-item-list subst))
         (consp c$::block-item-list)))

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

(defthm len-of-block-item-list-rename
  (equal (len (block-item-list-rename c$::block-item-list subst))
         (len c$::block-item-list)))

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

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

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

(defthm block-item-list-rename-of-revappend
  (equal (block-item-list-rename (revappend acl2::x acl2::y)
                                 subst)
         (revappend (block-item-list-rename acl2::x subst)
                    (block-item-list-rename acl2::y subst))))

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

(defthm block-item-list-rename-of-reverse
 (equal
      (block-item-list-rename (reverse c$::block-item-list)
                              subst)
      (reverse (block-item-list-rename c$::block-item-list subst))))

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

(defthm expr-rename-of-expr-fix-expr
  (equal (expr-rename (expr-fix c$::expr) subst)
         (expr-rename c$::expr subst)))

Theorem: expr-rename-of-ident-ident-alist-fix-subst

(defthm expr-rename-of-ident-ident-alist-fix-subst
  (equal (expr-rename c$::expr (ident-ident-alist-fix subst))
         (expr-rename c$::expr subst)))

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

(defthm expr-list-rename-of-expr-list-fix-expr-list
  (equal (expr-list-rename (expr-list-fix c$::expr-list)
                           subst)
         (expr-list-rename c$::expr-list subst)))

Theorem: expr-list-rename-of-ident-ident-alist-fix-subst

(defthm expr-list-rename-of-ident-ident-alist-fix-subst
  (equal (expr-list-rename c$::expr-list
                           (ident-ident-alist-fix subst))
         (expr-list-rename c$::expr-list subst)))

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

(defthm expr-option-rename-of-expr-option-fix-expr-option
  (equal (expr-option-rename (expr-option-fix c$::expr-option)
                             subst)
         (expr-option-rename c$::expr-option subst)))

Theorem: expr-option-rename-of-ident-ident-alist-fix-subst

(defthm expr-option-rename-of-ident-ident-alist-fix-subst
  (equal (expr-option-rename c$::expr-option
                             (ident-ident-alist-fix subst))
         (expr-option-rename c$::expr-option subst)))

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

(defthm const-expr-rename-of-const-expr-fix-const-expr
  (equal (const-expr-rename (c$::const-expr-fix const-expr)
                            subst)
         (const-expr-rename const-expr subst)))

Theorem: const-expr-rename-of-ident-ident-alist-fix-subst

(defthm const-expr-rename-of-ident-ident-alist-fix-subst
  (equal (const-expr-rename const-expr
                            (ident-ident-alist-fix subst))
         (const-expr-rename const-expr subst)))

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

(defthm
 const-expr-option-rename-of-const-expr-option-fix-const-expr-option
 (equal (const-expr-option-rename
             (const-expr-option-fix c$::const-expr-option)
             subst)
        (const-expr-option-rename c$::const-expr-option subst)))

Theorem: const-expr-option-rename-of-ident-ident-alist-fix-subst

(defthm const-expr-option-rename-of-ident-ident-alist-fix-subst
  (equal (const-expr-option-rename c$::const-expr-option
                                   (ident-ident-alist-fix subst))
         (const-expr-option-rename c$::const-expr-option subst)))

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

(defthm genassoc-rename-of-genassoc-fix-genassoc
  (equal (genassoc-rename (genassoc-fix c$::genassoc)
                          subst)
         (genassoc-rename c$::genassoc subst)))

Theorem: genassoc-rename-of-ident-ident-alist-fix-subst

(defthm genassoc-rename-of-ident-ident-alist-fix-subst
  (equal (genassoc-rename c$::genassoc
                          (ident-ident-alist-fix subst))
         (genassoc-rename c$::genassoc subst)))

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

(defthm genassoc-list-rename-of-genassoc-list-fix-genassoc-list
  (equal (genassoc-list-rename (genassoc-list-fix c$::genassoc-list)
                               subst)
         (genassoc-list-rename c$::genassoc-list subst)))

Theorem: genassoc-list-rename-of-ident-ident-alist-fix-subst

(defthm genassoc-list-rename-of-ident-ident-alist-fix-subst
  (equal (genassoc-list-rename c$::genassoc-list
                               (ident-ident-alist-fix subst))
         (genassoc-list-rename c$::genassoc-list subst)))

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

(defthm
      member-designor-rename-of-member-designor-fix-member-designor
 (equal
   (member-designor-rename (member-designor-fix c$::member-designor)
                           subst)
   (member-designor-rename c$::member-designor subst)))

Theorem: member-designor-rename-of-ident-ident-alist-fix-subst

(defthm member-designor-rename-of-ident-ident-alist-fix-subst
  (equal (member-designor-rename c$::member-designor
                                 (ident-ident-alist-fix subst))
         (member-designor-rename c$::member-designor subst)))

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

(defthm type-spec-rename-of-type-spec-fix-type-spec
  (equal (type-spec-rename (type-spec-fix c$::type-spec)
                           subst)
         (type-spec-rename c$::type-spec subst)))

Theorem: type-spec-rename-of-ident-ident-alist-fix-subst

(defthm type-spec-rename-of-ident-ident-alist-fix-subst
  (equal (type-spec-rename c$::type-spec
                           (ident-ident-alist-fix subst))
         (type-spec-rename c$::type-spec subst)))

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

(defthm spec/qual-rename-of-spec/qual-fix-spec/qual
  (equal (spec/qual-rename (spec/qual-fix c$::spec/qual)
                           subst)
         (spec/qual-rename c$::spec/qual subst)))

Theorem: spec/qual-rename-of-ident-ident-alist-fix-subst

(defthm spec/qual-rename-of-ident-ident-alist-fix-subst
  (equal (spec/qual-rename c$::spec/qual
                           (ident-ident-alist-fix subst))
         (spec/qual-rename c$::spec/qual subst)))

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

(defthm spec/qual-list-rename-of-spec/qual-list-fix-spec/qual-list
 (equal
      (spec/qual-list-rename (spec/qual-list-fix c$::spec/qual-list)
                             subst)
      (spec/qual-list-rename c$::spec/qual-list subst)))

Theorem: spec/qual-list-rename-of-ident-ident-alist-fix-subst

(defthm spec/qual-list-rename-of-ident-ident-alist-fix-subst
  (equal (spec/qual-list-rename c$::spec/qual-list
                                (ident-ident-alist-fix subst))
         (spec/qual-list-rename c$::spec/qual-list subst)))

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

(defthm align-spec-rename-of-align-spec-fix-align-spec
  (equal (align-spec-rename (align-spec-fix c$::align-spec)
                            subst)
         (align-spec-rename c$::align-spec subst)))

Theorem: align-spec-rename-of-ident-ident-alist-fix-subst

(defthm align-spec-rename-of-ident-ident-alist-fix-subst
  (equal (align-spec-rename c$::align-spec
                            (ident-ident-alist-fix subst))
         (align-spec-rename c$::align-spec subst)))

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

(defthm decl-spec-rename-of-decl-spec-fix-decl-spec
  (equal (decl-spec-rename (decl-spec-fix c$::decl-spec)
                           subst)
         (decl-spec-rename c$::decl-spec subst)))

Theorem: decl-spec-rename-of-ident-ident-alist-fix-subst

(defthm decl-spec-rename-of-ident-ident-alist-fix-subst
  (equal (decl-spec-rename c$::decl-spec
                           (ident-ident-alist-fix subst))
         (decl-spec-rename c$::decl-spec subst)))

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

(defthm decl-spec-list-rename-of-decl-spec-list-fix-decl-spec-list
 (equal
      (decl-spec-list-rename (decl-spec-list-fix c$::decl-spec-list)
                             subst)
      (decl-spec-list-rename c$::decl-spec-list subst)))

Theorem: decl-spec-list-rename-of-ident-ident-alist-fix-subst

(defthm decl-spec-list-rename-of-ident-ident-alist-fix-subst
  (equal (decl-spec-list-rename c$::decl-spec-list
                                (ident-ident-alist-fix subst))
         (decl-spec-list-rename c$::decl-spec-list subst)))

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

(defthm
 typequal/attribspec-rename-of-typequal/attribspec-fix-typequal/attribspec
 (equal (typequal/attribspec-rename
             (c$::typequal/attribspec-fix c$::typequal/attribspec)
             subst)
        (typequal/attribspec-rename c$::typequal/attribspec subst)))

Theorem: typequal/attribspec-rename-of-ident-ident-alist-fix-subst

(defthm typequal/attribspec-rename-of-ident-ident-alist-fix-subst
 (equal (typequal/attribspec-rename c$::typequal/attribspec
                                    (ident-ident-alist-fix subst))
        (typequal/attribspec-rename c$::typequal/attribspec subst)))

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

(defthm
 typequal/attribspec-list-rename-of-typequal/attribspec-list-fix-typequal/attribspec-list
 (equal
  (typequal/attribspec-list-rename
     (c$::typequal/attribspec-list-fix c$::typequal/attribspec-list)
     subst)
  (typequal/attribspec-list-rename
       c$::typequal/attribspec-list subst)))

Theorem: typequal/attribspec-list-rename-of-ident-ident-alist-fix-subst

(defthm
     typequal/attribspec-list-rename-of-ident-ident-alist-fix-subst
 (equal
     (typequal/attribspec-list-rename c$::typequal/attribspec-list
                                      (ident-ident-alist-fix subst))
     (typequal/attribspec-list-rename
          c$::typequal/attribspec-list subst)))

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

(defthm
 typequal/attribspec-list-list-rename-of-typequal/attribspec-list-list-fix-typequal/attribspec-list-list
 (equal (typequal/attribspec-list-list-rename
             (c$::typequal/attribspec-list-list-fix
                  c$::typequal/attribspec-list-list)
             subst)
        (typequal/attribspec-list-list-rename
             c$::typequal/attribspec-list-list
             subst)))

Theorem: typequal/attribspec-list-list-rename-of-ident-ident-alist-fix-subst

(defthm
 typequal/attribspec-list-list-rename-of-ident-ident-alist-fix-subst
 (equal (typequal/attribspec-list-list-rename
             c$::typequal/attribspec-list-list
             (ident-ident-alist-fix subst))
        (typequal/attribspec-list-list-rename
             c$::typequal/attribspec-list-list
             subst)))

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

(defthm initer-rename-of-initer-fix-initer
  (equal (initer-rename (initer-fix c$::initer)
                        subst)
         (initer-rename c$::initer subst)))

Theorem: initer-rename-of-ident-ident-alist-fix-subst

(defthm initer-rename-of-ident-ident-alist-fix-subst
  (equal (initer-rename c$::initer
                        (ident-ident-alist-fix subst))
         (initer-rename c$::initer subst)))

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

(defthm initer-option-rename-of-initer-option-fix-initer-option
  (equal (initer-option-rename (initer-option-fix c$::initer-option)
                               subst)
         (initer-option-rename c$::initer-option subst)))

Theorem: initer-option-rename-of-ident-ident-alist-fix-subst

(defthm initer-option-rename-of-ident-ident-alist-fix-subst
  (equal (initer-option-rename c$::initer-option
                               (ident-ident-alist-fix subst))
         (initer-option-rename c$::initer-option subst)))

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

(defthm desiniter-rename-of-desiniter-fix-desiniter
  (equal (desiniter-rename (desiniter-fix desiniter)
                           subst)
         (desiniter-rename desiniter subst)))

Theorem: desiniter-rename-of-ident-ident-alist-fix-subst

(defthm desiniter-rename-of-ident-ident-alist-fix-subst
  (equal (desiniter-rename desiniter (ident-ident-alist-fix subst))
         (desiniter-rename desiniter subst)))

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

(defthm desiniter-list-rename-of-desiniter-list-fix-desiniter-list
 (equal
      (desiniter-list-rename (desiniter-list-fix c$::desiniter-list)
                             subst)
      (desiniter-list-rename c$::desiniter-list subst)))

Theorem: desiniter-list-rename-of-ident-ident-alist-fix-subst

(defthm desiniter-list-rename-of-ident-ident-alist-fix-subst
  (equal (desiniter-list-rename c$::desiniter-list
                                (ident-ident-alist-fix subst))
         (desiniter-list-rename c$::desiniter-list subst)))

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

(defthm designor-rename-of-designor-fix-designor
  (equal (designor-rename (designor-fix c$::designor)
                          subst)
         (designor-rename c$::designor subst)))

Theorem: designor-rename-of-ident-ident-alist-fix-subst

(defthm designor-rename-of-ident-ident-alist-fix-subst
  (equal (designor-rename c$::designor
                          (ident-ident-alist-fix subst))
         (designor-rename c$::designor subst)))

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

(defthm designor-list-rename-of-designor-list-fix-designor-list
  (equal (designor-list-rename (designor-list-fix c$::designor-list)
                               subst)
         (designor-list-rename c$::designor-list subst)))

Theorem: designor-list-rename-of-ident-ident-alist-fix-subst

(defthm designor-list-rename-of-ident-ident-alist-fix-subst
  (equal (designor-list-rename c$::designor-list
                               (ident-ident-alist-fix subst))
         (designor-list-rename c$::designor-list subst)))

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

(defthm declor-rename-of-declor-fix-declor
  (equal (declor-rename (declor-fix declor)
                        subst)
         (declor-rename declor subst)))

Theorem: declor-rename-of-ident-ident-alist-fix-subst

(defthm declor-rename-of-ident-ident-alist-fix-subst
  (equal (declor-rename declor (ident-ident-alist-fix subst))
         (declor-rename declor subst)))

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

(defthm declor-option-rename-of-declor-option-fix-declor-option
  (equal (declor-option-rename (declor-option-fix c$::declor-option)
                               subst)
         (declor-option-rename c$::declor-option subst)))

Theorem: declor-option-rename-of-ident-ident-alist-fix-subst

(defthm declor-option-rename-of-ident-ident-alist-fix-subst
  (equal (declor-option-rename c$::declor-option
                               (ident-ident-alist-fix subst))
         (declor-option-rename c$::declor-option subst)))

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

(defthm dirdeclor-rename-of-dirdeclor-fix-dirdeclor
  (equal (dirdeclor-rename (dirdeclor-fix dirdeclor)
                           subst)
         (dirdeclor-rename dirdeclor subst)))

Theorem: dirdeclor-rename-of-ident-ident-alist-fix-subst

(defthm dirdeclor-rename-of-ident-ident-alist-fix-subst
  (equal (dirdeclor-rename dirdeclor (ident-ident-alist-fix subst))
         (dirdeclor-rename dirdeclor subst)))

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

(defthm absdeclor-rename-of-absdeclor-fix-absdeclor
  (equal (absdeclor-rename (absdeclor-fix absdeclor)
                           subst)
         (absdeclor-rename absdeclor subst)))

Theorem: absdeclor-rename-of-ident-ident-alist-fix-subst

(defthm absdeclor-rename-of-ident-ident-alist-fix-subst
  (equal (absdeclor-rename absdeclor (ident-ident-alist-fix subst))
         (absdeclor-rename absdeclor subst)))

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

(defthm
   absdeclor-option-rename-of-absdeclor-option-fix-absdeclor-option
  (equal (absdeclor-option-rename
              (absdeclor-option-fix c$::absdeclor-option)
              subst)
         (absdeclor-option-rename c$::absdeclor-option subst)))

Theorem: absdeclor-option-rename-of-ident-ident-alist-fix-subst

(defthm absdeclor-option-rename-of-ident-ident-alist-fix-subst
  (equal (absdeclor-option-rename c$::absdeclor-option
                                  (ident-ident-alist-fix subst))
         (absdeclor-option-rename c$::absdeclor-option subst)))

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

(defthm dirabsdeclor-rename-of-dirabsdeclor-fix-dirabsdeclor
  (equal (dirabsdeclor-rename (dirabsdeclor-fix c$::dirabsdeclor)
                              subst)
         (dirabsdeclor-rename c$::dirabsdeclor subst)))

Theorem: dirabsdeclor-rename-of-ident-ident-alist-fix-subst

(defthm dirabsdeclor-rename-of-ident-ident-alist-fix-subst
  (equal (dirabsdeclor-rename c$::dirabsdeclor
                              (ident-ident-alist-fix subst))
         (dirabsdeclor-rename c$::dirabsdeclor subst)))

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

(defthm
 dirabsdeclor-option-rename-of-dirabsdeclor-option-fix-dirabsdeclor-option
 (equal (dirabsdeclor-option-rename
             (dirabsdeclor-option-fix c$::dirabsdeclor-option)
             subst)
        (dirabsdeclor-option-rename c$::dirabsdeclor-option subst)))

Theorem: dirabsdeclor-option-rename-of-ident-ident-alist-fix-subst

(defthm dirabsdeclor-option-rename-of-ident-ident-alist-fix-subst
 (equal (dirabsdeclor-option-rename c$::dirabsdeclor-option
                                    (ident-ident-alist-fix subst))
        (dirabsdeclor-option-rename c$::dirabsdeclor-option subst)))

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

(defthm param-declon-rename-of-param-declon-fix-param-declon
  (equal (param-declon-rename (param-declon-fix param-declon)
                              subst)
         (param-declon-rename param-declon subst)))

Theorem: param-declon-rename-of-ident-ident-alist-fix-subst

(defthm param-declon-rename-of-ident-ident-alist-fix-subst
  (equal (param-declon-rename param-declon
                              (ident-ident-alist-fix subst))
         (param-declon-rename param-declon subst)))

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

(defthm
 param-declon-list-rename-of-param-declon-list-fix-param-declon-list
 (equal (param-declon-list-rename
             (param-declon-list-fix c$::param-declon-list)
             subst)
        (param-declon-list-rename c$::param-declon-list subst)))

Theorem: param-declon-list-rename-of-ident-ident-alist-fix-subst

(defthm param-declon-list-rename-of-ident-ident-alist-fix-subst
  (equal (param-declon-list-rename c$::param-declon-list
                                   (ident-ident-alist-fix subst))
         (param-declon-list-rename c$::param-declon-list subst)))

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

(defthm param-declor-rename-of-param-declor-fix-param-declor
  (equal (param-declor-rename (param-declor-fix c$::param-declor)
                              subst)
         (param-declor-rename c$::param-declor subst)))

Theorem: param-declor-rename-of-ident-ident-alist-fix-subst

(defthm param-declor-rename-of-ident-ident-alist-fix-subst
  (equal (param-declor-rename c$::param-declor
                              (ident-ident-alist-fix subst))
         (param-declor-rename c$::param-declor subst)))

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

(defthm tyname-rename-of-tyname-fix-tyname
  (equal (tyname-rename (tyname-fix tyname)
                        subst)
         (tyname-rename tyname subst)))

Theorem: tyname-rename-of-ident-ident-alist-fix-subst

(defthm tyname-rename-of-ident-ident-alist-fix-subst
  (equal (tyname-rename tyname (ident-ident-alist-fix subst))
         (tyname-rename tyname subst)))

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

(defthm struni-spec-rename-of-struni-spec-fix-struni-spec
  (equal (struni-spec-rename (struni-spec-fix struni-spec)
                             subst)
         (struni-spec-rename struni-spec subst)))

Theorem: struni-spec-rename-of-ident-ident-alist-fix-subst

(defthm struni-spec-rename-of-ident-ident-alist-fix-subst
  (equal (struni-spec-rename struni-spec
                             (ident-ident-alist-fix subst))
         (struni-spec-rename struni-spec subst)))

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

(defthm struct-declon-rename-of-struct-declon-fix-struct-declon
  (equal (struct-declon-rename (struct-declon-fix c$::struct-declon)
                               subst)
         (struct-declon-rename c$::struct-declon subst)))

Theorem: struct-declon-rename-of-ident-ident-alist-fix-subst

(defthm struct-declon-rename-of-ident-ident-alist-fix-subst
  (equal (struct-declon-rename c$::struct-declon
                               (ident-ident-alist-fix subst))
         (struct-declon-rename c$::struct-declon subst)))

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

(defthm
 struct-declon-list-rename-of-struct-declon-list-fix-struct-declon-list
 (equal (struct-declon-list-rename
             (struct-declon-list-fix c$::struct-declon-list)
             subst)
        (struct-declon-list-rename c$::struct-declon-list subst)))

Theorem: struct-declon-list-rename-of-ident-ident-alist-fix-subst

(defthm struct-declon-list-rename-of-ident-ident-alist-fix-subst
  (equal (struct-declon-list-rename c$::struct-declon-list
                                    (ident-ident-alist-fix subst))
         (struct-declon-list-rename c$::struct-declon-list subst)))

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

(defthm struct-declor-rename-of-struct-declor-fix-struct-declor
  (equal (struct-declor-rename (struct-declor-fix struct-declor)
                               subst)
         (struct-declor-rename struct-declor subst)))

Theorem: struct-declor-rename-of-ident-ident-alist-fix-subst

(defthm struct-declor-rename-of-ident-ident-alist-fix-subst
  (equal (struct-declor-rename struct-declor
                               (ident-ident-alist-fix subst))
         (struct-declor-rename struct-declor subst)))

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

(defthm
 struct-declor-list-rename-of-struct-declor-list-fix-struct-declor-list
 (equal (struct-declor-list-rename
             (struct-declor-list-fix c$::struct-declor-list)
             subst)
        (struct-declor-list-rename c$::struct-declor-list subst)))

Theorem: struct-declor-list-rename-of-ident-ident-alist-fix-subst

(defthm struct-declor-list-rename-of-ident-ident-alist-fix-subst
  (equal (struct-declor-list-rename c$::struct-declor-list
                                    (ident-ident-alist-fix subst))
         (struct-declor-list-rename c$::struct-declor-list subst)))

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

(defthm enum-spec-rename-of-enum-spec-fix-enum-spec
  (equal (enum-spec-rename (enum-spec-fix enum-spec)
                           subst)
         (enum-spec-rename enum-spec subst)))

Theorem: enum-spec-rename-of-ident-ident-alist-fix-subst

(defthm enum-spec-rename-of-ident-ident-alist-fix-subst
  (equal (enum-spec-rename enum-spec (ident-ident-alist-fix subst))
         (enum-spec-rename enum-spec subst)))

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

(defthm enumer-rename-of-enumer-fix-enumer
  (equal (enumer-rename (enumer-fix enumer)
                        subst)
         (enumer-rename enumer subst)))

Theorem: enumer-rename-of-ident-ident-alist-fix-subst

(defthm enumer-rename-of-ident-ident-alist-fix-subst
  (equal (enumer-rename enumer (ident-ident-alist-fix subst))
         (enumer-rename enumer subst)))

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

(defthm enumer-list-rename-of-enumer-list-fix-enumer-list
  (equal (enumer-list-rename (enumer-list-fix c$::enumer-list)
                             subst)
         (enumer-list-rename c$::enumer-list subst)))

Theorem: enumer-list-rename-of-ident-ident-alist-fix-subst

(defthm enumer-list-rename-of-ident-ident-alist-fix-subst
  (equal (enumer-list-rename c$::enumer-list
                             (ident-ident-alist-fix subst))
         (enumer-list-rename c$::enumer-list subst)))

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

(defthm statassert-rename-of-statassert-fix-statassert
  (equal (statassert-rename (statassert-fix statassert)
                            subst)
         (statassert-rename statassert subst)))

Theorem: statassert-rename-of-ident-ident-alist-fix-subst

(defthm statassert-rename-of-ident-ident-alist-fix-subst
  (equal (statassert-rename statassert
                            (ident-ident-alist-fix subst))
         (statassert-rename statassert subst)))

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

(defthm attrib-rename-of-attrib-fix-attrib
  (equal (attrib-rename (c$::attrib-fix c$::attrib)
                        subst)
         (attrib-rename c$::attrib subst)))

Theorem: attrib-rename-of-ident-ident-alist-fix-subst

(defthm attrib-rename-of-ident-ident-alist-fix-subst
  (equal (attrib-rename c$::attrib
                        (ident-ident-alist-fix subst))
         (attrib-rename c$::attrib subst)))

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

(defthm attrib-list-rename-of-attrib-list-fix-attrib-list
  (equal (attrib-list-rename (c$::attrib-list-fix c$::attrib-list)
                             subst)
         (attrib-list-rename c$::attrib-list subst)))

Theorem: attrib-list-rename-of-ident-ident-alist-fix-subst

(defthm attrib-list-rename-of-ident-ident-alist-fix-subst
  (equal (attrib-list-rename c$::attrib-list
                             (ident-ident-alist-fix subst))
         (attrib-list-rename c$::attrib-list subst)))

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

(defthm attrib-spec-rename-of-attrib-spec-fix-attrib-spec
  (equal (attrib-spec-rename (c$::attrib-spec-fix c$::attrib-spec)
                             subst)
         (attrib-spec-rename c$::attrib-spec subst)))

Theorem: attrib-spec-rename-of-ident-ident-alist-fix-subst

(defthm attrib-spec-rename-of-ident-ident-alist-fix-subst
  (equal (attrib-spec-rename c$::attrib-spec
                             (ident-ident-alist-fix subst))
         (attrib-spec-rename c$::attrib-spec subst)))

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

(defthm
   attrib-spec-list-rename-of-attrib-spec-list-fix-attrib-spec-list
  (equal (attrib-spec-list-rename
              (c$::attrib-spec-list-fix c$::attrib-spec-list)
              subst)
         (attrib-spec-list-rename c$::attrib-spec-list subst)))

Theorem: attrib-spec-list-rename-of-ident-ident-alist-fix-subst

(defthm attrib-spec-list-rename-of-ident-ident-alist-fix-subst
  (equal (attrib-spec-list-rename c$::attrib-spec-list
                                  (ident-ident-alist-fix subst))
         (attrib-spec-list-rename c$::attrib-spec-list subst)))

Theorem: init-declor-rename-of-init-declor-fix-init-declor

(defthm init-declor-rename-of-init-declor-fix-init-declor
  (equal (init-declor-rename (init-declor-fix init-declor)
                             subst)
         (init-declor-rename init-declor subst)))

Theorem: init-declor-rename-of-ident-ident-alist-fix-subst

(defthm init-declor-rename-of-ident-ident-alist-fix-subst
  (equal (init-declor-rename init-declor
                             (ident-ident-alist-fix subst))
         (init-declor-rename init-declor subst)))

Theorem: init-declor-list-rename-of-init-declor-list-fix-init-declor-list

(defthm
   init-declor-list-rename-of-init-declor-list-fix-init-declor-list
  (equal (init-declor-list-rename
              (init-declor-list-fix c$::init-declor-list)
              subst)
         (init-declor-list-rename c$::init-declor-list subst)))

Theorem: init-declor-list-rename-of-ident-ident-alist-fix-subst

(defthm init-declor-list-rename-of-ident-ident-alist-fix-subst
  (equal (init-declor-list-rename c$::init-declor-list
                                  (ident-ident-alist-fix subst))
         (init-declor-list-rename c$::init-declor-list subst)))

Theorem: declon-rename-of-declon-fix-declon

(defthm declon-rename-of-declon-fix-declon
  (equal (declon-rename (declon-fix declon)
                        subst)
         (declon-rename declon subst)))

Theorem: declon-rename-of-ident-ident-alist-fix-subst

(defthm declon-rename-of-ident-ident-alist-fix-subst
  (equal (declon-rename declon (ident-ident-alist-fix subst))
         (declon-rename declon subst)))

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

(defthm declon-list-rename-of-declon-list-fix-declon-list
  (equal (declon-list-rename (c$::declon-list-fix c$::declon-list)
                             subst)
         (declon-list-rename c$::declon-list subst)))

Theorem: declon-list-rename-of-ident-ident-alist-fix-subst

(defthm declon-list-rename-of-ident-ident-alist-fix-subst
  (equal (declon-list-rename c$::declon-list
                             (ident-ident-alist-fix subst))
         (declon-list-rename c$::declon-list subst)))

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

(defthm label-rename-of-label-fix-label
  (equal (label-rename (label-fix c$::label)
                       subst)
         (label-rename c$::label subst)))

Theorem: label-rename-of-ident-ident-alist-fix-subst

(defthm label-rename-of-ident-ident-alist-fix-subst
  (equal (label-rename c$::label (ident-ident-alist-fix subst))
         (label-rename c$::label subst)))

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

(defthm asm-output-rename-of-asm-output-fix-asm-output
  (equal (asm-output-rename (c$::asm-output-fix c$::asm-output)
                            subst)
         (asm-output-rename c$::asm-output subst)))

Theorem: asm-output-rename-of-ident-ident-alist-fix-subst

(defthm asm-output-rename-of-ident-ident-alist-fix-subst
  (equal (asm-output-rename c$::asm-output
                            (ident-ident-alist-fix subst))
         (asm-output-rename c$::asm-output subst)))

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

(defthm
      asm-output-list-rename-of-asm-output-list-fix-asm-output-list
  (equal (asm-output-list-rename
              (c$::asm-output-list-fix c$::asm-output-list)
              subst)
         (asm-output-list-rename c$::asm-output-list subst)))

Theorem: asm-output-list-rename-of-ident-ident-alist-fix-subst

(defthm asm-output-list-rename-of-ident-ident-alist-fix-subst
  (equal (asm-output-list-rename c$::asm-output-list
                                 (ident-ident-alist-fix subst))
         (asm-output-list-rename c$::asm-output-list subst)))

Theorem: asm-input-rename-of-asm-input-fix-asm-input

(defthm asm-input-rename-of-asm-input-fix-asm-input
  (equal (asm-input-rename (c$::asm-input-fix c$::asm-input)
                           subst)
         (asm-input-rename c$::asm-input subst)))

Theorem: asm-input-rename-of-ident-ident-alist-fix-subst

(defthm asm-input-rename-of-ident-ident-alist-fix-subst
  (equal (asm-input-rename c$::asm-input
                           (ident-ident-alist-fix subst))
         (asm-input-rename c$::asm-input subst)))

Theorem: asm-input-list-rename-of-asm-input-list-fix-asm-input-list

(defthm asm-input-list-rename-of-asm-input-list-fix-asm-input-list
 (equal
  (asm-input-list-rename (c$::asm-input-list-fix c$::asm-input-list)
                         subst)
  (asm-input-list-rename c$::asm-input-list subst)))

Theorem: asm-input-list-rename-of-ident-ident-alist-fix-subst

(defthm asm-input-list-rename-of-ident-ident-alist-fix-subst
  (equal (asm-input-list-rename c$::asm-input-list
                                (ident-ident-alist-fix subst))
         (asm-input-list-rename c$::asm-input-list subst)))

Theorem: asm-stmt-rename-of-asm-stmt-fix-asm-stmt

(defthm asm-stmt-rename-of-asm-stmt-fix-asm-stmt
  (equal (asm-stmt-rename (c$::asm-stmt-fix c$::asm-stmt)
                          subst)
         (asm-stmt-rename c$::asm-stmt subst)))

Theorem: asm-stmt-rename-of-ident-ident-alist-fix-subst

(defthm asm-stmt-rename-of-ident-ident-alist-fix-subst
  (equal (asm-stmt-rename c$::asm-stmt
                          (ident-ident-alist-fix subst))
         (asm-stmt-rename c$::asm-stmt subst)))

Theorem: stmt-rename-of-stmt-fix-stmt

(defthm stmt-rename-of-stmt-fix-stmt
  (equal (stmt-rename (stmt-fix c$::stmt) subst)
         (stmt-rename c$::stmt subst)))

Theorem: stmt-rename-of-ident-ident-alist-fix-subst

(defthm stmt-rename-of-ident-ident-alist-fix-subst
  (equal (stmt-rename c$::stmt (ident-ident-alist-fix subst))
         (stmt-rename c$::stmt subst)))

Theorem: comp-stmt-rename-of-comp-stmt-fix-comp-stmt

(defthm comp-stmt-rename-of-comp-stmt-fix-comp-stmt
  (equal (comp-stmt-rename (c$::comp-stmt-fix comp-stmt)
                           subst)
         (comp-stmt-rename comp-stmt subst)))

Theorem: comp-stmt-rename-of-ident-ident-alist-fix-subst

(defthm comp-stmt-rename-of-ident-ident-alist-fix-subst
  (equal (comp-stmt-rename comp-stmt (ident-ident-alist-fix subst))
         (comp-stmt-rename comp-stmt subst)))

Theorem: block-item-rename-of-block-item-fix-block-item

(defthm block-item-rename-of-block-item-fix-block-item
  (equal (block-item-rename (block-item-fix c$::block-item)
                            subst)
         (block-item-rename c$::block-item subst)))

Theorem: block-item-rename-of-ident-ident-alist-fix-subst

(defthm block-item-rename-of-ident-ident-alist-fix-subst
  (equal (block-item-rename c$::block-item
                            (ident-ident-alist-fix subst))
         (block-item-rename c$::block-item subst)))

Theorem: block-item-list-rename-of-block-item-list-fix-block-item-list

(defthm
      block-item-list-rename-of-block-item-list-fix-block-item-list
 (equal
   (block-item-list-rename (block-item-list-fix c$::block-item-list)
                           subst)
   (block-item-list-rename c$::block-item-list subst)))

Theorem: block-item-list-rename-of-ident-ident-alist-fix-subst

(defthm block-item-list-rename-of-ident-ident-alist-fix-subst
  (equal (block-item-list-rename c$::block-item-list
                                 (ident-ident-alist-fix subst))
         (block-item-list-rename c$::block-item-list subst)))

Theorem: amb-expr/tyname-rename-of-amb-expr/tyname-fix-amb-expr/tyname

(defthm
      amb-expr/tyname-rename-of-amb-expr/tyname-fix-amb-expr/tyname
  (equal (amb-expr/tyname-rename
              (c$::amb-expr/tyname-fix c$::amb-expr/tyname)
              subst)
         (amb-expr/tyname-rename c$::amb-expr/tyname subst)))

Theorem: amb-expr/tyname-rename-of-ident-ident-alist-fix-subst

(defthm amb-expr/tyname-rename-of-ident-ident-alist-fix-subst
  (equal (amb-expr/tyname-rename c$::amb-expr/tyname
                                 (ident-ident-alist-fix subst))
         (amb-expr/tyname-rename c$::amb-expr/tyname subst)))

Theorem: amb-declor/absdeclor-rename-of-amb-declor/absdeclor-fix-amb-declor/absdeclor

(defthm
 amb-declor/absdeclor-rename-of-amb-declor/absdeclor-fix-amb-declor/absdeclor
 (equal
      (amb-declor/absdeclor-rename
           (c$::amb-declor/absdeclor-fix c$::amb-declor/absdeclor)
           subst)
      (amb-declor/absdeclor-rename c$::amb-declor/absdeclor subst)))

Theorem: amb-declor/absdeclor-rename-of-ident-ident-alist-fix-subst

(defthm amb-declor/absdeclor-rename-of-ident-ident-alist-fix-subst
 (equal
      (amb-declor/absdeclor-rename c$::amb-declor/absdeclor
                                   (ident-ident-alist-fix subst))
      (amb-declor/absdeclor-rename c$::amb-declor/absdeclor subst)))

Theorem: amb-declon/stmt-rename-of-amb-declon/stmt-fix-amb-declon/stmt

(defthm
      amb-declon/stmt-rename-of-amb-declon/stmt-fix-amb-declon/stmt
  (equal (amb-declon/stmt-rename
              (c$::amb-declon/stmt-fix c$::amb-declon/stmt)
              subst)
         (amb-declon/stmt-rename c$::amb-declon/stmt subst)))

Theorem: amb-declon/stmt-rename-of-ident-ident-alist-fix-subst

(defthm amb-declon/stmt-rename-of-ident-ident-alist-fix-subst
  (equal (amb-declon/stmt-rename c$::amb-declon/stmt
                                 (ident-ident-alist-fix subst))
         (amb-declon/stmt-rename c$::amb-declon/stmt subst)))

Theorem: expr-rename-expr-equiv-congruence-on-expr

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

Theorem: expr-rename-ident-ident-alist-equiv-congruence-on-subst

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

Theorem: expr-list-rename-expr-list-equiv-congruence-on-expr-list

(defthm expr-list-rename-expr-list-equiv-congruence-on-expr-list
  (implies (c$::expr-list-equiv c$::expr-list expr-list-equiv)
           (equal (expr-list-rename c$::expr-list subst)
                  (expr-list-rename expr-list-equiv subst)))
  :rule-classes :congruence)

Theorem: expr-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm expr-list-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (expr-list-rename c$::expr-list subst)
                  (expr-list-rename c$::expr-list subst-equiv)))
  :rule-classes :congruence)

Theorem: expr-option-rename-expr-option-equiv-congruence-on-expr-option

(defthm
     expr-option-rename-expr-option-equiv-congruence-on-expr-option
  (implies (c$::expr-option-equiv c$::expr-option expr-option-equiv)
           (equal (expr-option-rename c$::expr-option subst)
                  (expr-option-rename expr-option-equiv subst)))
  :rule-classes :congruence)

Theorem: expr-option-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
     expr-option-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (expr-option-rename c$::expr-option subst)
                  (expr-option-rename c$::expr-option subst-equiv)))
  :rule-classes :congruence)

Theorem: const-expr-rename-const-expr-equiv-congruence-on-const-expr

(defthm const-expr-rename-const-expr-equiv-congruence-on-const-expr
  (implies (c$::const-expr-equiv const-expr const-expr-equiv)
           (equal (const-expr-rename const-expr subst)
                  (const-expr-rename const-expr-equiv subst)))
  :rule-classes :congruence)

Theorem: const-expr-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
      const-expr-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (const-expr-rename const-expr subst)
                  (const-expr-rename const-expr subst-equiv)))
  :rule-classes :congruence)

Theorem: const-expr-option-rename-const-expr-option-equiv-congruence-on-const-expr-option

(defthm
 const-expr-option-rename-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 c$::const-expr-option subst)
          (const-expr-option-rename const-expr-option-equiv subst)))
 :rule-classes :congruence)

Theorem: const-expr-option-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 const-expr-option-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
  (ident-ident-alist-equiv subst subst-equiv)
  (equal
      (const-expr-option-rename c$::const-expr-option subst)
      (const-expr-option-rename c$::const-expr-option subst-equiv)))
 :rule-classes :congruence)

Theorem: genassoc-rename-genassoc-equiv-congruence-on-genassoc

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

Theorem: genassoc-rename-ident-ident-alist-equiv-congruence-on-subst

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

Theorem: genassoc-list-rename-genassoc-list-equiv-congruence-on-genassoc-list

(defthm
 genassoc-list-rename-genassoc-list-equiv-congruence-on-genassoc-list
 (implies
     (c$::genassoc-list-equiv c$::genassoc-list genassoc-list-equiv)
     (equal (genassoc-list-rename c$::genassoc-list subst)
            (genassoc-list-rename genassoc-list-equiv subst)))
 :rule-classes :congruence)

Theorem: genassoc-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
   genassoc-list-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies
       (ident-ident-alist-equiv subst subst-equiv)
       (equal (genassoc-list-rename c$::genassoc-list subst)
              (genassoc-list-rename c$::genassoc-list subst-equiv)))
  :rule-classes :congruence)

Theorem: member-designor-rename-member-designor-equiv-congruence-on-member-designor

(defthm
 member-designor-rename-member-designor-equiv-congruence-on-member-designor
 (implies
      (c$::member-designor-equiv c$::member-designor
                                 member-designor-equiv)
      (equal (member-designor-rename c$::member-designor subst)
             (member-designor-rename member-designor-equiv subst)))
 :rule-classes :congruence)

Theorem: member-designor-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 member-designor-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal (member-designor-rename c$::member-designor subst)
          (member-designor-rename c$::member-designor subst-equiv)))
 :rule-classes :congruence)

Theorem: type-spec-rename-type-spec-equiv-congruence-on-type-spec

(defthm type-spec-rename-type-spec-equiv-congruence-on-type-spec
  (implies (c$::type-spec-equiv c$::type-spec type-spec-equiv)
           (equal (type-spec-rename c$::type-spec subst)
                  (type-spec-rename type-spec-equiv subst)))
  :rule-classes :congruence)

Theorem: type-spec-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm type-spec-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (type-spec-rename c$::type-spec subst)
                  (type-spec-rename c$::type-spec subst-equiv)))
  :rule-classes :congruence)

Theorem: spec/qual-rename-spec/qual-equiv-congruence-on-spec/qual

(defthm spec/qual-rename-spec/qual-equiv-congruence-on-spec/qual
  (implies (c$::spec/qual-equiv c$::spec/qual spec/qual-equiv)
           (equal (spec/qual-rename c$::spec/qual subst)
                  (spec/qual-rename spec/qual-equiv subst)))
  :rule-classes :congruence)

Theorem: spec/qual-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm spec/qual-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (spec/qual-rename c$::spec/qual subst)
                  (spec/qual-rename c$::spec/qual subst-equiv)))
  :rule-classes :congruence)

Theorem: spec/qual-list-rename-spec/qual-list-equiv-congruence-on-spec/qual-list

(defthm
 spec/qual-list-rename-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 c$::spec/qual-list subst)
         (spec/qual-list-rename spec/qual-list-equiv subst)))
 :rule-classes :congruence)

Theorem: spec/qual-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
  spec/qual-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
     (ident-ident-alist-equiv subst subst-equiv)
     (equal (spec/qual-list-rename c$::spec/qual-list subst)
            (spec/qual-list-rename c$::spec/qual-list subst-equiv)))
 :rule-classes :congruence)

Theorem: align-spec-rename-align-spec-equiv-congruence-on-align-spec

(defthm align-spec-rename-align-spec-equiv-congruence-on-align-spec
  (implies (c$::align-spec-equiv c$::align-spec align-spec-equiv)
           (equal (align-spec-rename c$::align-spec subst)
                  (align-spec-rename align-spec-equiv subst)))
  :rule-classes :congruence)

Theorem: align-spec-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
      align-spec-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (align-spec-rename c$::align-spec subst)
                  (align-spec-rename c$::align-spec subst-equiv)))
  :rule-classes :congruence)

Theorem: decl-spec-rename-decl-spec-equiv-congruence-on-decl-spec

(defthm decl-spec-rename-decl-spec-equiv-congruence-on-decl-spec
  (implies (c$::decl-spec-equiv c$::decl-spec decl-spec-equiv)
           (equal (decl-spec-rename c$::decl-spec subst)
                  (decl-spec-rename decl-spec-equiv subst)))
  :rule-classes :congruence)

Theorem: decl-spec-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm decl-spec-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (decl-spec-rename c$::decl-spec subst)
                  (decl-spec-rename c$::decl-spec subst-equiv)))
  :rule-classes :congruence)

Theorem: decl-spec-list-rename-decl-spec-list-equiv-congruence-on-decl-spec-list

(defthm
 decl-spec-list-rename-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 c$::decl-spec-list subst)
         (decl-spec-list-rename decl-spec-list-equiv subst)))
 :rule-classes :congruence)

Theorem: decl-spec-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
  decl-spec-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
     (ident-ident-alist-equiv subst subst-equiv)
     (equal (decl-spec-list-rename c$::decl-spec-list subst)
            (decl-spec-list-rename c$::decl-spec-list subst-equiv)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-rename-typequal/attribspec-equiv-congruence-on-typequal/attribspec

(defthm
 typequal/attribspec-rename-typequal/attribspec-equiv-congruence-on-typequal/attribspec
 (implies
  (c$::typequal/attribspec-equiv c$::typequal/attribspec
                                 typequal/attribspec-equiv)
  (equal
      (typequal/attribspec-rename c$::typequal/attribspec subst)
      (typequal/attribspec-rename typequal/attribspec-equiv subst)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 typequal/attribspec-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal (typequal/attribspec-rename c$::typequal/attribspec subst)
          (typequal/attribspec-rename
               c$::typequal/attribspec subst-equiv)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-rename-typequal/attribspec-list-equiv-congruence-on-typequal/attribspec-list

(defthm
 typequal/attribspec-list-rename-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
                      c$::typequal/attribspec-list subst)
                 (typequal/attribspec-list-rename
                      typequal/attribspec-list-equiv subst)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 typequal/attribspec-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
  (ident-ident-alist-equiv subst subst-equiv)
  (equal
       (typequal/attribspec-list-rename
            c$::typequal/attribspec-list subst)
       (typequal/attribspec-list-rename c$::typequal/attribspec-list
                                        subst-equiv)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-list-rename-typequal/attribspec-list-list-equiv-congruence-on-typequal/attribspec-list-list

(defthm
 typequal/attribspec-list-list-rename-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
                      c$::typequal/attribspec-list-list subst)
                 (typequal/attribspec-list-list-rename
                      typequal/attribspec-list-list-equiv
                      subst)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 typequal/attribspec-list-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies (ident-ident-alist-equiv subst subst-equiv)
          (equal (typequal/attribspec-list-list-rename
                      c$::typequal/attribspec-list-list subst)
                 (typequal/attribspec-list-list-rename
                      c$::typequal/attribspec-list-list
                      subst-equiv)))
 :rule-classes :congruence)

Theorem: initer-rename-initer-equiv-congruence-on-initer

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

Theorem: initer-rename-ident-ident-alist-equiv-congruence-on-subst

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

Theorem: initer-option-rename-initer-option-equiv-congruence-on-initer-option

(defthm
 initer-option-rename-initer-option-equiv-congruence-on-initer-option
 (implies
     (c$::initer-option-equiv c$::initer-option initer-option-equiv)
     (equal (initer-option-rename c$::initer-option subst)
            (initer-option-rename initer-option-equiv subst)))
 :rule-classes :congruence)

Theorem: initer-option-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
   initer-option-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies
       (ident-ident-alist-equiv subst subst-equiv)
       (equal (initer-option-rename c$::initer-option subst)
              (initer-option-rename c$::initer-option subst-equiv)))
  :rule-classes :congruence)

Theorem: desiniter-rename-desiniter-equiv-congruence-on-desiniter

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

Theorem: desiniter-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm desiniter-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (desiniter-rename desiniter subst)
                  (desiniter-rename desiniter subst-equiv)))
  :rule-classes :congruence)

Theorem: desiniter-list-rename-desiniter-list-equiv-congruence-on-desiniter-list

(defthm
 desiniter-list-rename-desiniter-list-equiv-congruence-on-desiniter-list
 (implies
  (c$::desiniter-list-equiv c$::desiniter-list desiniter-list-equiv)
  (equal (desiniter-list-rename c$::desiniter-list subst)
         (desiniter-list-rename desiniter-list-equiv subst)))
 :rule-classes :congruence)

Theorem: desiniter-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
  desiniter-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
     (ident-ident-alist-equiv subst subst-equiv)
     (equal (desiniter-list-rename c$::desiniter-list subst)
            (desiniter-list-rename c$::desiniter-list subst-equiv)))
 :rule-classes :congruence)

Theorem: designor-rename-designor-equiv-congruence-on-designor

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

Theorem: designor-rename-ident-ident-alist-equiv-congruence-on-subst

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

Theorem: designor-list-rename-designor-list-equiv-congruence-on-designor-list

(defthm
 designor-list-rename-designor-list-equiv-congruence-on-designor-list
 (implies
     (c$::designor-list-equiv c$::designor-list designor-list-equiv)
     (equal (designor-list-rename c$::designor-list subst)
            (designor-list-rename designor-list-equiv subst)))
 :rule-classes :congruence)

Theorem: designor-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
   designor-list-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies
       (ident-ident-alist-equiv subst subst-equiv)
       (equal (designor-list-rename c$::designor-list subst)
              (designor-list-rename c$::designor-list subst-equiv)))
  :rule-classes :congruence)

Theorem: declor-rename-declor-equiv-congruence-on-declor

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

Theorem: declor-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm declor-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (declor-rename declor subst)
                  (declor-rename declor subst-equiv)))
  :rule-classes :congruence)

Theorem: declor-option-rename-declor-option-equiv-congruence-on-declor-option

(defthm
 declor-option-rename-declor-option-equiv-congruence-on-declor-option
 (implies
     (c$::declor-option-equiv c$::declor-option declor-option-equiv)
     (equal (declor-option-rename c$::declor-option subst)
            (declor-option-rename declor-option-equiv subst)))
 :rule-classes :congruence)

Theorem: declor-option-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
   declor-option-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies
       (ident-ident-alist-equiv subst subst-equiv)
       (equal (declor-option-rename c$::declor-option subst)
              (declor-option-rename c$::declor-option subst-equiv)))
  :rule-classes :congruence)

Theorem: dirdeclor-rename-dirdeclor-equiv-congruence-on-dirdeclor

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

Theorem: dirdeclor-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm dirdeclor-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (dirdeclor-rename dirdeclor subst)
                  (dirdeclor-rename dirdeclor subst-equiv)))
  :rule-classes :congruence)

Theorem: absdeclor-rename-absdeclor-equiv-congruence-on-absdeclor

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

Theorem: absdeclor-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm absdeclor-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (absdeclor-rename absdeclor subst)
                  (absdeclor-rename absdeclor subst-equiv)))
  :rule-classes :congruence)

Theorem: absdeclor-option-rename-absdeclor-option-equiv-congruence-on-absdeclor-option

(defthm
 absdeclor-option-rename-absdeclor-option-equiv-congruence-on-absdeclor-option
 (implies
     (c$::absdeclor-option-equiv c$::absdeclor-option
                                 absdeclor-option-equiv)
     (equal (absdeclor-option-rename c$::absdeclor-option subst)
            (absdeclor-option-rename absdeclor-option-equiv subst)))
 :rule-classes :congruence)

Theorem: absdeclor-option-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 absdeclor-option-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal
        (absdeclor-option-rename c$::absdeclor-option subst)
        (absdeclor-option-rename c$::absdeclor-option subst-equiv)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-rename-dirabsdeclor-equiv-congruence-on-dirabsdeclor

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

Theorem: dirabsdeclor-rename-ident-ident-alist-equiv-congruence-on-subst

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

Theorem: dirabsdeclor-option-rename-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor-option

(defthm
 dirabsdeclor-option-rename-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor-option
 (implies
  (c$::dirabsdeclor-option-equiv c$::dirabsdeclor-option
                                 dirabsdeclor-option-equiv)
  (equal
      (dirabsdeclor-option-rename c$::dirabsdeclor-option subst)
      (dirabsdeclor-option-rename dirabsdeclor-option-equiv subst)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-option-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 dirabsdeclor-option-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal (dirabsdeclor-option-rename c$::dirabsdeclor-option subst)
          (dirabsdeclor-option-rename
               c$::dirabsdeclor-option subst-equiv)))
 :rule-classes :congruence)

Theorem: param-declon-rename-param-declon-equiv-congruence-on-param-declon

(defthm
  param-declon-rename-param-declon-equiv-congruence-on-param-declon
  (implies (c$::param-declon-equiv param-declon param-declon-equiv)
           (equal (param-declon-rename param-declon subst)
                  (param-declon-rename param-declon-equiv subst)))
  :rule-classes :congruence)

Theorem: param-declon-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
    param-declon-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (param-declon-rename param-declon subst)
                  (param-declon-rename param-declon subst-equiv)))
  :rule-classes :congruence)

Theorem: param-declon-list-rename-param-declon-list-equiv-congruence-on-param-declon-list

(defthm
 param-declon-list-rename-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 c$::param-declon-list subst)
          (param-declon-list-rename param-declon-list-equiv subst)))
 :rule-classes :congruence)

Theorem: param-declon-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 param-declon-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
  (ident-ident-alist-equiv subst subst-equiv)
  (equal
      (param-declon-list-rename c$::param-declon-list subst)
      (param-declon-list-rename c$::param-declon-list subst-equiv)))
 :rule-classes :congruence)

Theorem: param-declor-rename-param-declor-equiv-congruence-on-param-declor

(defthm
  param-declor-rename-param-declor-equiv-congruence-on-param-declor
  (implies
       (c$::param-declor-equiv c$::param-declor param-declor-equiv)
       (equal (param-declor-rename c$::param-declor subst)
              (param-declor-rename param-declor-equiv subst)))
  :rule-classes :congruence)

Theorem: param-declor-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
    param-declor-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies
       (ident-ident-alist-equiv subst subst-equiv)
       (equal (param-declor-rename c$::param-declor subst)
              (param-declor-rename c$::param-declor subst-equiv)))
  :rule-classes :congruence)

Theorem: tyname-rename-tyname-equiv-congruence-on-tyname

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

Theorem: tyname-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm tyname-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (tyname-rename tyname subst)
                  (tyname-rename tyname subst-equiv)))
  :rule-classes :congruence)

Theorem: struni-spec-rename-struni-spec-equiv-congruence-on-struni-spec

(defthm
     struni-spec-rename-struni-spec-equiv-congruence-on-struni-spec
  (implies (c$::struni-spec-equiv struni-spec struni-spec-equiv)
           (equal (struni-spec-rename struni-spec subst)
                  (struni-spec-rename struni-spec-equiv subst)))
  :rule-classes :congruence)

Theorem: struni-spec-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
     struni-spec-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (struni-spec-rename struni-spec subst)
                  (struni-spec-rename struni-spec subst-equiv)))
  :rule-classes :congruence)

Theorem: struct-declon-rename-struct-declon-equiv-congruence-on-struct-declon

(defthm
 struct-declon-rename-struct-declon-equiv-congruence-on-struct-declon
 (implies
     (c$::struct-declon-equiv c$::struct-declon struct-declon-equiv)
     (equal (struct-declon-rename c$::struct-declon subst)
            (struct-declon-rename struct-declon-equiv subst)))
 :rule-classes :congruence)

Theorem: struct-declon-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
   struct-declon-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies
       (ident-ident-alist-equiv subst subst-equiv)
       (equal (struct-declon-rename c$::struct-declon subst)
              (struct-declon-rename c$::struct-declon subst-equiv)))
  :rule-classes :congruence)

Theorem: struct-declon-list-rename-struct-declon-list-equiv-congruence-on-struct-declon-list

(defthm
 struct-declon-list-rename-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 c$::struct-declon-list subst)
        (struct-declon-list-rename struct-declon-list-equiv subst)))
 :rule-classes :congruence)

Theorem: struct-declon-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 struct-declon-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
  (ident-ident-alist-equiv subst subst-equiv)
  (equal
    (struct-declon-list-rename c$::struct-declon-list subst)
    (struct-declon-list-rename c$::struct-declon-list subst-equiv)))
 :rule-classes :congruence)

Theorem: struct-declor-rename-struct-declor-equiv-congruence-on-struct-declor

(defthm
 struct-declor-rename-struct-declor-equiv-congruence-on-struct-declor
 (implies
      (c$::struct-declor-equiv struct-declor struct-declor-equiv)
      (equal (struct-declor-rename struct-declor subst)
             (struct-declor-rename struct-declor-equiv subst)))
 :rule-classes :congruence)

Theorem: struct-declor-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
   struct-declor-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (struct-declor-rename struct-declor subst)
                  (struct-declor-rename struct-declor subst-equiv)))
  :rule-classes :congruence)

Theorem: struct-declor-list-rename-struct-declor-list-equiv-congruence-on-struct-declor-list

(defthm
 struct-declor-list-rename-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 c$::struct-declor-list subst)
        (struct-declor-list-rename struct-declor-list-equiv subst)))
 :rule-classes :congruence)

Theorem: struct-declor-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 struct-declor-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
  (ident-ident-alist-equiv subst subst-equiv)
  (equal
    (struct-declor-list-rename c$::struct-declor-list subst)
    (struct-declor-list-rename c$::struct-declor-list subst-equiv)))
 :rule-classes :congruence)

Theorem: enum-spec-rename-enum-spec-equiv-congruence-on-enum-spec

(defthm enum-spec-rename-enum-spec-equiv-congruence-on-enum-spec
  (implies (c$::enum-spec-equiv enum-spec enum-spec-equiv)
           (equal (enum-spec-rename enum-spec subst)
                  (enum-spec-rename enum-spec-equiv subst)))
  :rule-classes :congruence)

Theorem: enum-spec-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm enum-spec-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (enum-spec-rename enum-spec subst)
                  (enum-spec-rename enum-spec subst-equiv)))
  :rule-classes :congruence)

Theorem: enumer-rename-enumer-equiv-congruence-on-enumer

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

Theorem: enumer-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm enumer-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (enumer-rename enumer subst)
                  (enumer-rename enumer subst-equiv)))
  :rule-classes :congruence)

Theorem: enumer-list-rename-enumer-list-equiv-congruence-on-enumer-list

(defthm
     enumer-list-rename-enumer-list-equiv-congruence-on-enumer-list
  (implies (c$::enumer-list-equiv c$::enumer-list enumer-list-equiv)
           (equal (enumer-list-rename c$::enumer-list subst)
                  (enumer-list-rename enumer-list-equiv subst)))
  :rule-classes :congruence)

Theorem: enumer-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
     enumer-list-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (enumer-list-rename c$::enumer-list subst)
                  (enumer-list-rename c$::enumer-list subst-equiv)))
  :rule-classes :congruence)

Theorem: statassert-rename-statassert-equiv-congruence-on-statassert

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

Theorem: statassert-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
      statassert-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (statassert-rename statassert subst)
                  (statassert-rename statassert subst-equiv)))
  :rule-classes :congruence)

Theorem: attrib-rename-attrib-equiv-congruence-on-attrib

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

Theorem: attrib-rename-ident-ident-alist-equiv-congruence-on-subst

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

Theorem: attrib-list-rename-attrib-list-equiv-congruence-on-attrib-list

(defthm
     attrib-list-rename-attrib-list-equiv-congruence-on-attrib-list
  (implies (c$::attrib-list-equiv c$::attrib-list attrib-list-equiv)
           (equal (attrib-list-rename c$::attrib-list subst)
                  (attrib-list-rename attrib-list-equiv subst)))
  :rule-classes :congruence)

Theorem: attrib-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
     attrib-list-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (attrib-list-rename c$::attrib-list subst)
                  (attrib-list-rename c$::attrib-list subst-equiv)))
  :rule-classes :congruence)

Theorem: attrib-spec-rename-attrib-spec-equiv-congruence-on-attrib-spec

(defthm
     attrib-spec-rename-attrib-spec-equiv-congruence-on-attrib-spec
  (implies (c$::attrib-spec-equiv c$::attrib-spec attrib-spec-equiv)
           (equal (attrib-spec-rename c$::attrib-spec subst)
                  (attrib-spec-rename attrib-spec-equiv subst)))
  :rule-classes :congruence)

Theorem: attrib-spec-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
     attrib-spec-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (attrib-spec-rename c$::attrib-spec subst)
                  (attrib-spec-rename c$::attrib-spec subst-equiv)))
  :rule-classes :congruence)

Theorem: attrib-spec-list-rename-attrib-spec-list-equiv-congruence-on-attrib-spec-list

(defthm
 attrib-spec-list-rename-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 c$::attrib-spec-list subst)
            (attrib-spec-list-rename attrib-spec-list-equiv subst)))
 :rule-classes :congruence)

Theorem: attrib-spec-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 attrib-spec-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal
        (attrib-spec-list-rename c$::attrib-spec-list subst)
        (attrib-spec-list-rename c$::attrib-spec-list subst-equiv)))
 :rule-classes :congruence)

Theorem: init-declor-rename-init-declor-equiv-congruence-on-init-declor

(defthm
     init-declor-rename-init-declor-equiv-congruence-on-init-declor
  (implies (c$::init-declor-equiv init-declor init-declor-equiv)
           (equal (init-declor-rename init-declor subst)
                  (init-declor-rename init-declor-equiv subst)))
  :rule-classes :congruence)

Theorem: init-declor-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
     init-declor-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (init-declor-rename init-declor subst)
                  (init-declor-rename init-declor subst-equiv)))
  :rule-classes :congruence)

Theorem: init-declor-list-rename-init-declor-list-equiv-congruence-on-init-declor-list

(defthm
 init-declor-list-rename-init-declor-list-equiv-congruence-on-init-declor-list
 (implies
     (c$::init-declor-list-equiv c$::init-declor-list
                                 init-declor-list-equiv)
     (equal (init-declor-list-rename c$::init-declor-list subst)
            (init-declor-list-rename init-declor-list-equiv subst)))
 :rule-classes :congruence)

Theorem: init-declor-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 init-declor-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal
        (init-declor-list-rename c$::init-declor-list subst)
        (init-declor-list-rename c$::init-declor-list subst-equiv)))
 :rule-classes :congruence)

Theorem: declon-rename-declon-equiv-congruence-on-declon

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

Theorem: declon-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm declon-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (declon-rename declon subst)
                  (declon-rename declon subst-equiv)))
  :rule-classes :congruence)

Theorem: declon-list-rename-declon-list-equiv-congruence-on-declon-list

(defthm
     declon-list-rename-declon-list-equiv-congruence-on-declon-list
  (implies (c$::declon-list-equiv c$::declon-list declon-list-equiv)
           (equal (declon-list-rename c$::declon-list subst)
                  (declon-list-rename declon-list-equiv subst)))
  :rule-classes :congruence)

Theorem: declon-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
     declon-list-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (declon-list-rename c$::declon-list subst)
                  (declon-list-rename c$::declon-list subst-equiv)))
  :rule-classes :congruence)

Theorem: label-rename-label-equiv-congruence-on-label

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

Theorem: label-rename-ident-ident-alist-equiv-congruence-on-subst

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

Theorem: asm-output-rename-asm-output-equiv-congruence-on-asm-output

(defthm asm-output-rename-asm-output-equiv-congruence-on-asm-output
  (implies (c$::asm-output-equiv c$::asm-output asm-output-equiv)
           (equal (asm-output-rename c$::asm-output subst)
                  (asm-output-rename asm-output-equiv subst)))
  :rule-classes :congruence)

Theorem: asm-output-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
      asm-output-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (asm-output-rename c$::asm-output subst)
                  (asm-output-rename c$::asm-output subst-equiv)))
  :rule-classes :congruence)

Theorem: asm-output-list-rename-asm-output-list-equiv-congruence-on-asm-output-list

(defthm
 asm-output-list-rename-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 c$::asm-output-list subst)
             (asm-output-list-rename asm-output-list-equiv subst)))
 :rule-classes :congruence)

Theorem: asm-output-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 asm-output-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal (asm-output-list-rename c$::asm-output-list subst)
          (asm-output-list-rename c$::asm-output-list subst-equiv)))
 :rule-classes :congruence)

Theorem: asm-input-rename-asm-input-equiv-congruence-on-asm-input

(defthm asm-input-rename-asm-input-equiv-congruence-on-asm-input
  (implies (c$::asm-input-equiv c$::asm-input asm-input-equiv)
           (equal (asm-input-rename c$::asm-input subst)
                  (asm-input-rename asm-input-equiv subst)))
  :rule-classes :congruence)

Theorem: asm-input-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm asm-input-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (asm-input-rename c$::asm-input subst)
                  (asm-input-rename c$::asm-input subst-equiv)))
  :rule-classes :congruence)

Theorem: asm-input-list-rename-asm-input-list-equiv-congruence-on-asm-input-list

(defthm
 asm-input-list-rename-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 c$::asm-input-list subst)
         (asm-input-list-rename asm-input-list-equiv subst)))
 :rule-classes :congruence)

Theorem: asm-input-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
  asm-input-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
     (ident-ident-alist-equiv subst subst-equiv)
     (equal (asm-input-list-rename c$::asm-input-list subst)
            (asm-input-list-rename c$::asm-input-list subst-equiv)))
 :rule-classes :congruence)

Theorem: asm-stmt-rename-asm-stmt-equiv-congruence-on-asm-stmt

(defthm asm-stmt-rename-asm-stmt-equiv-congruence-on-asm-stmt
  (implies (c$::asm-stmt-equiv c$::asm-stmt asm-stmt-equiv)
           (equal (asm-stmt-rename c$::asm-stmt subst)
                  (asm-stmt-rename asm-stmt-equiv subst)))
  :rule-classes :congruence)

Theorem: asm-stmt-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm asm-stmt-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (asm-stmt-rename c$::asm-stmt subst)
                  (asm-stmt-rename c$::asm-stmt subst-equiv)))
  :rule-classes :congruence)

Theorem: stmt-rename-stmt-equiv-congruence-on-stmt

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

Theorem: stmt-rename-ident-ident-alist-equiv-congruence-on-subst

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

Theorem: comp-stmt-rename-comp-stmt-equiv-congruence-on-comp-stmt

(defthm comp-stmt-rename-comp-stmt-equiv-congruence-on-comp-stmt
  (implies (c$::comp-stmt-equiv comp-stmt comp-stmt-equiv)
           (equal (comp-stmt-rename comp-stmt subst)
                  (comp-stmt-rename comp-stmt-equiv subst)))
  :rule-classes :congruence)

Theorem: comp-stmt-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm comp-stmt-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (comp-stmt-rename comp-stmt subst)
                  (comp-stmt-rename comp-stmt subst-equiv)))
  :rule-classes :congruence)

Theorem: block-item-rename-block-item-equiv-congruence-on-block-item

(defthm block-item-rename-block-item-equiv-congruence-on-block-item
  (implies (c$::block-item-equiv c$::block-item block-item-equiv)
           (equal (block-item-rename c$::block-item subst)
                  (block-item-rename block-item-equiv subst)))
  :rule-classes :congruence)

Theorem: block-item-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
      block-item-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (block-item-rename c$::block-item subst)
                  (block-item-rename c$::block-item subst-equiv)))
  :rule-classes :congruence)

Theorem: block-item-list-rename-block-item-list-equiv-congruence-on-block-item-list

(defthm
 block-item-list-rename-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 c$::block-item-list subst)
             (block-item-list-rename block-item-list-equiv subst)))
 :rule-classes :congruence)

Theorem: block-item-list-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 block-item-list-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal (block-item-list-rename c$::block-item-list subst)
          (block-item-list-rename c$::block-item-list subst-equiv)))
 :rule-classes :congruence)

Theorem: amb-expr/tyname-rename-amb-expr/tyname-equiv-congruence-on-amb-expr/tyname

(defthm
 amb-expr/tyname-rename-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 c$::amb-expr/tyname subst)
             (amb-expr/tyname-rename amb-expr/tyname-equiv subst)))
 :rule-classes :congruence)

Theorem: amb-expr/tyname-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 amb-expr/tyname-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal (amb-expr/tyname-rename c$::amb-expr/tyname subst)
          (amb-expr/tyname-rename c$::amb-expr/tyname subst-equiv)))
 :rule-classes :congruence)

Theorem: amb-declor/absdeclor-rename-amb-declor/absdeclor-equiv-congruence-on-amb-declor/absdeclor

(defthm
 amb-declor/absdeclor-rename-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 c$::amb-declor/absdeclor subst)
    (amb-declor/absdeclor-rename amb-declor/absdeclor-equiv subst)))
 :rule-classes :congruence)

Theorem: amb-declor/absdeclor-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 amb-declor/absdeclor-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal
        (amb-declor/absdeclor-rename c$::amb-declor/absdeclor subst)
        (amb-declor/absdeclor-rename
             c$::amb-declor/absdeclor subst-equiv)))
 :rule-classes :congruence)

Theorem: amb-declon/stmt-rename-amb-declon/stmt-equiv-congruence-on-amb-declon/stmt

(defthm
 amb-declon/stmt-rename-amb-declon/stmt-equiv-congruence-on-amb-declon/stmt
 (implies
      (c$::amb-declon/stmt-equiv c$::amb-declon/stmt
                                 amb-declon/stmt-equiv)
      (equal (amb-declon/stmt-rename c$::amb-declon/stmt subst)
             (amb-declon/stmt-rename amb-declon/stmt-equiv subst)))
 :rule-classes :congruence)

Theorem: amb-declon/stmt-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
 amb-declon/stmt-rename-ident-ident-alist-equiv-congruence-on-subst
 (implies
   (ident-ident-alist-equiv subst subst-equiv)
   (equal (amb-declon/stmt-rename c$::amb-declon/stmt subst)
          (amb-declon/stmt-rename c$::amb-declon/stmt subst-equiv)))
 :rule-classes :congruence)