		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-collect-idents

Exprs/decls/stmts-collect-idents

Definitions and Theorems

Function: expr-collect-idents

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

Function: expr-list-collect-idents

(defun expr-list-collect-idents (c$::expr-list)
 (declare (xargs :guard (expr-listp c$::expr-list)))
 (let ((__function__ 'expr-list-collect-idents))
  (declare (ignorable __function__))
  (cond
       ((endp c$::expr-list) nil)
       (t (union (expr-collect-idents (car c$::expr-list))
                 (expr-list-collect-idents (cdr c$::expr-list)))))))

Function: expr-option-collect-idents

(defun expr-option-collect-idents (c$::expr-option)
 (declare (xargs :guard (expr-optionp c$::expr-option)))
 (let ((__function__ 'expr-option-collect-idents))
  (declare (ignorable __function__))
  (expr-option-case
   c$::expr-option
   :some
   (expr-collect-idents (c$::expr-option-some->val c$::expr-option))
   :none nil)))

Function: const-expr-collect-idents

(defun const-expr-collect-idents (const-expr)
  (declare (xargs :guard (const-exprp const-expr)))
  (declare (ignorable const-expr))
  (let ((__function__ 'const-expr-collect-idents))
    (declare (ignorable __function__))
    (expr-collect-idents (const-expr->expr const-expr))))

Function: const-expr-option-collect-idents

(defun const-expr-option-collect-idents (c$::const-expr-option)
 (declare (xargs :guard (const-expr-optionp c$::const-expr-option)))
 (let ((__function__ 'const-expr-option-collect-idents))
  (declare (ignorable __function__))
  (const-expr-option-case
       c$::const-expr-option
       :some
       (const-expr-collect-idents
            (c$::const-expr-option-some->val c$::const-expr-option))
       :none nil)))

Function: genassoc-collect-idents

(defun genassoc-collect-idents (c$::genassoc)
 (declare (xargs :guard (genassocp c$::genassoc)))
 (declare (ignorable c$::genassoc))
 (let ((__function__ 'genassoc-collect-idents))
  (declare (ignorable __function__))
  (genassoc-case
   c$::genassoc
   :type
   (union
      (tyname-collect-idents (c$::genassoc-type->type c$::genassoc))
      (expr-collect-idents (c$::genassoc-type->expr c$::genassoc)))
   :default (expr-collect-idents
                 (c$::genassoc-default->expr c$::genassoc)))))

Function: genassoc-list-collect-idents

(defun genassoc-list-collect-idents (c$::genassoc-list)
 (declare (xargs :guard (genassoc-listp c$::genassoc-list)))
 (let ((__function__ 'genassoc-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::genassoc-list) nil)
   (t
    (union
         (genassoc-collect-idents (car c$::genassoc-list))
         (genassoc-list-collect-idents (cdr c$::genassoc-list)))))))

Function: member-designor-collect-idents

(defun member-designor-collect-idents (c$::member-designor)
 (declare (xargs :guard (member-designorp c$::member-designor)))
 (declare (ignorable c$::member-designor))
 (let ((__function__ 'member-designor-collect-idents))
  (declare (ignorable __function__))
  (member-designor-case
   c$::member-designor
   :ident
   (ident-collect-idents
        (c$::member-designor-ident->ident c$::member-designor))
   :dot
   (union
        (member-designor-collect-idents
             (c$::member-designor-dot->member c$::member-designor))
        (ident-collect-idents
             (c$::member-designor-dot->name c$::member-designor)))
   :sub
   (union
      (member-designor-collect-idents
           (c$::member-designor-sub->member c$::member-designor))
      (expr-collect-idents
           (c$::member-designor-sub->index c$::member-designor))))))

Function: type-spec-collect-idents

(defun type-spec-collect-idents (c$::type-spec)
 (declare (xargs :guard (type-specp c$::type-spec)))
 (declare (ignorable c$::type-spec))
 (let ((__function__ 'type-spec-collect-idents))
  (declare (ignorable __function__))
  (type-spec-case
    c$::type-spec
    :void nil
    :char nil
    :short nil
    :int nil
    :long nil
    :float nil
    :double nil
    :signed nil
    :unsigned nil
    :bool nil
    :complex nil
    :atomic (tyname-collect-idents
                 (c$::type-spec-atomic->type c$::type-spec))
    :struct (struni-spec-collect-idents
                 (c$::type-spec-struct->spec c$::type-spec))
    :union (struni-spec-collect-idents
                (c$::type-spec-union->spec c$::type-spec))
    :enum (enum-spec-collect-idents
               (c$::type-spec-enum->spec c$::type-spec))
    :typedef (ident-collect-idents
                  (c$::type-spec-typedef->name c$::type-spec))
    :int128 nil
    :locase-float80 nil
    :locase-float128 nil
    :float16 nil
    :float16x nil
    :float32 nil
    :float32x nil
    :float64 nil
    :float64x nil
    :float128 nil
    :float128x nil
    :builtin-va-list nil
    :struct-empty
    (union (attrib-spec-list-collect-idents
                (c$::type-spec-struct-empty->attribs c$::type-spec))
           (ident-option-collect-idents
                (c$::type-spec-struct-empty->name? c$::type-spec)))
    :typeof-expr
    (expr-collect-idents
         (c$::type-spec-typeof-expr->expr c$::type-spec))
    :typeof-type
    (tyname-collect-idents
         (c$::type-spec-typeof-type->type c$::type-spec))
    :typeof-ambig
    (amb-expr/tyname-collect-idents
         (c$::type-spec-typeof-ambig->expr/type c$::type-spec))
    :auto-type nil)))

Function: spec/qual-collect-idents

(defun spec/qual-collect-idents (c$::spec/qual)
 (declare (xargs :guard (spec/qual-p c$::spec/qual)))
 (declare (ignorable c$::spec/qual))
 (let ((__function__ 'spec/qual-collect-idents))
   (declare (ignorable __function__))
   (spec/qual-case
        c$::spec/qual
        :typespec (type-spec-collect-idents
                       (c$::spec/qual-typespec->spec c$::spec/qual))
        :typequal nil
        :align (align-spec-collect-idents
                    (c$::spec/qual-align->spec c$::spec/qual))
        :attrib (attrib-spec-collect-idents
                     (c$::spec/qual-attrib->spec c$::spec/qual)))))

Function: spec/qual-list-collect-idents

(defun spec/qual-list-collect-idents (c$::spec/qual-list)
 (declare (xargs :guard (spec/qual-listp c$::spec/qual-list)))
 (let ((__function__ 'spec/qual-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::spec/qual-list) nil)
   (t
    (union
       (spec/qual-collect-idents (car c$::spec/qual-list))
       (spec/qual-list-collect-idents (cdr c$::spec/qual-list)))))))

Function: align-spec-collect-idents

(defun align-spec-collect-idents (c$::align-spec)
 (declare (xargs :guard (align-specp c$::align-spec)))
 (declare (ignorable c$::align-spec))
 (let ((__function__ 'align-spec-collect-idents))
  (declare (ignorable __function__))
  (align-spec-case
   c$::align-spec
   :alignas-type
   (tyname-collect-idents
        (c$::align-spec-alignas-type->type c$::align-spec))
   :alignas-expr
   (const-expr-collect-idents
        (c$::align-spec-alignas-expr->expr c$::align-spec))
   :alignas-ambig
   (amb-expr/tyname-collect-idents
        (c$::align-spec-alignas-ambig->expr/type c$::align-spec)))))

Function: decl-spec-collect-idents

(defun decl-spec-collect-idents (c$::decl-spec)
 (declare (xargs :guard (decl-specp c$::decl-spec)))
 (declare (ignorable c$::decl-spec))
 (let ((__function__ 'decl-spec-collect-idents))
  (declare (ignorable __function__))
  (decl-spec-case
      c$::decl-spec
      :stoclass nil
      :typespec (type-spec-collect-idents
                     (c$::decl-spec-typespec->spec c$::decl-spec))
      :typequal nil
      :function nil
      :align (align-spec-collect-idents
                  (c$::decl-spec-align->spec c$::decl-spec))
      :attrib (attrib-spec-collect-idents
                   (c$::decl-spec-attrib->spec c$::decl-spec))
      :stdcall nil
      :declspec (ident-collect-idents
                     (c$::decl-spec-declspec->arg c$::decl-spec)))))

Function: decl-spec-list-collect-idents

(defun decl-spec-list-collect-idents (c$::decl-spec-list)
 (declare (xargs :guard (decl-spec-listp c$::decl-spec-list)))
 (let ((__function__ 'decl-spec-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::decl-spec-list) nil)
   (t
    (union
       (decl-spec-collect-idents (car c$::decl-spec-list))
       (decl-spec-list-collect-idents (cdr c$::decl-spec-list)))))))

Function: typequal/attribspec-collect-idents

(defun typequal/attribspec-collect-idents (c$::typequal/attribspec)
 (declare
   (xargs
        :guard (c$::typequal/attribspec-p c$::typequal/attribspec)))
 (declare (ignorable c$::typequal/attribspec))
 (let ((__function__ 'typequal/attribspec-collect-idents))
  (declare (ignorable __function__))
  (c$::typequal/attribspec-case
       c$::typequal/attribspec
       :type nil
       :attrib
       (attrib-spec-collect-idents (c$::typequal/attribspec-attrib->spec
                                        c$::typequal/attribspec)))))

Function: typequal/attribspec-list-collect-idents

(defun typequal/attribspec-list-collect-idents
       (c$::typequal/attribspec-list)
 (declare
  (xargs
      :guard
      (c$::typequal/attribspec-listp c$::typequal/attribspec-list)))
 (let ((__function__ 'typequal/attribspec-list-collect-idents))
   (declare (ignorable __function__))
   (cond ((endp c$::typequal/attribspec-list)
          nil)
         (t (union (typequal/attribspec-collect-idents
                        (car c$::typequal/attribspec-list))
                   (typequal/attribspec-list-collect-idents
                        (cdr c$::typequal/attribspec-list)))))))

Function: typequal/attribspec-list-list-collect-idents

(defun typequal/attribspec-list-list-collect-idents
       (c$::typequal/attribspec-list-list)
 (declare (xargs :guard (typequal/attribspec-list-listp
                             c$::typequal/attribspec-list-list)))
 (let ((__function__ 'typequal/attribspec-list-list-collect-idents))
  (declare (ignorable __function__))
  (cond ((endp c$::typequal/attribspec-list-list)
         nil)
        (t (union (typequal/attribspec-list-collect-idents
                       (car c$::typequal/attribspec-list-list))
                  (typequal/attribspec-list-list-collect-idents
                       (cdr c$::typequal/attribspec-list-list)))))))

Function: initer-collect-idents

(defun initer-collect-idents (c$::initer)
  (declare (xargs :guard (initerp c$::initer)))
  (declare (ignorable c$::initer))
  (let ((__function__ 'initer-collect-idents))
    (declare (ignorable __function__))
    (initer-case
         c$::initer
         :single
         (expr-collect-idents (c$::initer-single->expr c$::initer))
         :list (desiniter-list-collect-idents
                    (c$::initer-list->elems c$::initer)))))

Function: initer-option-collect-idents

(defun initer-option-collect-idents (c$::initer-option)
  (declare (xargs :guard (initer-optionp c$::initer-option)))
  (let ((__function__ 'initer-option-collect-idents))
    (declare (ignorable __function__))
    (initer-option-case
         c$::initer-option
         :some (initer-collect-idents
                    (c$::initer-option-some->val c$::initer-option))
         :none nil)))

Function: desiniter-collect-idents

(defun desiniter-collect-idents (desiniter)
 (declare (xargs :guard (desiniterp desiniter)))
 (declare (ignorable desiniter))
 (let ((__function__ 'desiniter-collect-idents))
   (declare (ignorable __function__))
   (union
        (designor-list-collect-idents
             (c$::desiniter->designors desiniter))
        (initer-collect-idents (c$::desiniter->initer desiniter)))))

Function: desiniter-list-collect-idents

(defun desiniter-list-collect-idents (c$::desiniter-list)
 (declare (xargs :guard (desiniter-listp c$::desiniter-list)))
 (let ((__function__ 'desiniter-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::desiniter-list) nil)
   (t
    (union
       (desiniter-collect-idents (car c$::desiniter-list))
       (desiniter-list-collect-idents (cdr c$::desiniter-list)))))))

Function: designor-collect-idents

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

Function: designor-list-collect-idents

(defun designor-list-collect-idents (c$::designor-list)
 (declare (xargs :guard (designor-listp c$::designor-list)))
 (let ((__function__ 'designor-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::designor-list) nil)
   (t
    (union
         (designor-collect-idents (car c$::designor-list))
         (designor-list-collect-idents (cdr c$::designor-list)))))))

Function: declor-collect-idents

(defun declor-collect-idents (declor)
  (declare (xargs :guard (declorp declor)))
  (declare (ignorable declor))
  (let ((__function__ 'declor-collect-idents))
    (declare (ignorable __function__))
    (union (typequal/attribspec-list-list-collect-idents
                (c$::declor->pointers declor))
           (dirdeclor-collect-idents (declor->direct declor)))))

Function: declor-option-collect-idents

(defun declor-option-collect-idents (c$::declor-option)
  (declare (xargs :guard (declor-optionp c$::declor-option)))
  (let ((__function__ 'declor-option-collect-idents))
    (declare (ignorable __function__))
    (declor-option-case
         c$::declor-option
         :some (declor-collect-idents
                    (c$::declor-option-some->val c$::declor-option))
         :none nil)))

Function: dirdeclor-collect-idents

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

Function: absdeclor-collect-idents

(defun absdeclor-collect-idents (absdeclor)
  (declare (xargs :guard (absdeclorp absdeclor)))
  (declare (ignorable absdeclor))
  (let ((__function__ 'absdeclor-collect-idents))
    (declare (ignorable __function__))
    (union (typequal/attribspec-list-list-collect-idents
                (c$::absdeclor->pointers absdeclor))
           (dirabsdeclor-option-collect-idents
                (c$::absdeclor->direct? absdeclor)))))

Function: absdeclor-option-collect-idents

(defun absdeclor-option-collect-idents (c$::absdeclor-option)
 (declare (xargs :guard (absdeclor-optionp c$::absdeclor-option)))
 (let ((__function__ 'absdeclor-option-collect-idents))
  (declare (ignorable __function__))
  (absdeclor-option-case
   c$::absdeclor-option
   :some (absdeclor-collect-idents
              (c$::absdeclor-option-some->val c$::absdeclor-option))
   :none nil)))

Function: dirabsdeclor-collect-idents

(defun dirabsdeclor-collect-idents (c$::dirabsdeclor)
 (declare (xargs :guard (dirabsdeclorp c$::dirabsdeclor)))
 (declare (ignorable c$::dirabsdeclor))
 (let ((__function__ 'dirabsdeclor-collect-idents))
  (declare (ignorable __function__))
  (dirabsdeclor-case
   c$::dirabsdeclor
   :dummy-base nil
   :paren (absdeclor-collect-idents
               (c$::dirabsdeclor-paren->inner c$::dirabsdeclor))
   :array
   (union
     (dirabsdeclor-option-collect-idents
          (c$::dirabsdeclor-array->declor? c$::dirabsdeclor))
     (union
          (typequal/attribspec-list-collect-idents
               (c$::dirabsdeclor-array->qualspecs c$::dirabsdeclor))
          (expr-option-collect-idents
               (c$::dirabsdeclor-array->size? c$::dirabsdeclor))))
   :array-static1
   (union
    (dirabsdeclor-option-collect-idents
         (c$::dirabsdeclor-array-static1->declor? c$::dirabsdeclor))
    (union
     (typequal/attribspec-list-collect-idents
       (c$::dirabsdeclor-array-static1->qualspecs c$::dirabsdeclor))
     (expr-collect-idents
          (c$::dirabsdeclor-array-static1->size c$::dirabsdeclor))))
   :array-static2
   (union
    (dirabsdeclor-option-collect-idents
         (c$::dirabsdeclor-array-static2->declor? c$::dirabsdeclor))
    (union
     (typequal/attribspec-list-collect-idents
       (c$::dirabsdeclor-array-static2->qualspecs c$::dirabsdeclor))
     (expr-collect-idents
          (c$::dirabsdeclor-array-static2->size c$::dirabsdeclor))))
   :array-star
   (dirabsdeclor-option-collect-idents
        (c$::dirabsdeclor-array-star->declor? c$::dirabsdeclor))
   :function
   (union
      (dirabsdeclor-option-collect-idents
           (c$::dirabsdeclor-function->declor? c$::dirabsdeclor))
      (param-declon-list-collect-idents
           (c$::dirabsdeclor-function->params c$::dirabsdeclor))))))

Function: dirabsdeclor-option-collect-idents

(defun dirabsdeclor-option-collect-idents (c$::dirabsdeclor-option)
 (declare
      (xargs :guard (dirabsdeclor-optionp c$::dirabsdeclor-option)))
 (let ((__function__ 'dirabsdeclor-option-collect-idents))
  (declare (ignorable __function__))
  (dirabsdeclor-option-case
   c$::dirabsdeclor-option
   :some
   (dirabsdeclor-collect-idents
        (c$::dirabsdeclor-option-some->val c$::dirabsdeclor-option))
   :none nil)))

Function: param-declon-collect-idents

(defun param-declon-collect-idents (param-declon)
  (declare (xargs :guard (param-declonp param-declon)))
  (declare (ignorable param-declon))
  (let ((__function__ 'param-declon-collect-idents))
    (declare (ignorable __function__))
    (union (decl-spec-list-collect-idents
                (c$::param-declon->specs param-declon))
           (union (param-declor-collect-idents
                       (c$::param-declon->declor param-declon))
                  (attrib-spec-list-collect-idents
                       (c$::param-declon->attribs param-declon))))))

Function: param-declon-list-collect-idents

(defun param-declon-list-collect-idents (c$::param-declon-list)
 (declare (xargs :guard (param-declon-listp c$::param-declon-list)))
 (let ((__function__ 'param-declon-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::param-declon-list) nil)
   (t
    (union (param-declon-collect-idents (car c$::param-declon-list))
           (param-declon-list-collect-idents
                (cdr c$::param-declon-list)))))))

Function: param-declor-collect-idents

(defun param-declor-collect-idents (c$::param-declor)
 (declare (xargs :guard (param-declorp c$::param-declor)))
 (declare (ignorable c$::param-declor))
 (let ((__function__ 'param-declor-collect-idents))
  (declare (ignorable __function__))
  (param-declor-case
   c$::param-declor
   :nonabstract
   (declor-collect-idents
        (param-declor-nonabstract->declor c$::param-declor))
   :abstract
   (absdeclor-collect-idents
        (c$::param-declor-abstract->declor c$::param-declor))
   :none nil
   :ambig (amb-declor/absdeclor-collect-idents
               (c$::param-declor-ambig->declor c$::param-declor)))))

Function: tyname-collect-idents

(defun tyname-collect-idents (tyname)
 (declare (xargs :guard (tynamep tyname)))
 (declare (ignorable tyname))
 (let ((__function__ 'tyname-collect-idents))
  (declare (ignorable __function__))
  (union
   (spec/qual-list-collect-idents (c$::tyname->specquals tyname))
   (absdeclor-option-collect-idents (c$::tyname->declor? tyname)))))

Function: struni-spec-collect-idents

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

Function: struct-declon-collect-idents

(defun struct-declon-collect-idents (c$::struct-declon)
 (declare (xargs :guard (struct-declonp c$::struct-declon)))
 (declare (ignorable c$::struct-declon))
 (let ((__function__ 'struct-declon-collect-idents))
  (declare (ignorable __function__))
  (struct-declon-case
   c$::struct-declon
   :member
   (union
    (spec/qual-list-collect-idents
         (c$::struct-declon-member->specquals c$::struct-declon))
    (union
       (struct-declor-list-collect-idents
            (c$::struct-declon-member->declors c$::struct-declon))
       (attrib-spec-list-collect-idents
            (c$::struct-declon-member->attribs c$::struct-declon))))
   :statassert
   (statassert-collect-idents
       (c$::struct-declon-statassert->statassert c$::struct-declon))
   :empty nil)))

Function: struct-declon-list-collect-idents

(defun struct-declon-list-collect-idents (c$::struct-declon-list)
 (declare
      (xargs :guard (struct-declon-listp c$::struct-declon-list)))
 (let ((__function__ 'struct-declon-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::struct-declon-list) nil)
   (t
    (union
         (struct-declon-collect-idents (car c$::struct-declon-list))
         (struct-declon-list-collect-idents
              (cdr c$::struct-declon-list)))))))

Function: struct-declor-collect-idents

(defun struct-declor-collect-idents (struct-declor)
  (declare (xargs :guard (struct-declorp struct-declor)))
  (declare (ignorable struct-declor))
  (let ((__function__ 'struct-declor-collect-idents))
    (declare (ignorable __function__))
    (union (declor-option-collect-idents
                (c$::struct-declor->declor? struct-declor))
           (const-expr-option-collect-idents
                (c$::struct-declor->expr? struct-declor)))))

Function: struct-declor-list-collect-idents

(defun struct-declor-list-collect-idents (c$::struct-declor-list)
 (declare
      (xargs :guard (struct-declor-listp c$::struct-declor-list)))
 (let ((__function__ 'struct-declor-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::struct-declor-list) nil)
   (t
    (union
         (struct-declor-collect-idents (car c$::struct-declor-list))
         (struct-declor-list-collect-idents
              (cdr c$::struct-declor-list)))))))

Function: enum-spec-collect-idents

(defun enum-spec-collect-idents (enum-spec)
 (declare (xargs :guard (enum-specp enum-spec)))
 (declare (ignorable enum-spec))
 (let ((__function__ 'enum-spec-collect-idents))
  (declare (ignorable __function__))
  (union
      (ident-option-collect-idents (c$::enum-spec->name? enum-spec))
      (enumer-list-collect-idents
           (c$::enum-spec->enumers enum-spec)))))

Function: enumer-collect-idents

(defun enumer-collect-idents (enumer)
 (declare (xargs :guard (enumerp enumer)))
 (declare (ignorable enumer))
 (let ((__function__ 'enumer-collect-idents))
  (declare (ignorable __function__))
  (union
   (ident-collect-idents (c$::enumer->name enumer))
   (const-expr-option-collect-idents (c$::enumer->value? enumer)))))

Function: enumer-list-collect-idents

(defun enumer-list-collect-idents (c$::enumer-list)
 (declare (xargs :guard (enumer-listp c$::enumer-list)))
 (let ((__function__ 'enumer-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::enumer-list) nil)
   (t (union (enumer-collect-idents (car c$::enumer-list))
             (enumer-list-collect-idents (cdr c$::enumer-list)))))))

Function: statassert-collect-idents

(defun statassert-collect-idents (statassert)
  (declare (xargs :guard (statassertp statassert)))
  (declare (ignorable statassert))
  (let ((__function__ 'statassert-collect-idents))
    (declare (ignorable __function__))
    (const-expr-collect-idents (c$::statassert->test statassert))))

Function: attrib-collect-idents

(defun attrib-collect-idents (c$::attrib)
 (declare (xargs :guard (c$::attribp c$::attrib)))
 (declare (ignorable c$::attrib))
 (let ((__function__ 'attrib-collect-idents))
  (declare (ignorable __function__))
  (c$::attrib-case
   c$::attrib
   :name nil
   :name-params (expr-list-collect-idents
                     (c$::attrib-name-params->params c$::attrib)))))

Function: attrib-list-collect-idents

(defun attrib-list-collect-idents (c$::attrib-list)
 (declare (xargs :guard (c$::attrib-listp c$::attrib-list)))
 (let ((__function__ 'attrib-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::attrib-list) nil)
   (t (union (attrib-collect-idents (car c$::attrib-list))
             (attrib-list-collect-idents (cdr c$::attrib-list)))))))

Function: attrib-spec-collect-idents

(defun attrib-spec-collect-idents (c$::attrib-spec)
  (declare (xargs :guard (c$::attrib-specp c$::attrib-spec)))
  (declare (ignorable c$::attrib-spec))
  (let ((__function__ 'attrib-spec-collect-idents))
    (declare (ignorable __function__))
    (attrib-list-collect-idents
         (c$::attrib-spec->attribs c$::attrib-spec))))

Function: attrib-spec-list-collect-idents

(defun attrib-spec-list-collect-idents (c$::attrib-spec-list)
 (declare (xargs :guard (attrib-spec-listp c$::attrib-spec-list)))
 (let ((__function__ 'attrib-spec-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::attrib-spec-list) nil)
   (t (union (attrib-spec-collect-idents (car c$::attrib-spec-list))
             (attrib-spec-list-collect-idents
                  (cdr c$::attrib-spec-list)))))))

Function: init-declor-collect-idents

(defun init-declor-collect-idents (init-declor)
  (declare (xargs :guard (init-declorp init-declor)))
  (declare (ignorable init-declor))
  (let ((__function__ 'init-declor-collect-idents))
    (declare (ignorable __function__))
    (union (declor-collect-idents (init-declor->declor init-declor))
           (union (attrib-spec-list-collect-idents
                       (c$::init-declor->attribs init-declor))
                  (initer-option-collect-idents
                       (init-declor->initer? init-declor))))))

Function: init-declor-list-collect-idents

(defun init-declor-list-collect-idents (c$::init-declor-list)
 (declare (xargs :guard (init-declor-listp c$::init-declor-list)))
 (let ((__function__ 'init-declor-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::init-declor-list) nil)
   (t (union (init-declor-collect-idents (car c$::init-declor-list))
             (init-declor-list-collect-idents
                  (cdr c$::init-declor-list)))))))

Function: declon-collect-idents

(defun declon-collect-idents (declon)
 (declare (xargs :guard (declonp declon)))
 (declare (ignorable declon))
 (let ((__function__ 'declon-collect-idents))
  (declare (ignorable __function__))
  (declon-case
   declon
   :declon
   (union
       (decl-spec-list-collect-idents (declon-declon->specs declon))
       (init-declor-list-collect-idents
            (declon-declon->declors declon)))
   :statassert (statassert-collect-idents
                    (c$::declon-statassert->statassert declon)))))

Function: declon-list-collect-idents

(defun declon-list-collect-idents (c$::declon-list)
 (declare (xargs :guard (declon-listp c$::declon-list)))
 (let ((__function__ 'declon-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::declon-list) nil)
   (t (union (declon-collect-idents (car c$::declon-list))
             (declon-list-collect-idents (cdr c$::declon-list)))))))

Function: label-collect-idents

(defun label-collect-idents (c$::label)
 (declare (xargs :guard (labelp c$::label)))
 (declare (ignorable c$::label))
 (let ((__function__ 'label-collect-idents))
  (declare (ignorable __function__))
  (label-case
   c$::label
   :name
   (union (ident-collect-idents (c$::label-name->name c$::label))
          (attrib-spec-list-collect-idents
               (c$::label-name->attribs c$::label)))
   :casexpr
   (union
     (const-expr-collect-idents (c$::label-casexpr->expr c$::label))
     (const-expr-option-collect-idents
          (c$::label-casexpr->range? c$::label)))
   :default nil)))

Function: asm-output-collect-idents

(defun asm-output-collect-idents (c$::asm-output)
 (declare (xargs :guard (c$::asm-outputp c$::asm-output)))
 (declare (ignorable c$::asm-output))
 (let ((__function__ 'asm-output-collect-idents))
  (declare (ignorable __function__))
  (union
    (ident-option-collect-idents
         (c$::asm-output->name? c$::asm-output))
    (expr-collect-idents (c$::asm-output->lvalue c$::asm-output)))))

Function: asm-output-list-collect-idents

(defun asm-output-list-collect-idents (c$::asm-output-list)
 (declare (xargs :guard (c$::asm-output-listp c$::asm-output-list)))
 (let ((__function__ 'asm-output-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::asm-output-list) nil)
   (t
    (union
     (asm-output-collect-idents (car c$::asm-output-list))
     (asm-output-list-collect-idents (cdr c$::asm-output-list)))))))

Function: asm-input-collect-idents

(defun asm-input-collect-idents (c$::asm-input)
 (declare (xargs :guard (c$::asm-inputp c$::asm-input)))
 (declare (ignorable c$::asm-input))
 (let ((__function__ 'asm-input-collect-idents))
  (declare (ignorable __function__))
  (union
      (ident-option-collect-idents
           (c$::asm-input->name? c$::asm-input))
      (expr-collect-idents (c$::asm-input->rvalue c$::asm-input)))))

Function: asm-input-list-collect-idents

(defun asm-input-list-collect-idents (c$::asm-input-list)
 (declare (xargs :guard (c$::asm-input-listp c$::asm-input-list)))
 (let ((__function__ 'asm-input-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::asm-input-list) nil)
   (t
    (union
       (asm-input-collect-idents (car c$::asm-input-list))
       (asm-input-list-collect-idents (cdr c$::asm-input-list)))))))

Function: asm-stmt-collect-idents

(defun asm-stmt-collect-idents (c$::asm-stmt)
  (declare (xargs :guard (c$::asm-stmtp c$::asm-stmt)))
  (declare (ignorable c$::asm-stmt))
  (let ((__function__ 'asm-stmt-collect-idents))
    (declare (ignorable __function__))
    (union (asm-output-list-collect-idents
                (c$::asm-stmt->outputs c$::asm-stmt))
           (union (asm-input-list-collect-idents
                       (c$::asm-stmt->inputs c$::asm-stmt))
                  (ident-list-collect-idents
                       (c$::asm-stmt->labels c$::asm-stmt))))))

Function: stmt-collect-idents

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

Function: comp-stmt-collect-idents

(defun comp-stmt-collect-idents (comp-stmt)
  (declare (xargs :guard (comp-stmtp comp-stmt)))
  (declare (ignorable comp-stmt))
  (let ((__function__ 'comp-stmt-collect-idents))
    (declare (ignorable __function__))
    (block-item-list-collect-idents (comp-stmt->items comp-stmt))))

Function: block-item-collect-idents

(defun block-item-collect-idents (c$::block-item)
 (declare (xargs :guard (block-itemp c$::block-item)))
 (declare (ignorable c$::block-item))
 (let ((__function__ 'block-item-collect-idents))
  (declare (ignorable __function__))
  (block-item-case
    c$::block-item
    :declon (declon-collect-idents
                 (c$::block-item-declon->declon c$::block-item))
    :stmt
    (stmt-collect-idents (c$::block-item-stmt->stmt c$::block-item))
    :ambig
    (amb-declon/stmt-collect-idents
         (c$::block-item-ambig->declon/stmt c$::block-item)))))

Function: block-item-list-collect-idents

(defun block-item-list-collect-idents (c$::block-item-list)
 (declare (xargs :guard (block-item-listp c$::block-item-list)))
 (let ((__function__ 'block-item-list-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((endp c$::block-item-list) nil)
   (t
    (union
     (block-item-collect-idents (car c$::block-item-list))
     (block-item-list-collect-idents (cdr c$::block-item-list)))))))

Function: amb-expr/tyname-collect-idents

(defun amb-expr/tyname-collect-idents (c$::amb-expr/tyname)
 (declare
      (xargs :guard (c$::amb-expr/tyname-p c$::amb-expr/tyname)))
 (declare (ignorable c$::amb-expr/tyname))
 (let ((__function__ 'amb-expr/tyname-collect-idents))
   (declare (ignorable __function__))
   (union (expr-collect-idents
               (c$::amb-expr/tyname->expr c$::amb-expr/tyname))
          (tyname-collect-idents
               (c$::amb-expr/tyname->tyname c$::amb-expr/tyname)))))

Function: amb-declor/absdeclor-collect-idents

(defun amb-declor/absdeclor-collect-idents
       (c$::amb-declor/absdeclor)
 (declare
  (xargs
      :guard (c$::amb-declor/absdeclor-p c$::amb-declor/absdeclor)))
 (declare (ignorable c$::amb-declor/absdeclor))
 (let ((__function__ 'amb-declor/absdeclor-collect-idents))
  (declare (ignorable __function__))
  (union
   (declor-collect-idents
        (c$::amb-declor/absdeclor->declor c$::amb-declor/absdeclor))
   (absdeclor-collect-idents (c$::amb-declor/absdeclor->absdeclor
                                  c$::amb-declor/absdeclor)))))

Function: amb-declon/stmt-collect-idents

(defun amb-declon/stmt-collect-idents (c$::amb-declon/stmt)
  (declare
       (xargs :guard (c$::amb-declon/stmt-p c$::amb-declon/stmt)))
  (declare (ignorable c$::amb-declon/stmt))
  (let ((__function__ 'amb-declon/stmt-collect-idents))
    (declare (ignorable __function__))
    (union (declon-collect-idents
                (c$::amb-declon/stmt->declon c$::amb-declon/stmt))
           (expr-collect-idents
                (c$::amb-declon/stmt->expr c$::amb-declon/stmt)))))

Theorem: return-type-of-expr-collect-idents.result

(defthm return-type-of-expr-collect-idents.result
  (b* ((fty::?result (expr-collect-idents c$::expr)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-expr-list-collect-idents.result

(defthm return-type-of-expr-list-collect-idents.result
  (b* ((fty::?result (expr-list-collect-idents c$::expr-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-expr-option-collect-idents.result

(defthm return-type-of-expr-option-collect-idents.result
  (b* ((fty::?result (expr-option-collect-idents c$::expr-option)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-const-expr-collect-idents.result

(defthm return-type-of-const-expr-collect-idents.result
  (b* ((fty::?result (const-expr-collect-idents const-expr)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-const-expr-option-collect-idents.result

(defthm return-type-of-const-expr-option-collect-idents.result
  (b*
    ((fty::?result
          (const-expr-option-collect-idents c$::const-expr-option)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-genassoc-collect-idents.result

(defthm return-type-of-genassoc-collect-idents.result
  (b* ((fty::?result (genassoc-collect-idents c$::genassoc)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-genassoc-list-collect-idents.result

(defthm return-type-of-genassoc-list-collect-idents.result
  (b*
   ((fty::?result (genassoc-list-collect-idents c$::genassoc-list)))
   (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-member-designor-collect-idents.result

(defthm return-type-of-member-designor-collect-idents.result
  (b* ((fty::?result
            (member-designor-collect-idents c$::member-designor)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-type-spec-collect-idents.result

(defthm return-type-of-type-spec-collect-idents.result
  (b* ((fty::?result (type-spec-collect-idents c$::type-spec)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-spec/qual-collect-idents.result

(defthm return-type-of-spec/qual-collect-idents.result
  (b* ((fty::?result (spec/qual-collect-idents c$::spec/qual)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-spec/qual-list-collect-idents.result
  (b* ((fty::?result
            (spec/qual-list-collect-idents c$::spec/qual-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-align-spec-collect-idents.result

(defthm return-type-of-align-spec-collect-idents.result
  (b* ((fty::?result (align-spec-collect-idents c$::align-spec)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-decl-spec-collect-idents.result

(defthm return-type-of-decl-spec-collect-idents.result
  (b* ((fty::?result (decl-spec-collect-idents c$::decl-spec)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-decl-spec-list-collect-idents.result

(defthm return-type-of-decl-spec-list-collect-idents.result
  (b* ((fty::?result
            (decl-spec-list-collect-idents c$::decl-spec-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-typequal/attribspec-collect-idents.result

(defthm return-type-of-typequal/attribspec-collect-idents.result
 (b*
  ((fty::?result
      (typequal/attribspec-collect-idents c$::typequal/attribspec)))
  (ident-setp fty::result))
 :rule-classes :rewrite)

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

(defthm
      return-type-of-typequal/attribspec-list-collect-idents.result
  (b* ((fty::?result (typequal/attribspec-list-collect-idents
                          c$::typequal/attribspec-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

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

(defthm
 return-type-of-typequal/attribspec-list-list-collect-idents.result
 (b* ((fty::?result (typequal/attribspec-list-list-collect-idents
                         c$::typequal/attribspec-list-list)))
   (ident-setp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-initer-collect-idents.result

(defthm return-type-of-initer-collect-idents.result
  (b* ((fty::?result (initer-collect-idents c$::initer)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-initer-option-collect-idents.result

(defthm return-type-of-initer-option-collect-idents.result
  (b*
   ((fty::?result (initer-option-collect-idents c$::initer-option)))
   (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-desiniter-collect-idents.result

(defthm return-type-of-desiniter-collect-idents.result
  (b* ((fty::?result (desiniter-collect-idents desiniter)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-desiniter-list-collect-idents.result

(defthm return-type-of-desiniter-list-collect-idents.result
  (b* ((fty::?result
            (desiniter-list-collect-idents c$::desiniter-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-designor-collect-idents.result

(defthm return-type-of-designor-collect-idents.result
  (b* ((fty::?result (designor-collect-idents c$::designor)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-designor-list-collect-idents.result

(defthm return-type-of-designor-list-collect-idents.result
  (b*
   ((fty::?result (designor-list-collect-idents c$::designor-list)))
   (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-declor-collect-idents.result

(defthm return-type-of-declor-collect-idents.result
  (b* ((fty::?result (declor-collect-idents declor)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-declor-option-collect-idents.result

(defthm return-type-of-declor-option-collect-idents.result
  (b*
   ((fty::?result (declor-option-collect-idents c$::declor-option)))
   (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-dirdeclor-collect-idents.result

(defthm return-type-of-dirdeclor-collect-idents.result
  (b* ((fty::?result (dirdeclor-collect-idents dirdeclor)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-absdeclor-collect-idents.result

(defthm return-type-of-absdeclor-collect-idents.result
  (b* ((fty::?result (absdeclor-collect-idents absdeclor)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-absdeclor-option-collect-idents.result

(defthm return-type-of-absdeclor-option-collect-idents.result
  (b* ((fty::?result
            (absdeclor-option-collect-idents c$::absdeclor-option)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-dirabsdeclor-collect-idents.result

(defthm return-type-of-dirabsdeclor-collect-idents.result
 (b* ((fty::?result (dirabsdeclor-collect-idents c$::dirabsdeclor)))
   (ident-setp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-dirabsdeclor-option-collect-idents.result

(defthm return-type-of-dirabsdeclor-option-collect-idents.result
 (b*
  ((fty::?result
      (dirabsdeclor-option-collect-idents c$::dirabsdeclor-option)))
  (ident-setp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-param-declon-collect-idents.result

(defthm return-type-of-param-declon-collect-idents.result
  (b* ((fty::?result (param-declon-collect-idents param-declon)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-param-declon-list-collect-idents.result

(defthm return-type-of-param-declon-list-collect-idents.result
  (b*
    ((fty::?result
          (param-declon-list-collect-idents c$::param-declon-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-param-declor-collect-idents.result

(defthm return-type-of-param-declor-collect-idents.result
 (b* ((fty::?result (param-declor-collect-idents c$::param-declor)))
   (ident-setp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-tyname-collect-idents.result

(defthm return-type-of-tyname-collect-idents.result
  (b* ((fty::?result (tyname-collect-idents tyname)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-struni-spec-collect-idents.result

(defthm return-type-of-struni-spec-collect-idents.result
  (b* ((fty::?result (struni-spec-collect-idents struni-spec)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-struct-declon-collect-idents.result

(defthm return-type-of-struct-declon-collect-idents.result
  (b*
   ((fty::?result (struct-declon-collect-idents c$::struct-declon)))
   (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-struct-declon-list-collect-idents.result

(defthm return-type-of-struct-declon-list-collect-idents.result
 (b*
  ((fty::?result
        (struct-declon-list-collect-idents c$::struct-declon-list)))
  (ident-setp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-struct-declor-collect-idents.result

(defthm return-type-of-struct-declor-collect-idents.result
  (b* ((fty::?result (struct-declor-collect-idents struct-declor)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-struct-declor-list-collect-idents.result

(defthm return-type-of-struct-declor-list-collect-idents.result
 (b*
  ((fty::?result
        (struct-declor-list-collect-idents c$::struct-declor-list)))
  (ident-setp fty::result))
 :rule-classes :rewrite)

Theorem: return-type-of-enum-spec-collect-idents.result

(defthm return-type-of-enum-spec-collect-idents.result
  (b* ((fty::?result (enum-spec-collect-idents enum-spec)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-enumer-collect-idents.result

(defthm return-type-of-enumer-collect-idents.result
  (b* ((fty::?result (enumer-collect-idents enumer)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-enumer-list-collect-idents.result

(defthm return-type-of-enumer-list-collect-idents.result
  (b* ((fty::?result (enumer-list-collect-idents c$::enumer-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-statassert-collect-idents.result

(defthm return-type-of-statassert-collect-idents.result
  (b* ((fty::?result (statassert-collect-idents statassert)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-attrib-collect-idents.result

(defthm return-type-of-attrib-collect-idents.result
  (b* ((fty::?result (attrib-collect-idents c$::attrib)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-attrib-list-collect-idents.result

(defthm return-type-of-attrib-list-collect-idents.result
  (b* ((fty::?result (attrib-list-collect-idents c$::attrib-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-attrib-spec-collect-idents.result

(defthm return-type-of-attrib-spec-collect-idents.result
  (b* ((fty::?result (attrib-spec-collect-idents c$::attrib-spec)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-attrib-spec-list-collect-idents.result

(defthm return-type-of-attrib-spec-list-collect-idents.result
  (b* ((fty::?result
            (attrib-spec-list-collect-idents c$::attrib-spec-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-init-declor-collect-idents.result

(defthm return-type-of-init-declor-collect-idents.result
  (b* ((fty::?result (init-declor-collect-idents init-declor)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-init-declor-list-collect-idents.result

(defthm return-type-of-init-declor-list-collect-idents.result
  (b* ((fty::?result
            (init-declor-list-collect-idents c$::init-declor-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-declon-collect-idents.result

(defthm return-type-of-declon-collect-idents.result
  (b* ((fty::?result (declon-collect-idents declon)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-declon-list-collect-idents.result

(defthm return-type-of-declon-list-collect-idents.result
  (b* ((fty::?result (declon-list-collect-idents c$::declon-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-label-collect-idents.result

(defthm return-type-of-label-collect-idents.result
  (b* ((fty::?result (label-collect-idents c$::label)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-asm-output-collect-idents.result

(defthm return-type-of-asm-output-collect-idents.result
  (b* ((fty::?result (asm-output-collect-idents c$::asm-output)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-asm-output-list-collect-idents.result

(defthm return-type-of-asm-output-list-collect-idents.result
  (b* ((fty::?result
            (asm-output-list-collect-idents c$::asm-output-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-asm-input-collect-idents.result

(defthm return-type-of-asm-input-collect-idents.result
  (b* ((fty::?result (asm-input-collect-idents c$::asm-input)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-asm-input-list-collect-idents.result

(defthm return-type-of-asm-input-list-collect-idents.result
  (b* ((fty::?result
            (asm-input-list-collect-idents c$::asm-input-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-asm-stmt-collect-idents.result

(defthm return-type-of-asm-stmt-collect-idents.result
  (b* ((fty::?result (asm-stmt-collect-idents c$::asm-stmt)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-stmt-collect-idents.result

(defthm return-type-of-stmt-collect-idents.result
  (b* ((fty::?result (stmt-collect-idents c$::stmt)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-comp-stmt-collect-idents.result

(defthm return-type-of-comp-stmt-collect-idents.result
  (b* ((fty::?result (comp-stmt-collect-idents comp-stmt)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-block-item-collect-idents.result

(defthm return-type-of-block-item-collect-idents.result
  (b* ((fty::?result (block-item-collect-idents c$::block-item)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-block-item-list-collect-idents.result

(defthm return-type-of-block-item-list-collect-idents.result
  (b* ((fty::?result
            (block-item-list-collect-idents c$::block-item-list)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-amb-expr/tyname-collect-idents.result
  (b* ((fty::?result
            (amb-expr/tyname-collect-idents c$::amb-expr/tyname)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-amb-declor/absdeclor-collect-idents.result
 (b*
  ((fty::?result
    (amb-declor/absdeclor-collect-idents c$::amb-declor/absdeclor)))
  (ident-setp fty::result))
 :rule-classes :rewrite)

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

(defthm return-type-of-amb-declon/stmt-collect-idents.result
  (b* ((fty::?result
            (amb-declon/stmt-collect-idents c$::amb-declon/stmt)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: expr-collect-idents-of-expr-fix-expr

(defthm expr-collect-idents-of-expr-fix-expr
  (equal (expr-collect-idents (expr-fix c$::expr))
         (expr-collect-idents c$::expr)))

Theorem: expr-list-collect-idents-of-expr-list-fix-expr-list

(defthm expr-list-collect-idents-of-expr-list-fix-expr-list
  (equal (expr-list-collect-idents (expr-list-fix c$::expr-list))
         (expr-list-collect-idents c$::expr-list)))

Theorem: expr-option-collect-idents-of-expr-option-fix-expr-option

(defthm expr-option-collect-idents-of-expr-option-fix-expr-option
 (equal
      (expr-option-collect-idents (expr-option-fix c$::expr-option))
      (expr-option-collect-idents c$::expr-option)))

Theorem: const-expr-collect-idents-of-const-expr-fix-const-expr

(defthm const-expr-collect-idents-of-const-expr-fix-const-expr
  (equal (const-expr-collect-idents (c$::const-expr-fix const-expr))
         (const-expr-collect-idents const-expr)))

Theorem: const-expr-option-collect-idents-of-const-expr-option-fix-const-expr-option

(defthm
 const-expr-option-collect-idents-of-const-expr-option-fix-const-expr-option
 (equal (const-expr-option-collect-idents
             (const-expr-option-fix c$::const-expr-option))
        (const-expr-option-collect-idents c$::const-expr-option)))

Theorem: genassoc-collect-idents-of-genassoc-fix-genassoc

(defthm genassoc-collect-idents-of-genassoc-fix-genassoc
  (equal (genassoc-collect-idents (genassoc-fix c$::genassoc))
         (genassoc-collect-idents c$::genassoc)))

Theorem: genassoc-list-collect-idents-of-genassoc-list-fix-genassoc-list

(defthm
    genassoc-list-collect-idents-of-genassoc-list-fix-genassoc-list
  (equal (genassoc-list-collect-idents
              (genassoc-list-fix c$::genassoc-list))
         (genassoc-list-collect-idents c$::genassoc-list)))

Theorem: member-designor-collect-idents-of-member-designor-fix-member-designor

(defthm
 member-designor-collect-idents-of-member-designor-fix-member-designor
 (equal (member-designor-collect-idents
             (member-designor-fix c$::member-designor))
        (member-designor-collect-idents c$::member-designor)))

Theorem: type-spec-collect-idents-of-type-spec-fix-type-spec

(defthm type-spec-collect-idents-of-type-spec-fix-type-spec
  (equal (type-spec-collect-idents (type-spec-fix c$::type-spec))
         (type-spec-collect-idents c$::type-spec)))

Theorem: spec/qual-collect-idents-of-spec/qual-fix-spec/qual

(defthm spec/qual-collect-idents-of-spec/qual-fix-spec/qual
  (equal (spec/qual-collect-idents (spec/qual-fix c$::spec/qual))
         (spec/qual-collect-idents c$::spec/qual)))

Theorem: spec/qual-list-collect-idents-of-spec/qual-list-fix-spec/qual-list

(defthm
 spec/qual-list-collect-idents-of-spec/qual-list-fix-spec/qual-list
 (equal (spec/qual-list-collect-idents
             (spec/qual-list-fix c$::spec/qual-list))
        (spec/qual-list-collect-idents c$::spec/qual-list)))

Theorem: align-spec-collect-idents-of-align-spec-fix-align-spec

(defthm align-spec-collect-idents-of-align-spec-fix-align-spec
  (equal (align-spec-collect-idents (align-spec-fix c$::align-spec))
         (align-spec-collect-idents c$::align-spec)))

Theorem: decl-spec-collect-idents-of-decl-spec-fix-decl-spec

(defthm decl-spec-collect-idents-of-decl-spec-fix-decl-spec
  (equal (decl-spec-collect-idents (decl-spec-fix c$::decl-spec))
         (decl-spec-collect-idents c$::decl-spec)))

Theorem: decl-spec-list-collect-idents-of-decl-spec-list-fix-decl-spec-list

(defthm
 decl-spec-list-collect-idents-of-decl-spec-list-fix-decl-spec-list
 (equal (decl-spec-list-collect-idents
             (decl-spec-list-fix c$::decl-spec-list))
        (decl-spec-list-collect-idents c$::decl-spec-list)))

Theorem: typequal/attribspec-collect-idents-of-typequal/attribspec-fix-typequal/attribspec

(defthm
 typequal/attribspec-collect-idents-of-typequal/attribspec-fix-typequal/attribspec
 (equal
      (typequal/attribspec-collect-idents
           (c$::typequal/attribspec-fix c$::typequal/attribspec))
      (typequal/attribspec-collect-idents c$::typequal/attribspec)))

Theorem: typequal/attribspec-list-collect-idents-of-typequal/attribspec-list-fix-typequal/attribspec-list

(defthm
 typequal/attribspec-list-collect-idents-of-typequal/attribspec-list-fix-typequal/attribspec-list
 (equal
  (typequal/attribspec-list-collect-idents
    (c$::typequal/attribspec-list-fix c$::typequal/attribspec-list))
  (typequal/attribspec-list-collect-idents
       c$::typequal/attribspec-list)))

Theorem: typequal/attribspec-list-list-collect-idents-of-typequal/attribspec-list-list-fix-typequal/attribspec-list-list

(defthm
 typequal/attribspec-list-list-collect-idents-of-typequal/attribspec-list-list-fix-typequal/attribspec-list-list
 (equal (typequal/attribspec-list-list-collect-idents
             (c$::typequal/attribspec-list-list-fix
                  c$::typequal/attribspec-list-list))
        (typequal/attribspec-list-list-collect-idents
             c$::typequal/attribspec-list-list)))

Theorem: initer-collect-idents-of-initer-fix-initer

(defthm initer-collect-idents-of-initer-fix-initer
  (equal (initer-collect-idents (initer-fix c$::initer))
         (initer-collect-idents c$::initer)))

Theorem: initer-option-collect-idents-of-initer-option-fix-initer-option

(defthm
    initer-option-collect-idents-of-initer-option-fix-initer-option
  (equal (initer-option-collect-idents
              (initer-option-fix c$::initer-option))
         (initer-option-collect-idents c$::initer-option)))

Theorem: desiniter-collect-idents-of-desiniter-fix-desiniter

(defthm desiniter-collect-idents-of-desiniter-fix-desiniter
  (equal (desiniter-collect-idents (desiniter-fix desiniter))
         (desiniter-collect-idents desiniter)))

Theorem: desiniter-list-collect-idents-of-desiniter-list-fix-desiniter-list

(defthm
 desiniter-list-collect-idents-of-desiniter-list-fix-desiniter-list
 (equal (desiniter-list-collect-idents
             (desiniter-list-fix c$::desiniter-list))
        (desiniter-list-collect-idents c$::desiniter-list)))

Theorem: designor-collect-idents-of-designor-fix-designor

(defthm designor-collect-idents-of-designor-fix-designor
  (equal (designor-collect-idents (designor-fix c$::designor))
         (designor-collect-idents c$::designor)))

Theorem: designor-list-collect-idents-of-designor-list-fix-designor-list

(defthm
    designor-list-collect-idents-of-designor-list-fix-designor-list
  (equal (designor-list-collect-idents
              (designor-list-fix c$::designor-list))
         (designor-list-collect-idents c$::designor-list)))

Theorem: declor-collect-idents-of-declor-fix-declor

(defthm declor-collect-idents-of-declor-fix-declor
  (equal (declor-collect-idents (declor-fix declor))
         (declor-collect-idents declor)))

Theorem: declor-option-collect-idents-of-declor-option-fix-declor-option

(defthm
    declor-option-collect-idents-of-declor-option-fix-declor-option
  (equal (declor-option-collect-idents
              (declor-option-fix c$::declor-option))
         (declor-option-collect-idents c$::declor-option)))

Theorem: dirdeclor-collect-idents-of-dirdeclor-fix-dirdeclor

(defthm dirdeclor-collect-idents-of-dirdeclor-fix-dirdeclor
  (equal (dirdeclor-collect-idents (dirdeclor-fix dirdeclor))
         (dirdeclor-collect-idents dirdeclor)))

Theorem: absdeclor-collect-idents-of-absdeclor-fix-absdeclor

(defthm absdeclor-collect-idents-of-absdeclor-fix-absdeclor
  (equal (absdeclor-collect-idents (absdeclor-fix absdeclor))
         (absdeclor-collect-idents absdeclor)))

Theorem: absdeclor-option-collect-idents-of-absdeclor-option-fix-absdeclor-option

(defthm
 absdeclor-option-collect-idents-of-absdeclor-option-fix-absdeclor-option
 (equal (absdeclor-option-collect-idents
             (absdeclor-option-fix c$::absdeclor-option))
        (absdeclor-option-collect-idents c$::absdeclor-option)))

Theorem: dirabsdeclor-collect-idents-of-dirabsdeclor-fix-dirabsdeclor

(defthm dirabsdeclor-collect-idents-of-dirabsdeclor-fix-dirabsdeclor
 (equal
   (dirabsdeclor-collect-idents (dirabsdeclor-fix c$::dirabsdeclor))
   (dirabsdeclor-collect-idents c$::dirabsdeclor)))

Theorem: dirabsdeclor-option-collect-idents-of-dirabsdeclor-option-fix-dirabsdeclor-option

(defthm
 dirabsdeclor-option-collect-idents-of-dirabsdeclor-option-fix-dirabsdeclor-option
 (equal
      (dirabsdeclor-option-collect-idents
           (dirabsdeclor-option-fix c$::dirabsdeclor-option))
      (dirabsdeclor-option-collect-idents c$::dirabsdeclor-option)))

Theorem: param-declon-collect-idents-of-param-declon-fix-param-declon

(defthm param-declon-collect-idents-of-param-declon-fix-param-declon
  (equal
       (param-declon-collect-idents (param-declon-fix param-declon))
       (param-declon-collect-idents param-declon)))

Theorem: param-declon-list-collect-idents-of-param-declon-list-fix-param-declon-list

(defthm
 param-declon-list-collect-idents-of-param-declon-list-fix-param-declon-list
 (equal (param-declon-list-collect-idents
             (param-declon-list-fix c$::param-declon-list))
        (param-declon-list-collect-idents c$::param-declon-list)))

Theorem: param-declor-collect-idents-of-param-declor-fix-param-declor

(defthm param-declor-collect-idents-of-param-declor-fix-param-declor
 (equal
   (param-declor-collect-idents (param-declor-fix c$::param-declor))
   (param-declor-collect-idents c$::param-declor)))

Theorem: tyname-collect-idents-of-tyname-fix-tyname

(defthm tyname-collect-idents-of-tyname-fix-tyname
  (equal (tyname-collect-idents (tyname-fix tyname))
         (tyname-collect-idents tyname)))

Theorem: struni-spec-collect-idents-of-struni-spec-fix-struni-spec

(defthm struni-spec-collect-idents-of-struni-spec-fix-struni-spec
  (equal (struni-spec-collect-idents (struni-spec-fix struni-spec))
         (struni-spec-collect-idents struni-spec)))

Theorem: struct-declon-collect-idents-of-struct-declon-fix-struct-declon

(defthm
    struct-declon-collect-idents-of-struct-declon-fix-struct-declon
  (equal (struct-declon-collect-idents
              (struct-declon-fix c$::struct-declon))
         (struct-declon-collect-idents c$::struct-declon)))

Theorem: struct-declon-list-collect-idents-of-struct-declon-list-fix-struct-declon-list

(defthm
 struct-declon-list-collect-idents-of-struct-declon-list-fix-struct-declon-list
 (equal (struct-declon-list-collect-idents
             (struct-declon-list-fix c$::struct-declon-list))
        (struct-declon-list-collect-idents c$::struct-declon-list)))

Theorem: struct-declor-collect-idents-of-struct-declor-fix-struct-declor

(defthm
    struct-declor-collect-idents-of-struct-declor-fix-struct-declor
 (equal
    (struct-declor-collect-idents (struct-declor-fix struct-declor))
    (struct-declor-collect-idents struct-declor)))

Theorem: struct-declor-list-collect-idents-of-struct-declor-list-fix-struct-declor-list

(defthm
 struct-declor-list-collect-idents-of-struct-declor-list-fix-struct-declor-list
 (equal (struct-declor-list-collect-idents
             (struct-declor-list-fix c$::struct-declor-list))
        (struct-declor-list-collect-idents c$::struct-declor-list)))

Theorem: enum-spec-collect-idents-of-enum-spec-fix-enum-spec

(defthm enum-spec-collect-idents-of-enum-spec-fix-enum-spec
  (equal (enum-spec-collect-idents (enum-spec-fix enum-spec))
         (enum-spec-collect-idents enum-spec)))

Theorem: enumer-collect-idents-of-enumer-fix-enumer

(defthm enumer-collect-idents-of-enumer-fix-enumer
  (equal (enumer-collect-idents (enumer-fix enumer))
         (enumer-collect-idents enumer)))

Theorem: enumer-list-collect-idents-of-enumer-list-fix-enumer-list

(defthm enumer-list-collect-idents-of-enumer-list-fix-enumer-list
 (equal
      (enumer-list-collect-idents (enumer-list-fix c$::enumer-list))
      (enumer-list-collect-idents c$::enumer-list)))

Theorem: statassert-collect-idents-of-statassert-fix-statassert

(defthm statassert-collect-idents-of-statassert-fix-statassert
  (equal (statassert-collect-idents (statassert-fix statassert))
         (statassert-collect-idents statassert)))

Theorem: attrib-collect-idents-of-attrib-fix-attrib

(defthm attrib-collect-idents-of-attrib-fix-attrib
  (equal (attrib-collect-idents (c$::attrib-fix c$::attrib))
         (attrib-collect-idents c$::attrib)))

Theorem: attrib-list-collect-idents-of-attrib-list-fix-attrib-list

(defthm attrib-list-collect-idents-of-attrib-list-fix-attrib-list
 (equal
  (attrib-list-collect-idents (c$::attrib-list-fix c$::attrib-list))
  (attrib-list-collect-idents c$::attrib-list)))

Theorem: attrib-spec-collect-idents-of-attrib-spec-fix-attrib-spec

(defthm attrib-spec-collect-idents-of-attrib-spec-fix-attrib-spec
 (equal
  (attrib-spec-collect-idents (c$::attrib-spec-fix c$::attrib-spec))
  (attrib-spec-collect-idents c$::attrib-spec)))

Theorem: attrib-spec-list-collect-idents-of-attrib-spec-list-fix-attrib-spec-list

(defthm
 attrib-spec-list-collect-idents-of-attrib-spec-list-fix-attrib-spec-list
 (equal (attrib-spec-list-collect-idents
             (c$::attrib-spec-list-fix c$::attrib-spec-list))
        (attrib-spec-list-collect-idents c$::attrib-spec-list)))

Theorem: init-declor-collect-idents-of-init-declor-fix-init-declor

(defthm init-declor-collect-idents-of-init-declor-fix-init-declor
  (equal (init-declor-collect-idents (init-declor-fix init-declor))
         (init-declor-collect-idents init-declor)))

Theorem: init-declor-list-collect-idents-of-init-declor-list-fix-init-declor-list

(defthm
 init-declor-list-collect-idents-of-init-declor-list-fix-init-declor-list
 (equal (init-declor-list-collect-idents
             (init-declor-list-fix c$::init-declor-list))
        (init-declor-list-collect-idents c$::init-declor-list)))

Theorem: declon-collect-idents-of-declon-fix-declon

(defthm declon-collect-idents-of-declon-fix-declon
  (equal (declon-collect-idents (declon-fix declon))
         (declon-collect-idents declon)))

Theorem: declon-list-collect-idents-of-declon-list-fix-declon-list

(defthm declon-list-collect-idents-of-declon-list-fix-declon-list
 (equal
  (declon-list-collect-idents (c$::declon-list-fix c$::declon-list))
  (declon-list-collect-idents c$::declon-list)))

Theorem: label-collect-idents-of-label-fix-label

(defthm label-collect-idents-of-label-fix-label
  (equal (label-collect-idents (label-fix c$::label))
         (label-collect-idents c$::label)))

Theorem: asm-output-collect-idents-of-asm-output-fix-asm-output

(defthm asm-output-collect-idents-of-asm-output-fix-asm-output
 (equal
     (asm-output-collect-idents (c$::asm-output-fix c$::asm-output))
     (asm-output-collect-idents c$::asm-output)))

Theorem: asm-output-list-collect-idents-of-asm-output-list-fix-asm-output-list

(defthm
 asm-output-list-collect-idents-of-asm-output-list-fix-asm-output-list
 (equal (asm-output-list-collect-idents
             (c$::asm-output-list-fix c$::asm-output-list))
        (asm-output-list-collect-idents c$::asm-output-list)))

Theorem: asm-input-collect-idents-of-asm-input-fix-asm-input

(defthm asm-input-collect-idents-of-asm-input-fix-asm-input
 (equal (asm-input-collect-idents (c$::asm-input-fix c$::asm-input))
        (asm-input-collect-idents c$::asm-input)))

Theorem: asm-input-list-collect-idents-of-asm-input-list-fix-asm-input-list

(defthm
 asm-input-list-collect-idents-of-asm-input-list-fix-asm-input-list
 (equal (asm-input-list-collect-idents
             (c$::asm-input-list-fix c$::asm-input-list))
        (asm-input-list-collect-idents c$::asm-input-list)))

Theorem: asm-stmt-collect-idents-of-asm-stmt-fix-asm-stmt

(defthm asm-stmt-collect-idents-of-asm-stmt-fix-asm-stmt
  (equal (asm-stmt-collect-idents (c$::asm-stmt-fix c$::asm-stmt))
         (asm-stmt-collect-idents c$::asm-stmt)))

Theorem: stmt-collect-idents-of-stmt-fix-stmt

(defthm stmt-collect-idents-of-stmt-fix-stmt
  (equal (stmt-collect-idents (stmt-fix c$::stmt))
         (stmt-collect-idents c$::stmt)))

Theorem: comp-stmt-collect-idents-of-comp-stmt-fix-comp-stmt

(defthm comp-stmt-collect-idents-of-comp-stmt-fix-comp-stmt
  (equal (comp-stmt-collect-idents (c$::comp-stmt-fix comp-stmt))
         (comp-stmt-collect-idents comp-stmt)))

Theorem: block-item-collect-idents-of-block-item-fix-block-item

(defthm block-item-collect-idents-of-block-item-fix-block-item
  (equal (block-item-collect-idents (block-item-fix c$::block-item))
         (block-item-collect-idents c$::block-item)))

Theorem: block-item-list-collect-idents-of-block-item-list-fix-block-item-list

(defthm
 block-item-list-collect-idents-of-block-item-list-fix-block-item-list
 (equal (block-item-list-collect-idents
             (block-item-list-fix c$::block-item-list))
        (block-item-list-collect-idents c$::block-item-list)))

Theorem: amb-expr/tyname-collect-idents-of-amb-expr/tyname-fix-amb-expr/tyname

(defthm
 amb-expr/tyname-collect-idents-of-amb-expr/tyname-fix-amb-expr/tyname
 (equal (amb-expr/tyname-collect-idents
             (c$::amb-expr/tyname-fix c$::amb-expr/tyname))
        (amb-expr/tyname-collect-idents c$::amb-expr/tyname)))

Theorem: amb-declor/absdeclor-collect-idents-of-amb-declor/absdeclor-fix-amb-declor/absdeclor

(defthm
 amb-declor/absdeclor-collect-idents-of-amb-declor/absdeclor-fix-amb-declor/absdeclor
 (equal
    (amb-declor/absdeclor-collect-idents
         (c$::amb-declor/absdeclor-fix c$::amb-declor/absdeclor))
    (amb-declor/absdeclor-collect-idents c$::amb-declor/absdeclor)))

Theorem: amb-declon/stmt-collect-idents-of-amb-declon/stmt-fix-amb-declon/stmt

(defthm
 amb-declon/stmt-collect-idents-of-amb-declon/stmt-fix-amb-declon/stmt
 (equal (amb-declon/stmt-collect-idents
             (c$::amb-declon/stmt-fix c$::amb-declon/stmt))
        (amb-declon/stmt-collect-idents c$::amb-declon/stmt)))

Theorem: expr-collect-idents-expr-equiv-congruence-on-expr

(defthm expr-collect-idents-expr-equiv-congruence-on-expr
  (implies (c$::expr-equiv c$::expr expr-equiv)
           (equal (expr-collect-idents c$::expr)
                  (expr-collect-idents expr-equiv)))
  :rule-classes :congruence)

Theorem: expr-list-collect-idents-expr-list-equiv-congruence-on-expr-list

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

Theorem: expr-option-collect-idents-expr-option-equiv-congruence-on-expr-option

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

Theorem: const-expr-collect-idents-const-expr-equiv-congruence-on-const-expr

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

Theorem: const-expr-option-collect-idents-const-expr-option-equiv-congruence-on-const-expr-option

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

Theorem: genassoc-collect-idents-genassoc-equiv-congruence-on-genassoc

(defthm
      genassoc-collect-idents-genassoc-equiv-congruence-on-genassoc
  (implies (c$::genassoc-equiv c$::genassoc genassoc-equiv)
           (equal (genassoc-collect-idents c$::genassoc)
                  (genassoc-collect-idents genassoc-equiv)))
  :rule-classes :congruence)

Theorem: genassoc-list-collect-idents-genassoc-list-equiv-congruence-on-genassoc-list

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

Theorem: member-designor-collect-idents-member-designor-equiv-congruence-on-member-designor

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

Theorem: type-spec-collect-idents-type-spec-equiv-congruence-on-type-spec

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

Theorem: spec/qual-collect-idents-spec/qual-equiv-congruence-on-spec/qual

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

Theorem: spec/qual-list-collect-idents-spec/qual-list-equiv-congruence-on-spec/qual-list

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

Theorem: align-spec-collect-idents-align-spec-equiv-congruence-on-align-spec

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

Theorem: decl-spec-collect-idents-decl-spec-equiv-congruence-on-decl-spec

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

Theorem: decl-spec-list-collect-idents-decl-spec-list-equiv-congruence-on-decl-spec-list

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

Theorem: typequal/attribspec-collect-idents-typequal/attribspec-equiv-congruence-on-typequal/attribspec

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

Theorem: typequal/attribspec-list-collect-idents-typequal/attribspec-list-equiv-congruence-on-typequal/attribspec-list

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

Theorem: typequal/attribspec-list-list-collect-idents-typequal/attribspec-list-list-equiv-congruence-on-typequal/attribspec-list-list

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

Theorem: initer-collect-idents-initer-equiv-congruence-on-initer

(defthm initer-collect-idents-initer-equiv-congruence-on-initer
  (implies (c$::initer-equiv c$::initer initer-equiv)
           (equal (initer-collect-idents c$::initer)
                  (initer-collect-idents initer-equiv)))
  :rule-classes :congruence)

Theorem: initer-option-collect-idents-initer-option-equiv-congruence-on-initer-option

(defthm
 initer-option-collect-idents-initer-option-equiv-congruence-on-initer-option
 (implies
     (c$::initer-option-equiv c$::initer-option initer-option-equiv)
     (equal (initer-option-collect-idents c$::initer-option)
            (initer-option-collect-idents initer-option-equiv)))
 :rule-classes :congruence)

Theorem: desiniter-collect-idents-desiniter-equiv-congruence-on-desiniter

(defthm
   desiniter-collect-idents-desiniter-equiv-congruence-on-desiniter
  (implies (c$::desiniter-equiv desiniter desiniter-equiv)
           (equal (desiniter-collect-idents desiniter)
                  (desiniter-collect-idents desiniter-equiv)))
  :rule-classes :congruence)

Theorem: desiniter-list-collect-idents-desiniter-list-equiv-congruence-on-desiniter-list

(defthm
 desiniter-list-collect-idents-desiniter-list-equiv-congruence-on-desiniter-list
 (implies
  (c$::desiniter-list-equiv c$::desiniter-list desiniter-list-equiv)
  (equal (desiniter-list-collect-idents c$::desiniter-list)
         (desiniter-list-collect-idents desiniter-list-equiv)))
 :rule-classes :congruence)

Theorem: designor-collect-idents-designor-equiv-congruence-on-designor

(defthm
      designor-collect-idents-designor-equiv-congruence-on-designor
  (implies (c$::designor-equiv c$::designor designor-equiv)
           (equal (designor-collect-idents c$::designor)
                  (designor-collect-idents designor-equiv)))
  :rule-classes :congruence)

Theorem: designor-list-collect-idents-designor-list-equiv-congruence-on-designor-list

(defthm
 designor-list-collect-idents-designor-list-equiv-congruence-on-designor-list
 (implies
     (c$::designor-list-equiv c$::designor-list designor-list-equiv)
     (equal (designor-list-collect-idents c$::designor-list)
            (designor-list-collect-idents designor-list-equiv)))
 :rule-classes :congruence)

Theorem: declor-collect-idents-declor-equiv-congruence-on-declor

(defthm declor-collect-idents-declor-equiv-congruence-on-declor
  (implies (c$::declor-equiv declor declor-equiv)
           (equal (declor-collect-idents declor)
                  (declor-collect-idents declor-equiv)))
  :rule-classes :congruence)

Theorem: declor-option-collect-idents-declor-option-equiv-congruence-on-declor-option

(defthm
 declor-option-collect-idents-declor-option-equiv-congruence-on-declor-option
 (implies
     (c$::declor-option-equiv c$::declor-option declor-option-equiv)
     (equal (declor-option-collect-idents c$::declor-option)
            (declor-option-collect-idents declor-option-equiv)))
 :rule-classes :congruence)

Theorem: dirdeclor-collect-idents-dirdeclor-equiv-congruence-on-dirdeclor

(defthm
   dirdeclor-collect-idents-dirdeclor-equiv-congruence-on-dirdeclor
  (implies (c$::dirdeclor-equiv dirdeclor dirdeclor-equiv)
           (equal (dirdeclor-collect-idents dirdeclor)
                  (dirdeclor-collect-idents dirdeclor-equiv)))
  :rule-classes :congruence)

Theorem: absdeclor-collect-idents-absdeclor-equiv-congruence-on-absdeclor

(defthm
   absdeclor-collect-idents-absdeclor-equiv-congruence-on-absdeclor
  (implies (c$::absdeclor-equiv absdeclor absdeclor-equiv)
           (equal (absdeclor-collect-idents absdeclor)
                  (absdeclor-collect-idents absdeclor-equiv)))
  :rule-classes :congruence)

Theorem: absdeclor-option-collect-idents-absdeclor-option-equiv-congruence-on-absdeclor-option

(defthm
 absdeclor-option-collect-idents-absdeclor-option-equiv-congruence-on-absdeclor-option
 (implies
   (c$::absdeclor-option-equiv c$::absdeclor-option
                               absdeclor-option-equiv)
   (equal (absdeclor-option-collect-idents c$::absdeclor-option)
          (absdeclor-option-collect-idents absdeclor-option-equiv)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-collect-idents-dirabsdeclor-equiv-congruence-on-dirabsdeclor

(defthm
 dirabsdeclor-collect-idents-dirabsdeclor-equiv-congruence-on-dirabsdeclor
 (implies
      (c$::dirabsdeclor-equiv c$::dirabsdeclor dirabsdeclor-equiv)
      (equal (dirabsdeclor-collect-idents c$::dirabsdeclor)
             (dirabsdeclor-collect-idents dirabsdeclor-equiv)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-option-collect-idents-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor-option

(defthm
 dirabsdeclor-option-collect-idents-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor-option
 (implies
  (c$::dirabsdeclor-option-equiv c$::dirabsdeclor-option
                                 dirabsdeclor-option-equiv)
  (equal
    (dirabsdeclor-option-collect-idents c$::dirabsdeclor-option)
    (dirabsdeclor-option-collect-idents dirabsdeclor-option-equiv)))
 :rule-classes :congruence)

Theorem: param-declon-collect-idents-param-declon-equiv-congruence-on-param-declon

(defthm
 param-declon-collect-idents-param-declon-equiv-congruence-on-param-declon
 (implies (c$::param-declon-equiv param-declon param-declon-equiv)
          (equal (param-declon-collect-idents param-declon)
                 (param-declon-collect-idents param-declon-equiv)))
 :rule-classes :congruence)

Theorem: param-declon-list-collect-idents-param-declon-list-equiv-congruence-on-param-declon-list

(defthm
 param-declon-list-collect-idents-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-collect-idents c$::param-declon-list)
        (param-declon-list-collect-idents param-declon-list-equiv)))
 :rule-classes :congruence)

Theorem: param-declor-collect-idents-param-declor-equiv-congruence-on-param-declor

(defthm
 param-declor-collect-idents-param-declor-equiv-congruence-on-param-declor
 (implies
      (c$::param-declor-equiv c$::param-declor param-declor-equiv)
      (equal (param-declor-collect-idents c$::param-declor)
             (param-declor-collect-idents param-declor-equiv)))
 :rule-classes :congruence)

Theorem: tyname-collect-idents-tyname-equiv-congruence-on-tyname

(defthm tyname-collect-idents-tyname-equiv-congruence-on-tyname
  (implies (c$::tyname-equiv tyname tyname-equiv)
           (equal (tyname-collect-idents tyname)
                  (tyname-collect-idents tyname-equiv)))
  :rule-classes :congruence)

Theorem: struni-spec-collect-idents-struni-spec-equiv-congruence-on-struni-spec

(defthm
 struni-spec-collect-idents-struni-spec-equiv-congruence-on-struni-spec
 (implies (c$::struni-spec-equiv struni-spec struni-spec-equiv)
          (equal (struni-spec-collect-idents struni-spec)
                 (struni-spec-collect-idents struni-spec-equiv)))
 :rule-classes :congruence)

Theorem: struct-declon-collect-idents-struct-declon-equiv-congruence-on-struct-declon

(defthm
 struct-declon-collect-idents-struct-declon-equiv-congruence-on-struct-declon
 (implies
     (c$::struct-declon-equiv c$::struct-declon struct-declon-equiv)
     (equal (struct-declon-collect-idents c$::struct-declon)
            (struct-declon-collect-idents struct-declon-equiv)))
 :rule-classes :congruence)

Theorem: struct-declon-list-collect-idents-struct-declon-list-equiv-congruence-on-struct-declon-list

(defthm
 struct-declon-list-collect-idents-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-collect-idents c$::struct-declon-list)
      (struct-declon-list-collect-idents struct-declon-list-equiv)))
 :rule-classes :congruence)

Theorem: struct-declor-collect-idents-struct-declor-equiv-congruence-on-struct-declor

(defthm
 struct-declor-collect-idents-struct-declor-equiv-congruence-on-struct-declor
 (implies
      (c$::struct-declor-equiv struct-declor struct-declor-equiv)
      (equal (struct-declor-collect-idents struct-declor)
             (struct-declor-collect-idents struct-declor-equiv)))
 :rule-classes :congruence)

Theorem: struct-declor-list-collect-idents-struct-declor-list-equiv-congruence-on-struct-declor-list

(defthm
 struct-declor-list-collect-idents-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-collect-idents c$::struct-declor-list)
      (struct-declor-list-collect-idents struct-declor-list-equiv)))
 :rule-classes :congruence)

Theorem: enum-spec-collect-idents-enum-spec-equiv-congruence-on-enum-spec

(defthm
   enum-spec-collect-idents-enum-spec-equiv-congruence-on-enum-spec
  (implies (c$::enum-spec-equiv enum-spec enum-spec-equiv)
           (equal (enum-spec-collect-idents enum-spec)
                  (enum-spec-collect-idents enum-spec-equiv)))
  :rule-classes :congruence)

Theorem: enumer-collect-idents-enumer-equiv-congruence-on-enumer

(defthm enumer-collect-idents-enumer-equiv-congruence-on-enumer
  (implies (c$::enumer-equiv enumer enumer-equiv)
           (equal (enumer-collect-idents enumer)
                  (enumer-collect-idents enumer-equiv)))
  :rule-classes :congruence)

Theorem: enumer-list-collect-idents-enumer-list-equiv-congruence-on-enumer-list

(defthm
 enumer-list-collect-idents-enumer-list-equiv-congruence-on-enumer-list
 (implies (c$::enumer-list-equiv c$::enumer-list enumer-list-equiv)
          (equal (enumer-list-collect-idents c$::enumer-list)
                 (enumer-list-collect-idents enumer-list-equiv)))
 :rule-classes :congruence)

Theorem: statassert-collect-idents-statassert-equiv-congruence-on-statassert

(defthm
 statassert-collect-idents-statassert-equiv-congruence-on-statassert
 (implies (c$::statassert-equiv statassert statassert-equiv)
          (equal (statassert-collect-idents statassert)
                 (statassert-collect-idents statassert-equiv)))
 :rule-classes :congruence)

Theorem: attrib-collect-idents-attrib-equiv-congruence-on-attrib

(defthm attrib-collect-idents-attrib-equiv-congruence-on-attrib
  (implies (c$::attrib-equiv c$::attrib attrib-equiv)
           (equal (attrib-collect-idents c$::attrib)
                  (attrib-collect-idents attrib-equiv)))
  :rule-classes :congruence)

Theorem: attrib-list-collect-idents-attrib-list-equiv-congruence-on-attrib-list

(defthm
 attrib-list-collect-idents-attrib-list-equiv-congruence-on-attrib-list
 (implies (c$::attrib-list-equiv c$::attrib-list attrib-list-equiv)
          (equal (attrib-list-collect-idents c$::attrib-list)
                 (attrib-list-collect-idents attrib-list-equiv)))
 :rule-classes :congruence)

Theorem: attrib-spec-collect-idents-attrib-spec-equiv-congruence-on-attrib-spec

(defthm
 attrib-spec-collect-idents-attrib-spec-equiv-congruence-on-attrib-spec
 (implies (c$::attrib-spec-equiv c$::attrib-spec attrib-spec-equiv)
          (equal (attrib-spec-collect-idents c$::attrib-spec)
                 (attrib-spec-collect-idents attrib-spec-equiv)))
 :rule-classes :congruence)

Theorem: attrib-spec-list-collect-idents-attrib-spec-list-equiv-congruence-on-attrib-spec-list

(defthm
 attrib-spec-list-collect-idents-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-collect-idents c$::attrib-spec-list)
          (attrib-spec-list-collect-idents attrib-spec-list-equiv)))
 :rule-classes :congruence)

Theorem: init-declor-collect-idents-init-declor-equiv-congruence-on-init-declor

(defthm
 init-declor-collect-idents-init-declor-equiv-congruence-on-init-declor
 (implies (c$::init-declor-equiv init-declor init-declor-equiv)
          (equal (init-declor-collect-idents init-declor)
                 (init-declor-collect-idents init-declor-equiv)))
 :rule-classes :congruence)

Theorem: init-declor-list-collect-idents-init-declor-list-equiv-congruence-on-init-declor-list

(defthm
 init-declor-list-collect-idents-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-collect-idents c$::init-declor-list)
          (init-declor-list-collect-idents init-declor-list-equiv)))
 :rule-classes :congruence)

Theorem: declon-collect-idents-declon-equiv-congruence-on-declon

(defthm declon-collect-idents-declon-equiv-congruence-on-declon
  (implies (c$::declon-equiv declon declon-equiv)
           (equal (declon-collect-idents declon)
                  (declon-collect-idents declon-equiv)))
  :rule-classes :congruence)

Theorem: declon-list-collect-idents-declon-list-equiv-congruence-on-declon-list

(defthm
 declon-list-collect-idents-declon-list-equiv-congruence-on-declon-list
 (implies (c$::declon-list-equiv c$::declon-list declon-list-equiv)
          (equal (declon-list-collect-idents c$::declon-list)
                 (declon-list-collect-idents declon-list-equiv)))
 :rule-classes :congruence)

Theorem: label-collect-idents-label-equiv-congruence-on-label

(defthm label-collect-idents-label-equiv-congruence-on-label
  (implies (c$::label-equiv c$::label label-equiv)
           (equal (label-collect-idents c$::label)
                  (label-collect-idents label-equiv)))
  :rule-classes :congruence)

Theorem: asm-output-collect-idents-asm-output-equiv-congruence-on-asm-output

(defthm
 asm-output-collect-idents-asm-output-equiv-congruence-on-asm-output
 (implies (c$::asm-output-equiv c$::asm-output asm-output-equiv)
          (equal (asm-output-collect-idents c$::asm-output)
                 (asm-output-collect-idents asm-output-equiv)))
 :rule-classes :congruence)

Theorem: asm-output-list-collect-idents-asm-output-list-equiv-congruence-on-asm-output-list

(defthm
 asm-output-list-collect-idents-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-collect-idents c$::asm-output-list)
            (asm-output-list-collect-idents asm-output-list-equiv)))
 :rule-classes :congruence)

Theorem: asm-input-collect-idents-asm-input-equiv-congruence-on-asm-input

(defthm
   asm-input-collect-idents-asm-input-equiv-congruence-on-asm-input
  (implies (c$::asm-input-equiv c$::asm-input asm-input-equiv)
           (equal (asm-input-collect-idents c$::asm-input)
                  (asm-input-collect-idents asm-input-equiv)))
  :rule-classes :congruence)

Theorem: asm-input-list-collect-idents-asm-input-list-equiv-congruence-on-asm-input-list

(defthm
 asm-input-list-collect-idents-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-collect-idents c$::asm-input-list)
         (asm-input-list-collect-idents asm-input-list-equiv)))
 :rule-classes :congruence)

Theorem: asm-stmt-collect-idents-asm-stmt-equiv-congruence-on-asm-stmt

(defthm
      asm-stmt-collect-idents-asm-stmt-equiv-congruence-on-asm-stmt
  (implies (c$::asm-stmt-equiv c$::asm-stmt asm-stmt-equiv)
           (equal (asm-stmt-collect-idents c$::asm-stmt)
                  (asm-stmt-collect-idents asm-stmt-equiv)))
  :rule-classes :congruence)

Theorem: stmt-collect-idents-stmt-equiv-congruence-on-stmt

(defthm stmt-collect-idents-stmt-equiv-congruence-on-stmt
  (implies (c$::stmt-equiv c$::stmt stmt-equiv)
           (equal (stmt-collect-idents c$::stmt)
                  (stmt-collect-idents stmt-equiv)))
  :rule-classes :congruence)

Theorem: comp-stmt-collect-idents-comp-stmt-equiv-congruence-on-comp-stmt

(defthm
   comp-stmt-collect-idents-comp-stmt-equiv-congruence-on-comp-stmt
  (implies (c$::comp-stmt-equiv comp-stmt comp-stmt-equiv)
           (equal (comp-stmt-collect-idents comp-stmt)
                  (comp-stmt-collect-idents comp-stmt-equiv)))
  :rule-classes :congruence)

Theorem: block-item-collect-idents-block-item-equiv-congruence-on-block-item

(defthm
 block-item-collect-idents-block-item-equiv-congruence-on-block-item
 (implies (c$::block-item-equiv c$::block-item block-item-equiv)
          (equal (block-item-collect-idents c$::block-item)
                 (block-item-collect-idents block-item-equiv)))
 :rule-classes :congruence)

Theorem: block-item-list-collect-idents-block-item-list-equiv-congruence-on-block-item-list

(defthm
 block-item-list-collect-idents-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-collect-idents c$::block-item-list)
            (block-item-list-collect-idents block-item-list-equiv)))
 :rule-classes :congruence)

Theorem: amb-expr/tyname-collect-idents-amb-expr/tyname-equiv-congruence-on-amb-expr/tyname

(defthm
 amb-expr/tyname-collect-idents-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-collect-idents c$::amb-expr/tyname)
            (amb-expr/tyname-collect-idents amb-expr/tyname-equiv)))
 :rule-classes :congruence)

Theorem: amb-declor/absdeclor-collect-idents-amb-declor/absdeclor-equiv-congruence-on-amb-declor/absdeclor

(defthm
 amb-declor/absdeclor-collect-idents-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-collect-idents c$::amb-declor/absdeclor)
      (amb-declor/absdeclor-collect-idents
           amb-declor/absdeclor-equiv)))
 :rule-classes :congruence)

Theorem: amb-declon/stmt-collect-idents-amb-declon/stmt-equiv-congruence-on-amb-declon/stmt

(defthm
 amb-declon/stmt-collect-idents-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-collect-idents c$::amb-declon/stmt)
            (amb-declon/stmt-collect-idents amb-declon/stmt-equiv)))
 :rule-classes :congruence)