		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-aidentp

Exprs/decls/stmts-aidentp

Definitions and Theorems

Function: expr-aidentp

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

Function: expr-list-aidentp

(defun expr-list-aidentp (expr-list gcc)
  (declare (xargs :guard (and (expr-listp expr-list)
                              (booleanp gcc))))
  (let ((__function__ 'expr-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp expr-list) t)
          (t (and (expr-aidentp (car expr-list) gcc)
                  (expr-list-aidentp (cdr expr-list)
                                     gcc))))))

Function: expr-option-aidentp

(defun expr-option-aidentp (expr-option gcc)
  (declare (xargs :guard (and (expr-optionp expr-option)
                              (booleanp gcc))))
  (let ((__function__ 'expr-option-aidentp))
    (declare (ignorable __function__))
    (expr-option-case
         expr-option
         :some (expr-aidentp (expr-option-some->val expr-option)
                             gcc)
         :none t)))

Function: const-expr-aidentp

(defun const-expr-aidentp (const-expr gcc)
  (declare (xargs :guard (and (const-exprp const-expr)
                              (booleanp gcc))))
  (declare (ignorable const-expr))
  (let ((__function__ 'const-expr-aidentp))
    (declare (ignorable __function__))
    (expr-aidentp (const-expr->expr const-expr)
                  gcc)))

Function: const-expr-option-aidentp

(defun const-expr-option-aidentp (const-expr-option gcc)
  (declare (xargs :guard (and (const-expr-optionp const-expr-option)
                              (booleanp gcc))))
  (let ((__function__ 'const-expr-option-aidentp))
    (declare (ignorable __function__))
    (const-expr-option-case
         const-expr-option
         :some (const-expr-aidentp
                    (const-expr-option-some->val const-expr-option)
                    gcc)
         :none t)))

Function: genassoc-aidentp

(defun genassoc-aidentp (genassoc gcc)
  (declare (xargs :guard (and (genassocp genassoc)
                              (booleanp gcc))))
  (declare (ignorable genassoc))
  (let ((__function__ 'genassoc-aidentp))
    (declare (ignorable __function__))
    (genassoc-case
         genassoc
         :type (and (tyname-aidentp (genassoc-type->type genassoc)
                                    gcc)
                    (expr-aidentp (genassoc-type->expr genassoc)
                                  gcc))
         :default (expr-aidentp (genassoc-default->expr genassoc)
                                gcc))))

Function: genassoc-list-aidentp

(defun genassoc-list-aidentp (genassoc-list gcc)
  (declare (xargs :guard (and (genassoc-listp genassoc-list)
                              (booleanp gcc))))
  (let ((__function__ 'genassoc-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp genassoc-list) t)
          (t (and (genassoc-aidentp (car genassoc-list)
                                    gcc)
                  (genassoc-list-aidentp (cdr genassoc-list)
                                         gcc))))))

Function: member-designor-aidentp

(defun member-designor-aidentp (member-designor gcc)
 (declare (xargs :guard (and (member-designorp member-designor)
                             (booleanp gcc))))
 (declare (ignorable member-designor))
 (let ((__function__ 'member-designor-aidentp))
  (declare (ignorable __function__))
  (member-designor-case
     member-designor
     :ident
     (ident-aidentp (member-designor-ident->ident member-designor)
                    gcc)
     :dot
     (and (member-designor-aidentp
               (member-designor-dot->member member-designor)
               gcc)
          (ident-aidentp (member-designor-dot->name member-designor)
                         gcc))
     :sub
     (and (member-designor-aidentp
               (member-designor-sub->member member-designor)
               gcc)
          (expr-aidentp (member-designor-sub->index member-designor)
                        gcc)))))

Function: type-spec-aidentp

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

Function: spec/qual-aidentp

(defun spec/qual-aidentp (spec/qual gcc)
 (declare (xargs :guard (and (spec/qual-p spec/qual)
                             (booleanp gcc))))
 (declare (ignorable spec/qual))
 (let ((__function__ 'spec/qual-aidentp))
  (declare (ignorable __function__))
  (spec/qual-case
   spec/qual
   :typespec (type-spec-aidentp (spec/qual-typespec->spec spec/qual)
                                gcc)
   :typequal t
   :align (align-spec-aidentp (spec/qual-align->spec spec/qual)
                              gcc)
   :attrib (attrib-spec-aidentp (spec/qual-attrib->spec spec/qual)
                                gcc))))

Function: spec/qual-list-aidentp

(defun spec/qual-list-aidentp (spec/qual-list gcc)
  (declare (xargs :guard (and (spec/qual-listp spec/qual-list)
                              (booleanp gcc))))
  (let ((__function__ 'spec/qual-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp spec/qual-list) t)
          (t (and (spec/qual-aidentp (car spec/qual-list)
                                     gcc)
                  (spec/qual-list-aidentp (cdr spec/qual-list)
                                          gcc))))))

Function: align-spec-aidentp

(defun align-spec-aidentp (align-spec gcc)
 (declare (xargs :guard (and (align-specp align-spec)
                             (booleanp gcc))))
 (declare (ignorable align-spec))
 (let ((__function__ 'align-spec-aidentp))
  (declare (ignorable __function__))
  (align-spec-case
      align-spec
      :alignas-type
      (tyname-aidentp (align-spec-alignas-type->type align-spec)
                      gcc)
      :alignas-expr
      (const-expr-aidentp (align-spec-alignas-expr->expr align-spec)
                          gcc)
      :alignas-ambig
      (amb-expr/tyname-aidentp
           (align-spec-alignas-ambig->expr/type align-spec)
           gcc))))

Function: decl-spec-aidentp

(defun decl-spec-aidentp (decl-spec gcc)
 (declare (xargs :guard (and (decl-specp decl-spec)
                             (booleanp gcc))))
 (declare (ignorable decl-spec))
 (let ((__function__ 'decl-spec-aidentp))
  (declare (ignorable __function__))
  (decl-spec-case
   decl-spec
   :stoclass t
   :typespec (type-spec-aidentp (decl-spec-typespec->spec decl-spec)
                                gcc)
   :typequal t
   :function t
   :align (align-spec-aidentp (decl-spec-align->spec decl-spec)
                              gcc)
   :attrib (attrib-spec-aidentp (decl-spec-attrib->spec decl-spec)
                                gcc)
   :stdcall t
   :declspec (ident-aidentp (decl-spec-declspec->arg decl-spec)
                            gcc))))

Function: decl-spec-list-aidentp

(defun decl-spec-list-aidentp (decl-spec-list gcc)
  (declare (xargs :guard (and (decl-spec-listp decl-spec-list)
                              (booleanp gcc))))
  (let ((__function__ 'decl-spec-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp decl-spec-list) t)
          (t (and (decl-spec-aidentp (car decl-spec-list)
                                     gcc)
                  (decl-spec-list-aidentp (cdr decl-spec-list)
                                          gcc))))))

Function: typequal/attribspec-aidentp

(defun typequal/attribspec-aidentp (typequal/attribspec gcc)
 (declare
      (xargs :guard (and (typequal/attribspec-p typequal/attribspec)
                         (booleanp gcc))))
 (declare (ignorable typequal/attribspec))
 (let ((__function__ 'typequal/attribspec-aidentp))
   (declare (ignorable __function__))
   (typequal/attribspec-case
        typequal/attribspec
        :type t
        :attrib
        (attrib-spec-aidentp
             (typequal/attribspec-attrib->spec typequal/attribspec)
             gcc))))

Function: typequal/attribspec-list-aidentp

(defun typequal/attribspec-list-aidentp
       (typequal/attribspec-list gcc)
 (declare
  (xargs
    :guard (and (typequal/attribspec-listp typequal/attribspec-list)
                (booleanp gcc))))
 (let ((__function__ 'typequal/attribspec-list-aidentp))
  (declare (ignorable __function__))
  (cond
   ((endp typequal/attribspec-list) t)
   (t
    (and (typequal/attribspec-aidentp (car typequal/attribspec-list)
                                      gcc)
         (typequal/attribspec-list-aidentp
              (cdr typequal/attribspec-list)
              gcc))))))

Function: typequal/attribspec-list-list-aidentp

(defun typequal/attribspec-list-list-aidentp
       (typequal/attribspec-list-list gcc)
 (declare
  (xargs
   :guard
   (and
      (typequal/attribspec-list-listp typequal/attribspec-list-list)
      (booleanp gcc))))
 (let ((__function__ 'typequal/attribspec-list-list-aidentp))
   (declare (ignorable __function__))
   (cond ((endp typequal/attribspec-list-list) t)
         (t (and (typequal/attribspec-list-aidentp
                      (car typequal/attribspec-list-list)
                      gcc)
                 (typequal/attribspec-list-list-aidentp
                      (cdr typequal/attribspec-list-list)
                      gcc))))))

Function: initer-aidentp

(defun initer-aidentp (initer gcc)
  (declare (xargs :guard (and (initerp initer) (booleanp gcc))))
  (declare (ignorable initer))
  (let ((__function__ 'initer-aidentp))
    (declare (ignorable __function__))
    (initer-case
         initer
         :single (expr-aidentp (initer-single->expr initer)
                               gcc)
         :list (desiniter-list-aidentp (initer-list->elems initer)
                                       gcc))))

Function: initer-option-aidentp

(defun initer-option-aidentp (initer-option gcc)
 (declare (xargs :guard (and (initer-optionp initer-option)
                             (booleanp gcc))))
 (let ((__function__ 'initer-option-aidentp))
  (declare (ignorable __function__))
  (initer-option-case
       initer-option
       :some (initer-aidentp (initer-option-some->val initer-option)
                             gcc)
       :none t)))

Function: desiniter-aidentp

(defun desiniter-aidentp (desiniter gcc)
  (declare (xargs :guard (and (desiniterp desiniter)
                              (booleanp gcc))))
  (declare (ignorable desiniter))
  (let ((__function__ 'desiniter-aidentp))
    (declare (ignorable __function__))
    (and (designor-list-aidentp (desiniter->designors desiniter)
                                gcc)
         (initer-aidentp (desiniter->initer desiniter)
                         gcc))))

Function: desiniter-list-aidentp

(defun desiniter-list-aidentp (desiniter-list gcc)
  (declare (xargs :guard (and (desiniter-listp desiniter-list)
                              (booleanp gcc))))
  (let ((__function__ 'desiniter-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp desiniter-list) t)
          (t (and (desiniter-aidentp (car desiniter-list)
                                     gcc)
                  (desiniter-list-aidentp (cdr desiniter-list)
                                          gcc))))))

Function: designor-aidentp

(defun designor-aidentp (designor gcc)
 (declare (xargs :guard (and (designorp designor)
                             (booleanp gcc))))
 (declare (ignorable designor))
 (let ((__function__ 'designor-aidentp))
  (declare (ignorable __function__))
  (designor-case
     designor
     :sub
     (and (const-expr-aidentp (designor-sub->index designor)
                              gcc)
          (const-expr-option-aidentp (designor-sub->range? designor)
                                     gcc))
     :dot (ident-aidentp (designor-dot->name designor)
                         gcc))))

Function: designor-list-aidentp

(defun designor-list-aidentp (designor-list gcc)
  (declare (xargs :guard (and (designor-listp designor-list)
                              (booleanp gcc))))
  (let ((__function__ 'designor-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp designor-list) t)
          (t (and (designor-aidentp (car designor-list)
                                    gcc)
                  (designor-list-aidentp (cdr designor-list)
                                         gcc))))))

Function: declor-aidentp

(defun declor-aidentp (declor gcc)
 (declare (xargs :guard (and (declorp declor) (booleanp gcc))))
 (declare (ignorable declor))
 (let ((__function__ 'declor-aidentp))
  (declare (ignorable __function__))
  (and
    (typequal/attribspec-list-list-aidentp (declor->pointers declor)
                                           gcc)
    (dirdeclor-aidentp (declor->direct declor)
                       gcc))))

Function: declor-option-aidentp

(defun declor-option-aidentp (declor-option gcc)
 (declare (xargs :guard (and (declor-optionp declor-option)
                             (booleanp gcc))))
 (let ((__function__ 'declor-option-aidentp))
  (declare (ignorable __function__))
  (declor-option-case
       declor-option
       :some (declor-aidentp (declor-option-some->val declor-option)
                             gcc)
       :none t)))

Function: dirdeclor-aidentp

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

Function: absdeclor-aidentp

(defun absdeclor-aidentp (absdeclor gcc)
  (declare (xargs :guard (and (absdeclorp absdeclor)
                              (booleanp gcc))))
  (declare (ignorable absdeclor))
  (let ((__function__ 'absdeclor-aidentp))
    (declare (ignorable __function__))
    (and (typequal/attribspec-list-list-aidentp
              (absdeclor->pointers absdeclor)
              gcc)
         (dirabsdeclor-option-aidentp (absdeclor->direct? absdeclor)
                                      gcc))))

Function: absdeclor-option-aidentp

(defun absdeclor-option-aidentp (absdeclor-option gcc)
 (declare (xargs :guard (and (absdeclor-optionp absdeclor-option)
                             (booleanp gcc))))
 (let ((__function__ 'absdeclor-option-aidentp))
  (declare (ignorable __function__))
  (absdeclor-option-case
    absdeclor-option
    :some
    (absdeclor-aidentp (absdeclor-option-some->val absdeclor-option)
                       gcc)
    :none t)))

Function: dirabsdeclor-aidentp

(defun dirabsdeclor-aidentp (dirabsdeclor gcc)
 (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor)
                             (booleanp gcc))))
 (declare (ignorable dirabsdeclor))
 (let ((__function__ 'dirabsdeclor-aidentp))
  (declare (ignorable __function__))
  (dirabsdeclor-case
   dirabsdeclor
   :dummy-base t
   :paren
   (absdeclor-aidentp (dirabsdeclor-paren->inner dirabsdeclor)
                      gcc)
   :array
   (and
    (dirabsdeclor-option-aidentp
         (dirabsdeclor-array->declor? dirabsdeclor)
         gcc)
    (and
       (typequal/attribspec-list-aidentp
            (dirabsdeclor-array->qualspecs dirabsdeclor)
            gcc)
       (expr-option-aidentp (dirabsdeclor-array->size? dirabsdeclor)
                            gcc)))
   :array-static1
   (and
    (dirabsdeclor-option-aidentp
         (dirabsdeclor-array-static1->declor? dirabsdeclor)
         gcc)
    (and
       (typequal/attribspec-list-aidentp
            (dirabsdeclor-array-static1->qualspecs dirabsdeclor)
            gcc)
       (expr-aidentp (dirabsdeclor-array-static1->size dirabsdeclor)
                     gcc)))
   :array-static2
   (and
    (dirabsdeclor-option-aidentp
         (dirabsdeclor-array-static2->declor? dirabsdeclor)
         gcc)
    (and
       (typequal/attribspec-list-aidentp
            (dirabsdeclor-array-static2->qualspecs dirabsdeclor)
            gcc)
       (expr-aidentp (dirabsdeclor-array-static2->size dirabsdeclor)
                     gcc)))
   :array-star (dirabsdeclor-option-aidentp
                    (dirabsdeclor-array-star->declor? dirabsdeclor)
                    gcc)
   :function (and (dirabsdeclor-option-aidentp
                       (dirabsdeclor-function->declor? dirabsdeclor)
                       gcc)
                  (param-declon-list-aidentp
                       (dirabsdeclor-function->params dirabsdeclor)
                       gcc)))))

Function: dirabsdeclor-option-aidentp

(defun dirabsdeclor-option-aidentp (dirabsdeclor-option gcc)
 (declare
      (xargs :guard (and (dirabsdeclor-optionp dirabsdeclor-option)
                         (booleanp gcc))))
 (let ((__function__ 'dirabsdeclor-option-aidentp))
  (declare (ignorable __function__))
  (dirabsdeclor-option-case
      dirabsdeclor-option
      :some (dirabsdeclor-aidentp
                 (dirabsdeclor-option-some->val dirabsdeclor-option)
                 gcc)
      :none t)))

Function: param-declon-aidentp

(defun param-declon-aidentp (param-declon gcc)
 (declare (xargs :guard (and (param-declonp param-declon)
                             (booleanp gcc))))
 (declare (ignorable param-declon))
 (let ((__function__ 'param-declon-aidentp))
  (declare (ignorable __function__))
  (and
   (decl-spec-list-aidentp (param-declon->specs param-declon)
                           gcc)
   (and
      (param-declor-aidentp (param-declon->declor param-declon)
                            gcc)
      (attrib-spec-list-aidentp (param-declon->attribs param-declon)
                                gcc)))))

Function: param-declon-list-aidentp

(defun param-declon-list-aidentp (param-declon-list gcc)
  (declare (xargs :guard (and (param-declon-listp param-declon-list)
                              (booleanp gcc))))
  (let ((__function__ 'param-declon-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp param-declon-list) t)
          (t (and (param-declon-aidentp (car param-declon-list)
                                        gcc)
                  (param-declon-list-aidentp (cdr param-declon-list)
                                             gcc))))))

Function: param-declor-aidentp

(defun param-declor-aidentp (param-declor gcc)
 (declare (xargs :guard (and (param-declorp param-declor)
                             (booleanp gcc))))
 (declare (ignorable param-declor))
 (let ((__function__ 'param-declor-aidentp))
  (declare (ignorable __function__))
  (param-declor-case
     param-declor
     :nonabstract
     (declor-aidentp (param-declor-nonabstract->declor param-declor)
                     gcc)
     :abstract
     (absdeclor-aidentp (param-declor-abstract->declor param-declor)
                        gcc)
     :none t
     :ambig (amb-declor/absdeclor-aidentp
                 (param-declor-ambig->declor param-declor)
                 gcc))))

Function: tyname-aidentp

(defun tyname-aidentp (tyname gcc)
  (declare (xargs :guard (and (tynamep tyname) (booleanp gcc))))
  (declare (ignorable tyname))
  (let ((__function__ 'tyname-aidentp))
    (declare (ignorable __function__))
    (and (spec/qual-list-aidentp (tyname->specquals tyname)
                                 gcc)
         (absdeclor-option-aidentp (tyname->declor? tyname)
                                   gcc))))

Function: struni-spec-aidentp

(defun struni-spec-aidentp (struni-spec gcc)
 (declare (xargs :guard (and (struni-specp struni-spec)
                             (booleanp gcc))))
 (declare (ignorable struni-spec))
 (let ((__function__ 'struni-spec-aidentp))
  (declare (ignorable __function__))
  (and
   (attrib-spec-list-aidentp (struni-spec->attribs struni-spec)
                             gcc)
   (and
      (ident-option-aidentp (struni-spec->name? struni-spec)
                            gcc)
      (struct-declon-list-aidentp (struni-spec->members struni-spec)
                                  gcc)))))

Function: struct-declon-aidentp

(defun struct-declon-aidentp (struct-declon gcc)
 (declare (xargs :guard (and (struct-declonp struct-declon)
                             (booleanp gcc))))
 (declare (ignorable struct-declon))
 (let ((__function__ 'struct-declon-aidentp))
   (declare (ignorable __function__))
   (struct-declon-case
        struct-declon
        :member
        (and (spec/qual-list-aidentp
                  (struct-declon-member->specquals struct-declon)
                  gcc)
             (and (struct-declor-list-aidentp
                       (struct-declon-member->declors struct-declon)
                       gcc)
                  (attrib-spec-list-aidentp
                       (struct-declon-member->attribs struct-declon)
                       gcc)))
        :statassert
        (statassert-aidentp
             (struct-declon-statassert->statassert struct-declon)
             gcc)
        :empty t)))

Function: struct-declon-list-aidentp

(defun struct-declon-list-aidentp (struct-declon-list gcc)
 (declare
      (xargs :guard (and (struct-declon-listp struct-declon-list)
                         (booleanp gcc))))
 (let ((__function__ 'struct-declon-list-aidentp))
  (declare (ignorable __function__))
  (cond ((endp struct-declon-list) t)
        (t (and (struct-declon-aidentp (car struct-declon-list)
                                       gcc)
                (struct-declon-list-aidentp (cdr struct-declon-list)
                                            gcc))))))

Function: struct-declor-aidentp

(defun struct-declor-aidentp (struct-declor gcc)
 (declare (xargs :guard (and (struct-declorp struct-declor)
                             (booleanp gcc))))
 (declare (ignorable struct-declor))
 (let ((__function__ 'struct-declor-aidentp))
  (declare (ignorable __function__))
  (and
     (declor-option-aidentp (struct-declor->declor? struct-declor)
                            gcc)
     (const-expr-option-aidentp (struct-declor->expr? struct-declor)
                                gcc))))

Function: struct-declor-list-aidentp

(defun struct-declor-list-aidentp (struct-declor-list gcc)
 (declare
      (xargs :guard (and (struct-declor-listp struct-declor-list)
                         (booleanp gcc))))
 (let ((__function__ 'struct-declor-list-aidentp))
  (declare (ignorable __function__))
  (cond ((endp struct-declor-list) t)
        (t (and (struct-declor-aidentp (car struct-declor-list)
                                       gcc)
                (struct-declor-list-aidentp (cdr struct-declor-list)
                                            gcc))))))

Function: enum-spec-aidentp

(defun enum-spec-aidentp (enum-spec gcc)
  (declare (xargs :guard (and (enum-specp enum-spec)
                              (booleanp gcc))))
  (declare (ignorable enum-spec))
  (let ((__function__ 'enum-spec-aidentp))
    (declare (ignorable __function__))
    (and (ident-option-aidentp (enum-spec->name? enum-spec)
                               gcc)
         (enumer-list-aidentp (enum-spec->enumers enum-spec)
                              gcc))))

Function: enumer-aidentp

(defun enumer-aidentp (enumer gcc)
  (declare (xargs :guard (and (enumerp enumer) (booleanp gcc))))
  (declare (ignorable enumer))
  (let ((__function__ 'enumer-aidentp))
    (declare (ignorable __function__))
    (and (ident-aidentp (enumer->name enumer)
                        gcc)
         (const-expr-option-aidentp (enumer->value? enumer)
                                    gcc))))

Function: enumer-list-aidentp

(defun enumer-list-aidentp (enumer-list gcc)
  (declare (xargs :guard (and (enumer-listp enumer-list)
                              (booleanp gcc))))
  (let ((__function__ 'enumer-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp enumer-list) t)
          (t (and (enumer-aidentp (car enumer-list) gcc)
                  (enumer-list-aidentp (cdr enumer-list)
                                       gcc))))))

Function: statassert-aidentp

(defun statassert-aidentp (statassert gcc)
  (declare (xargs :guard (and (statassertp statassert)
                              (booleanp gcc))))
  (declare (ignorable statassert))
  (let ((__function__ 'statassert-aidentp))
    (declare (ignorable __function__))
    (const-expr-aidentp (statassert->test statassert)
                        gcc)))

Function: attrib-aidentp

(defun attrib-aidentp (attrib gcc)
  (declare (xargs :guard (and (attribp attrib) (booleanp gcc))))
  (declare (ignorable attrib))
  (let ((__function__ 'attrib-aidentp))
    (declare (ignorable __function__))
    (attrib-case
         attrib
         :name (attrib-name-aidentp (attrib-name->name attrib)
                                    gcc)
         :name-params
         (and (attrib-name-aidentp (attrib-name-params->name attrib)
                                   gcc)
              (expr-list-aidentp (attrib-name-params->params attrib)
                                 gcc)))))

Function: attrib-list-aidentp

(defun attrib-list-aidentp (attrib-list gcc)
  (declare (xargs :guard (and (attrib-listp attrib-list)
                              (booleanp gcc))))
  (let ((__function__ 'attrib-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp attrib-list) t)
          (t (and (attrib-aidentp (car attrib-list) gcc)
                  (attrib-list-aidentp (cdr attrib-list)
                                       gcc))))))

Function: attrib-spec-aidentp

(defun attrib-spec-aidentp (attrib-spec gcc)
  (declare (xargs :guard (and (attrib-specp attrib-spec)
                              (booleanp gcc))))
  (declare (ignorable attrib-spec))
  (let ((__function__ 'attrib-spec-aidentp))
    (declare (ignorable __function__))
    (attrib-list-aidentp (attrib-spec->attribs attrib-spec)
                         gcc)))

Function: attrib-spec-list-aidentp

(defun attrib-spec-list-aidentp (attrib-spec-list gcc)
  (declare (xargs :guard (and (attrib-spec-listp attrib-spec-list)
                              (booleanp gcc))))
  (let ((__function__ 'attrib-spec-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp attrib-spec-list) t)
          (t (and (attrib-spec-aidentp (car attrib-spec-list)
                                       gcc)
                  (attrib-spec-list-aidentp (cdr attrib-spec-list)
                                            gcc))))))

Function: init-declor-aidentp

(defun init-declor-aidentp (init-declor gcc)
 (declare (xargs :guard (and (init-declorp init-declor)
                             (booleanp gcc))))
 (declare (ignorable init-declor))
 (let ((__function__ 'init-declor-aidentp))
  (declare (ignorable __function__))
  (and
   (declor-aidentp (init-declor->declor init-declor)
                   gcc)
   (and (attrib-spec-list-aidentp (init-declor->attribs init-declor)
                                  gcc)
        (initer-option-aidentp (init-declor->initer? init-declor)
                               gcc)))))

Function: init-declor-list-aidentp

(defun init-declor-list-aidentp (init-declor-list gcc)
  (declare (xargs :guard (and (init-declor-listp init-declor-list)
                              (booleanp gcc))))
  (let ((__function__ 'init-declor-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp init-declor-list) t)
          (t (and (init-declor-aidentp (car init-declor-list)
                                       gcc)
                  (init-declor-list-aidentp (cdr init-declor-list)
                                            gcc))))))

Function: declon-aidentp

(defun declon-aidentp (declon gcc)
 (declare (xargs :guard (and (declonp declon) (booleanp gcc))))
 (declare (ignorable declon))
 (let ((__function__ 'declon-aidentp))
  (declare (ignorable __function__))
  (declon-case
      declon
      :declon
      (and (decl-spec-list-aidentp (declon-declon->specs declon)
                                   gcc)
           (init-declor-list-aidentp (declon-declon->declors declon)
                                     gcc))
      :statassert
      (statassert-aidentp (declon-statassert->statassert declon)
                          gcc))))

Function: declon-list-aidentp

(defun declon-list-aidentp (declon-list gcc)
  (declare (xargs :guard (and (declon-listp declon-list)
                              (booleanp gcc))))
  (let ((__function__ 'declon-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp declon-list) t)
          (t (and (declon-aidentp (car declon-list) gcc)
                  (declon-list-aidentp (cdr declon-list)
                                       gcc))))))

Function: label-aidentp

(defun label-aidentp (label gcc)
 (declare (xargs :guard (and (labelp label) (booleanp gcc))))
 (declare (ignorable label))
 (let ((__function__ 'label-aidentp))
  (declare (ignorable __function__))
  (label-case
    label
    :name (and (ident-aidentp (label-name->name label)
                              gcc)
               (attrib-spec-list-aidentp (label-name->attribs label)
                                         gcc))
    :casexpr
    (and (const-expr-aidentp (label-casexpr->expr label)
                             gcc)
         (const-expr-option-aidentp (label-casexpr->range? label)
                                    gcc))
    :default t)))

Function: asm-output-aidentp

(defun asm-output-aidentp (asm-output gcc)
  (declare (xargs :guard (and (asm-outputp asm-output)
                              (booleanp gcc))))
  (declare (ignorable asm-output))
  (let ((__function__ 'asm-output-aidentp))
    (declare (ignorable __function__))
    (and (ident-option-aidentp (asm-output->name? asm-output)
                               gcc)
         (expr-aidentp (asm-output->lvalue asm-output)
                       gcc))))

Function: asm-output-list-aidentp

(defun asm-output-list-aidentp (asm-output-list gcc)
  (declare (xargs :guard (and (asm-output-listp asm-output-list)
                              (booleanp gcc))))
  (let ((__function__ 'asm-output-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp asm-output-list) t)
          (t (and (asm-output-aidentp (car asm-output-list)
                                      gcc)
                  (asm-output-list-aidentp (cdr asm-output-list)
                                           gcc))))))

Function: asm-input-aidentp

(defun asm-input-aidentp (asm-input gcc)
  (declare (xargs :guard (and (asm-inputp asm-input)
                              (booleanp gcc))))
  (declare (ignorable asm-input))
  (let ((__function__ 'asm-input-aidentp))
    (declare (ignorable __function__))
    (and (ident-option-aidentp (asm-input->name? asm-input)
                               gcc)
         (expr-aidentp (asm-input->rvalue asm-input)
                       gcc))))

Function: asm-input-list-aidentp

(defun asm-input-list-aidentp (asm-input-list gcc)
  (declare (xargs :guard (and (asm-input-listp asm-input-list)
                              (booleanp gcc))))
  (let ((__function__ 'asm-input-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp asm-input-list) t)
          (t (and (asm-input-aidentp (car asm-input-list)
                                     gcc)
                  (asm-input-list-aidentp (cdr asm-input-list)
                                          gcc))))))

Function: asm-stmt-aidentp

(defun asm-stmt-aidentp (asm-stmt gcc)
  (declare (xargs :guard (and (asm-stmtp asm-stmt)
                              (booleanp gcc))))
  (declare (ignorable asm-stmt))
  (let ((__function__ 'asm-stmt-aidentp))
    (declare (ignorable __function__))
    (and (asm-output-list-aidentp (asm-stmt->outputs asm-stmt)
                                  gcc)
         (and (asm-input-list-aidentp (asm-stmt->inputs asm-stmt)
                                      gcc)
              (ident-list-aidentp (asm-stmt->labels asm-stmt)
                                  gcc)))))

Function: stmt-aidentp

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

Function: comp-stmt-aidentp

(defun comp-stmt-aidentp (comp-stmt gcc)
  (declare (xargs :guard (and (comp-stmtp comp-stmt)
                              (booleanp gcc))))
  (declare (ignorable comp-stmt))
  (let ((__function__ 'comp-stmt-aidentp))
    (declare (ignorable __function__))
    (and (ident-list-list-aidentp (comp-stmt->labels comp-stmt)
                                  gcc)
         (block-item-list-aidentp (comp-stmt->items comp-stmt)
                                  gcc))))

Function: block-item-aidentp

(defun block-item-aidentp (block-item gcc)
 (declare (xargs :guard (and (block-itemp block-item)
                             (booleanp gcc))))
 (declare (ignorable block-item))
 (let ((__function__ 'block-item-aidentp))
  (declare (ignorable __function__))
  (block-item-case
      block-item
      :declon (declon-aidentp (block-item-declon->declon block-item)
                              gcc)
      :stmt (stmt-aidentp (block-item-stmt->stmt block-item)
                          gcc)
      :ambig (amb-declon/stmt-aidentp
                  (block-item-ambig->declon/stmt block-item)
                  gcc))))

Function: block-item-list-aidentp

(defun block-item-list-aidentp (block-item-list gcc)
  (declare (xargs :guard (and (block-item-listp block-item-list)
                              (booleanp gcc))))
  (let ((__function__ 'block-item-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp block-item-list) t)
          (t (and (block-item-aidentp (car block-item-list)
                                      gcc)
                  (block-item-list-aidentp (cdr block-item-list)
                                           gcc))))))

Function: amb-expr/tyname-aidentp

(defun amb-expr/tyname-aidentp (amb-expr/tyname gcc)
  (declare (xargs :guard (and (amb-expr/tyname-p amb-expr/tyname)
                              (booleanp gcc))))
  (declare (ignorable amb-expr/tyname))
  (let ((__function__ 'amb-expr/tyname-aidentp))
    (declare (ignorable __function__))
    (and (expr-aidentp (amb-expr/tyname->expr amb-expr/tyname)
                       gcc)
         (tyname-aidentp (amb-expr/tyname->tyname amb-expr/tyname)
                         gcc))))

Function: amb-declor/absdeclor-aidentp

(defun amb-declor/absdeclor-aidentp (amb-declor/absdeclor gcc)
 (declare
    (xargs :guard (and (amb-declor/absdeclor-p amb-declor/absdeclor)
                       (booleanp gcc))))
 (declare (ignorable amb-declor/absdeclor))
 (let ((__function__ 'amb-declor/absdeclor-aidentp))
   (declare (ignorable __function__))
   (and (declor-aidentp
             (amb-declor/absdeclor->declor amb-declor/absdeclor)
             gcc)
        (absdeclor-aidentp
             (amb-declor/absdeclor->absdeclor amb-declor/absdeclor)
             gcc))))

Function: amb-declon/stmt-aidentp

(defun amb-declon/stmt-aidentp (amb-declon/stmt gcc)
  (declare (xargs :guard (and (amb-declon/stmt-p amb-declon/stmt)
                              (booleanp gcc))))
  (declare (ignorable amb-declon/stmt))
  (let ((__function__ 'amb-declon/stmt-aidentp))
    (declare (ignorable __function__))
    (and (declon-aidentp (amb-declon/stmt->declon amb-declon/stmt)
                         gcc)
         (expr-aidentp (amb-declon/stmt->expr amb-declon/stmt)
                       gcc))))

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

(defthm return-type-of-expr-aidentp.result
  (b* ((fty::?result (expr-aidentp expr gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-expr-list-aidentp.result
  (b* ((fty::?result (expr-list-aidentp expr-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-expr-option-aidentp.result
  (b* ((fty::?result (expr-option-aidentp expr-option gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-const-expr-aidentp.result
  (b* ((fty::?result (const-expr-aidentp const-expr gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-const-expr-option-aidentp.result
 (b*
  ((fty::?result (const-expr-option-aidentp const-expr-option gcc)))
  (booleanp fty::result))
 :rule-classes :rewrite)

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

(defthm return-type-of-genassoc-aidentp.result
  (b* ((fty::?result (genassoc-aidentp genassoc gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-genassoc-list-aidentp.result
  (b* ((fty::?result (genassoc-list-aidentp genassoc-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-member-designor-aidentp.result
  (b* ((fty::?result (member-designor-aidentp member-designor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-type-spec-aidentp.result
  (b* ((fty::?result (type-spec-aidentp type-spec gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-spec/qual-aidentp.result
  (b* ((fty::?result (spec/qual-aidentp spec/qual gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-spec/qual-list-aidentp.result
  (b* ((fty::?result (spec/qual-list-aidentp spec/qual-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-align-spec-aidentp.result
  (b* ((fty::?result (align-spec-aidentp align-spec gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-decl-spec-aidentp.result
  (b* ((fty::?result (decl-spec-aidentp decl-spec gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-decl-spec-list-aidentp.result
  (b* ((fty::?result (decl-spec-list-aidentp decl-spec-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-typequal/attribspec-aidentp.result
  (b* ((fty::?result
            (typequal/attribspec-aidentp typequal/attribspec gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-typequal/attribspec-list-aidentp.result
  (b* ((fty::?result (typequal/attribspec-list-aidentp
                          typequal/attribspec-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-typequal/attribspec-list-list-aidentp.result
  (b* ((fty::?result (typequal/attribspec-list-list-aidentp
                          typequal/attribspec-list-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-initer-aidentp.result
  (b* ((fty::?result (initer-aidentp initer gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-initer-option-aidentp.result
  (b* ((fty::?result (initer-option-aidentp initer-option gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-desiniter-aidentp.result
  (b* ((fty::?result (desiniter-aidentp desiniter gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-desiniter-list-aidentp.result
  (b* ((fty::?result (desiniter-list-aidentp desiniter-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-designor-aidentp.result
  (b* ((fty::?result (designor-aidentp designor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-designor-list-aidentp.result
  (b* ((fty::?result (designor-list-aidentp designor-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-declor-aidentp.result
  (b* ((fty::?result (declor-aidentp declor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-declor-option-aidentp.result
  (b* ((fty::?result (declor-option-aidentp declor-option gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-dirdeclor-aidentp.result
  (b* ((fty::?result (dirdeclor-aidentp dirdeclor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-absdeclor-aidentp.result
  (b* ((fty::?result (absdeclor-aidentp absdeclor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-absdeclor-option-aidentp.result
  (b*
    ((fty::?result (absdeclor-option-aidentp absdeclor-option gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-dirabsdeclor-aidentp.result
  (b* ((fty::?result (dirabsdeclor-aidentp dirabsdeclor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-dirabsdeclor-option-aidentp.result
  (b* ((fty::?result
            (dirabsdeclor-option-aidentp dirabsdeclor-option gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-param-declon-aidentp.result
  (b* ((fty::?result (param-declon-aidentp param-declon gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-param-declon-list-aidentp.result
 (b*
  ((fty::?result (param-declon-list-aidentp param-declon-list gcc)))
  (booleanp fty::result))
 :rule-classes :rewrite)

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

(defthm return-type-of-param-declor-aidentp.result
  (b* ((fty::?result (param-declor-aidentp param-declor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-tyname-aidentp.result
  (b* ((fty::?result (tyname-aidentp tyname gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-struni-spec-aidentp.result
  (b* ((fty::?result (struni-spec-aidentp struni-spec gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-struct-declon-aidentp.result
  (b* ((fty::?result (struct-declon-aidentp struct-declon gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-struct-declon-list-aidentp.result
  (b* ((fty::?result
            (struct-declon-list-aidentp struct-declon-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-struct-declor-aidentp.result
  (b* ((fty::?result (struct-declor-aidentp struct-declor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-struct-declor-list-aidentp.result
  (b* ((fty::?result
            (struct-declor-list-aidentp struct-declor-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-enum-spec-aidentp.result
  (b* ((fty::?result (enum-spec-aidentp enum-spec gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-enumer-aidentp.result
  (b* ((fty::?result (enumer-aidentp enumer gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-enumer-list-aidentp.result
  (b* ((fty::?result (enumer-list-aidentp enumer-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-statassert-aidentp.result
  (b* ((fty::?result (statassert-aidentp statassert gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-attrib-aidentp.result
  (b* ((fty::?result (attrib-aidentp attrib gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-attrib-list-aidentp.result
  (b* ((fty::?result (attrib-list-aidentp attrib-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-attrib-spec-aidentp.result
  (b* ((fty::?result (attrib-spec-aidentp attrib-spec gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-attrib-spec-list-aidentp.result
  (b*
    ((fty::?result (attrib-spec-list-aidentp attrib-spec-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-init-declor-aidentp.result
  (b* ((fty::?result (init-declor-aidentp init-declor gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-init-declor-list-aidentp.result
  (b*
    ((fty::?result (init-declor-list-aidentp init-declor-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-declon-aidentp.result
  (b* ((fty::?result (declon-aidentp declon gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-declon-list-aidentp.result
  (b* ((fty::?result (declon-list-aidentp declon-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-label-aidentp.result
  (b* ((fty::?result (label-aidentp label gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-asm-output-aidentp.result
  (b* ((fty::?result (asm-output-aidentp asm-output gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-asm-output-list-aidentp.result
  (b* ((fty::?result (asm-output-list-aidentp asm-output-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-asm-input-aidentp.result
  (b* ((fty::?result (asm-input-aidentp asm-input gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-asm-input-list-aidentp.result
  (b* ((fty::?result (asm-input-list-aidentp asm-input-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-asm-stmt-aidentp.result
  (b* ((fty::?result (asm-stmt-aidentp asm-stmt gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-stmt-aidentp.result
  (b* ((fty::?result (stmt-aidentp stmt gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-comp-stmt-aidentp.result
  (b* ((fty::?result (comp-stmt-aidentp comp-stmt gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-block-item-aidentp.result
  (b* ((fty::?result (block-item-aidentp block-item gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-block-item-list-aidentp.result
  (b* ((fty::?result (block-item-list-aidentp block-item-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-amb-expr/tyname-aidentp.result
  (b* ((fty::?result (amb-expr/tyname-aidentp amb-expr/tyname gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

(defthm return-type-of-amb-declor/absdeclor-aidentp.result
 (b* ((fty::?result
           (amb-declor/absdeclor-aidentp amb-declor/absdeclor gcc)))
   (booleanp fty::result))
 :rule-classes :rewrite)

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

(defthm return-type-of-amb-declon/stmt-aidentp.result
  (b* ((fty::?result (amb-declon/stmt-aidentp amb-declon/stmt gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: expr-aidentp-of-expr-fix-expr

(defthm expr-aidentp-of-expr-fix-expr
  (equal (expr-aidentp (expr-fix expr) gcc)
         (expr-aidentp expr gcc)))

Theorem: expr-aidentp-of-bool-fix-gcc

(defthm expr-aidentp-of-bool-fix-gcc
  (equal (expr-aidentp expr (bool-fix gcc))
         (expr-aidentp expr gcc)))

Theorem: expr-list-aidentp-of-expr-list-fix-expr-list

(defthm expr-list-aidentp-of-expr-list-fix-expr-list
  (equal (expr-list-aidentp (expr-list-fix expr-list)
                            gcc)
         (expr-list-aidentp expr-list gcc)))

Theorem: expr-list-aidentp-of-bool-fix-gcc

(defthm expr-list-aidentp-of-bool-fix-gcc
  (equal (expr-list-aidentp expr-list (bool-fix gcc))
         (expr-list-aidentp expr-list gcc)))

Theorem: expr-option-aidentp-of-expr-option-fix-expr-option

(defthm expr-option-aidentp-of-expr-option-fix-expr-option
  (equal (expr-option-aidentp (expr-option-fix expr-option)
                              gcc)
         (expr-option-aidentp expr-option gcc)))

Theorem: expr-option-aidentp-of-bool-fix-gcc

(defthm expr-option-aidentp-of-bool-fix-gcc
  (equal (expr-option-aidentp expr-option (bool-fix gcc))
         (expr-option-aidentp expr-option gcc)))

Theorem: const-expr-aidentp-of-const-expr-fix-const-expr

(defthm const-expr-aidentp-of-const-expr-fix-const-expr
  (equal (const-expr-aidentp (const-expr-fix const-expr)
                             gcc)
         (const-expr-aidentp const-expr gcc)))

Theorem: const-expr-aidentp-of-bool-fix-gcc

(defthm const-expr-aidentp-of-bool-fix-gcc
  (equal (const-expr-aidentp const-expr (bool-fix gcc))
         (const-expr-aidentp const-expr gcc)))

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

(defthm
 const-expr-option-aidentp-of-const-expr-option-fix-const-expr-option
 (equal (const-expr-option-aidentp
             (const-expr-option-fix const-expr-option)
             gcc)
        (const-expr-option-aidentp const-expr-option gcc)))

Theorem: const-expr-option-aidentp-of-bool-fix-gcc

(defthm const-expr-option-aidentp-of-bool-fix-gcc
 (equal (const-expr-option-aidentp const-expr-option (bool-fix gcc))
        (const-expr-option-aidentp const-expr-option gcc)))

Theorem: genassoc-aidentp-of-genassoc-fix-genassoc

(defthm genassoc-aidentp-of-genassoc-fix-genassoc
  (equal (genassoc-aidentp (genassoc-fix genassoc)
                           gcc)
         (genassoc-aidentp genassoc gcc)))

Theorem: genassoc-aidentp-of-bool-fix-gcc

(defthm genassoc-aidentp-of-bool-fix-gcc
  (equal (genassoc-aidentp genassoc (bool-fix gcc))
         (genassoc-aidentp genassoc gcc)))

Theorem: genassoc-list-aidentp-of-genassoc-list-fix-genassoc-list

(defthm genassoc-list-aidentp-of-genassoc-list-fix-genassoc-list
  (equal (genassoc-list-aidentp (genassoc-list-fix genassoc-list)
                                gcc)
         (genassoc-list-aidentp genassoc-list gcc)))

Theorem: genassoc-list-aidentp-of-bool-fix-gcc

(defthm genassoc-list-aidentp-of-bool-fix-gcc
  (equal (genassoc-list-aidentp genassoc-list (bool-fix gcc))
         (genassoc-list-aidentp genassoc-list gcc)))

Theorem: member-designor-aidentp-of-member-designor-fix-member-designor

(defthm
     member-designor-aidentp-of-member-designor-fix-member-designor
 (equal
      (member-designor-aidentp (member-designor-fix member-designor)
                               gcc)
      (member-designor-aidentp member-designor gcc)))

Theorem: member-designor-aidentp-of-bool-fix-gcc

(defthm member-designor-aidentp-of-bool-fix-gcc
  (equal (member-designor-aidentp member-designor (bool-fix gcc))
         (member-designor-aidentp member-designor gcc)))

Theorem: type-spec-aidentp-of-type-spec-fix-type-spec

(defthm type-spec-aidentp-of-type-spec-fix-type-spec
  (equal (type-spec-aidentp (type-spec-fix type-spec)
                            gcc)
         (type-spec-aidentp type-spec gcc)))

Theorem: type-spec-aidentp-of-bool-fix-gcc

(defthm type-spec-aidentp-of-bool-fix-gcc
  (equal (type-spec-aidentp type-spec (bool-fix gcc))
         (type-spec-aidentp type-spec gcc)))

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

(defthm spec/qual-aidentp-of-spec/qual-fix-spec/qual
  (equal (spec/qual-aidentp (spec/qual-fix spec/qual)
                            gcc)
         (spec/qual-aidentp spec/qual gcc)))

Theorem: spec/qual-aidentp-of-bool-fix-gcc

(defthm spec/qual-aidentp-of-bool-fix-gcc
  (equal (spec/qual-aidentp spec/qual (bool-fix gcc))
         (spec/qual-aidentp spec/qual gcc)))

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

(defthm spec/qual-list-aidentp-of-spec/qual-list-fix-spec/qual-list
  (equal (spec/qual-list-aidentp (spec/qual-list-fix spec/qual-list)
                                 gcc)
         (spec/qual-list-aidentp spec/qual-list gcc)))

Theorem: spec/qual-list-aidentp-of-bool-fix-gcc

(defthm spec/qual-list-aidentp-of-bool-fix-gcc
  (equal (spec/qual-list-aidentp spec/qual-list (bool-fix gcc))
         (spec/qual-list-aidentp spec/qual-list gcc)))

Theorem: align-spec-aidentp-of-align-spec-fix-align-spec

(defthm align-spec-aidentp-of-align-spec-fix-align-spec
  (equal (align-spec-aidentp (align-spec-fix align-spec)
                             gcc)
         (align-spec-aidentp align-spec gcc)))

Theorem: align-spec-aidentp-of-bool-fix-gcc

(defthm align-spec-aidentp-of-bool-fix-gcc
  (equal (align-spec-aidentp align-spec (bool-fix gcc))
         (align-spec-aidentp align-spec gcc)))

Theorem: decl-spec-aidentp-of-decl-spec-fix-decl-spec

(defthm decl-spec-aidentp-of-decl-spec-fix-decl-spec
  (equal (decl-spec-aidentp (decl-spec-fix decl-spec)
                            gcc)
         (decl-spec-aidentp decl-spec gcc)))

Theorem: decl-spec-aidentp-of-bool-fix-gcc

(defthm decl-spec-aidentp-of-bool-fix-gcc
  (equal (decl-spec-aidentp decl-spec (bool-fix gcc))
         (decl-spec-aidentp decl-spec gcc)))

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

(defthm decl-spec-list-aidentp-of-decl-spec-list-fix-decl-spec-list
  (equal (decl-spec-list-aidentp (decl-spec-list-fix decl-spec-list)
                                 gcc)
         (decl-spec-list-aidentp decl-spec-list gcc)))

Theorem: decl-spec-list-aidentp-of-bool-fix-gcc

(defthm decl-spec-list-aidentp-of-bool-fix-gcc
  (equal (decl-spec-list-aidentp decl-spec-list (bool-fix gcc))
         (decl-spec-list-aidentp decl-spec-list gcc)))

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

(defthm
 typequal/attribspec-aidentp-of-typequal/attribspec-fix-typequal/attribspec
 (equal (typequal/attribspec-aidentp
             (typequal/attribspec-fix typequal/attribspec)
             gcc)
        (typequal/attribspec-aidentp typequal/attribspec gcc)))

Theorem: typequal/attribspec-aidentp-of-bool-fix-gcc

(defthm typequal/attribspec-aidentp-of-bool-fix-gcc
 (equal
    (typequal/attribspec-aidentp typequal/attribspec (bool-fix gcc))
    (typequal/attribspec-aidentp typequal/attribspec gcc)))

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

(defthm
 typequal/attribspec-list-aidentp-of-typequal/attribspec-list-fix-typequal/attribspec-list
 (equal
   (typequal/attribspec-list-aidentp
        (typequal/attribspec-list-fix typequal/attribspec-list)
        gcc)
   (typequal/attribspec-list-aidentp typequal/attribspec-list gcc)))

Theorem: typequal/attribspec-list-aidentp-of-bool-fix-gcc

(defthm typequal/attribspec-list-aidentp-of-bool-fix-gcc
 (equal
   (typequal/attribspec-list-aidentp
        typequal/attribspec-list (bool-fix gcc))
   (typequal/attribspec-list-aidentp typequal/attribspec-list gcc)))

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

(defthm
 typequal/attribspec-list-list-aidentp-of-typequal/attribspec-list-list-fix-typequal/attribspec-list-list
 (equal
  (typequal/attribspec-list-list-aidentp
   (typequal/attribspec-list-list-fix typequal/attribspec-list-list)
   gcc)
  (typequal/attribspec-list-list-aidentp
       typequal/attribspec-list-list gcc)))

Theorem: typequal/attribspec-list-list-aidentp-of-bool-fix-gcc

(defthm typequal/attribspec-list-list-aidentp-of-bool-fix-gcc
  (equal (typequal/attribspec-list-list-aidentp
              typequal/attribspec-list-list
              (bool-fix gcc))
         (typequal/attribspec-list-list-aidentp
              typequal/attribspec-list-list gcc)))

Theorem: initer-aidentp-of-initer-fix-initer

(defthm initer-aidentp-of-initer-fix-initer
  (equal (initer-aidentp (initer-fix initer) gcc)
         (initer-aidentp initer gcc)))

Theorem: initer-aidentp-of-bool-fix-gcc

(defthm initer-aidentp-of-bool-fix-gcc
  (equal (initer-aidentp initer (bool-fix gcc))
         (initer-aidentp initer gcc)))

Theorem: initer-option-aidentp-of-initer-option-fix-initer-option

(defthm initer-option-aidentp-of-initer-option-fix-initer-option
  (equal (initer-option-aidentp (initer-option-fix initer-option)
                                gcc)
         (initer-option-aidentp initer-option gcc)))

Theorem: initer-option-aidentp-of-bool-fix-gcc

(defthm initer-option-aidentp-of-bool-fix-gcc
  (equal (initer-option-aidentp initer-option (bool-fix gcc))
         (initer-option-aidentp initer-option gcc)))

Theorem: desiniter-aidentp-of-desiniter-fix-desiniter

(defthm desiniter-aidentp-of-desiniter-fix-desiniter
  (equal (desiniter-aidentp (desiniter-fix desiniter)
                            gcc)
         (desiniter-aidentp desiniter gcc)))

Theorem: desiniter-aidentp-of-bool-fix-gcc

(defthm desiniter-aidentp-of-bool-fix-gcc
  (equal (desiniter-aidentp desiniter (bool-fix gcc))
         (desiniter-aidentp desiniter gcc)))

Theorem: desiniter-list-aidentp-of-desiniter-list-fix-desiniter-list

(defthm desiniter-list-aidentp-of-desiniter-list-fix-desiniter-list
  (equal (desiniter-list-aidentp (desiniter-list-fix desiniter-list)
                                 gcc)
         (desiniter-list-aidentp desiniter-list gcc)))

Theorem: desiniter-list-aidentp-of-bool-fix-gcc

(defthm desiniter-list-aidentp-of-bool-fix-gcc
  (equal (desiniter-list-aidentp desiniter-list (bool-fix gcc))
         (desiniter-list-aidentp desiniter-list gcc)))

Theorem: designor-aidentp-of-designor-fix-designor

(defthm designor-aidentp-of-designor-fix-designor
  (equal (designor-aidentp (designor-fix designor)
                           gcc)
         (designor-aidentp designor gcc)))

Theorem: designor-aidentp-of-bool-fix-gcc

(defthm designor-aidentp-of-bool-fix-gcc
  (equal (designor-aidentp designor (bool-fix gcc))
         (designor-aidentp designor gcc)))

Theorem: designor-list-aidentp-of-designor-list-fix-designor-list

(defthm designor-list-aidentp-of-designor-list-fix-designor-list
  (equal (designor-list-aidentp (designor-list-fix designor-list)
                                gcc)
         (designor-list-aidentp designor-list gcc)))

Theorem: designor-list-aidentp-of-bool-fix-gcc

(defthm designor-list-aidentp-of-bool-fix-gcc
  (equal (designor-list-aidentp designor-list (bool-fix gcc))
         (designor-list-aidentp designor-list gcc)))

Theorem: declor-aidentp-of-declor-fix-declor

(defthm declor-aidentp-of-declor-fix-declor
  (equal (declor-aidentp (declor-fix declor) gcc)
         (declor-aidentp declor gcc)))

Theorem: declor-aidentp-of-bool-fix-gcc

(defthm declor-aidentp-of-bool-fix-gcc
  (equal (declor-aidentp declor (bool-fix gcc))
         (declor-aidentp declor gcc)))

Theorem: declor-option-aidentp-of-declor-option-fix-declor-option

(defthm declor-option-aidentp-of-declor-option-fix-declor-option
  (equal (declor-option-aidentp (declor-option-fix declor-option)
                                gcc)
         (declor-option-aidentp declor-option gcc)))

Theorem: declor-option-aidentp-of-bool-fix-gcc

(defthm declor-option-aidentp-of-bool-fix-gcc
  (equal (declor-option-aidentp declor-option (bool-fix gcc))
         (declor-option-aidentp declor-option gcc)))

Theorem: dirdeclor-aidentp-of-dirdeclor-fix-dirdeclor

(defthm dirdeclor-aidentp-of-dirdeclor-fix-dirdeclor
  (equal (dirdeclor-aidentp (dirdeclor-fix dirdeclor)
                            gcc)
         (dirdeclor-aidentp dirdeclor gcc)))

Theorem: dirdeclor-aidentp-of-bool-fix-gcc

(defthm dirdeclor-aidentp-of-bool-fix-gcc
  (equal (dirdeclor-aidentp dirdeclor (bool-fix gcc))
         (dirdeclor-aidentp dirdeclor gcc)))

Theorem: absdeclor-aidentp-of-absdeclor-fix-absdeclor

(defthm absdeclor-aidentp-of-absdeclor-fix-absdeclor
  (equal (absdeclor-aidentp (absdeclor-fix absdeclor)
                            gcc)
         (absdeclor-aidentp absdeclor gcc)))

Theorem: absdeclor-aidentp-of-bool-fix-gcc

(defthm absdeclor-aidentp-of-bool-fix-gcc
  (equal (absdeclor-aidentp absdeclor (bool-fix gcc))
         (absdeclor-aidentp absdeclor gcc)))

Theorem: absdeclor-option-aidentp-of-absdeclor-option-fix-absdeclor-option

(defthm
  absdeclor-option-aidentp-of-absdeclor-option-fix-absdeclor-option
 (equal
   (absdeclor-option-aidentp (absdeclor-option-fix absdeclor-option)
                             gcc)
   (absdeclor-option-aidentp absdeclor-option gcc)))

Theorem: absdeclor-option-aidentp-of-bool-fix-gcc

(defthm absdeclor-option-aidentp-of-bool-fix-gcc
  (equal (absdeclor-option-aidentp absdeclor-option (bool-fix gcc))
         (absdeclor-option-aidentp absdeclor-option gcc)))

Theorem: dirabsdeclor-aidentp-of-dirabsdeclor-fix-dirabsdeclor

(defthm dirabsdeclor-aidentp-of-dirabsdeclor-fix-dirabsdeclor
  (equal (dirabsdeclor-aidentp (dirabsdeclor-fix dirabsdeclor)
                               gcc)
         (dirabsdeclor-aidentp dirabsdeclor gcc)))

Theorem: dirabsdeclor-aidentp-of-bool-fix-gcc

(defthm dirabsdeclor-aidentp-of-bool-fix-gcc
  (equal (dirabsdeclor-aidentp dirabsdeclor (bool-fix gcc))
         (dirabsdeclor-aidentp dirabsdeclor gcc)))

Theorem: dirabsdeclor-option-aidentp-of-dirabsdeclor-option-fix-dirabsdeclor-option

(defthm
 dirabsdeclor-option-aidentp-of-dirabsdeclor-option-fix-dirabsdeclor-option
 (equal (dirabsdeclor-option-aidentp
             (dirabsdeclor-option-fix dirabsdeclor-option)
             gcc)
        (dirabsdeclor-option-aidentp dirabsdeclor-option gcc)))

Theorem: dirabsdeclor-option-aidentp-of-bool-fix-gcc

(defthm dirabsdeclor-option-aidentp-of-bool-fix-gcc
 (equal
    (dirabsdeclor-option-aidentp dirabsdeclor-option (bool-fix gcc))
    (dirabsdeclor-option-aidentp dirabsdeclor-option gcc)))

Theorem: param-declon-aidentp-of-param-declon-fix-param-declon

(defthm param-declon-aidentp-of-param-declon-fix-param-declon
  (equal (param-declon-aidentp (param-declon-fix param-declon)
                               gcc)
         (param-declon-aidentp param-declon gcc)))

Theorem: param-declon-aidentp-of-bool-fix-gcc

(defthm param-declon-aidentp-of-bool-fix-gcc
  (equal (param-declon-aidentp param-declon (bool-fix gcc))
         (param-declon-aidentp param-declon gcc)))

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

(defthm
 param-declon-list-aidentp-of-param-declon-list-fix-param-declon-list
 (equal (param-declon-list-aidentp
             (param-declon-list-fix param-declon-list)
             gcc)
        (param-declon-list-aidentp param-declon-list gcc)))

Theorem: param-declon-list-aidentp-of-bool-fix-gcc

(defthm param-declon-list-aidentp-of-bool-fix-gcc
 (equal (param-declon-list-aidentp param-declon-list (bool-fix gcc))
        (param-declon-list-aidentp param-declon-list gcc)))

Theorem: param-declor-aidentp-of-param-declor-fix-param-declor

(defthm param-declor-aidentp-of-param-declor-fix-param-declor
  (equal (param-declor-aidentp (param-declor-fix param-declor)
                               gcc)
         (param-declor-aidentp param-declor gcc)))

Theorem: param-declor-aidentp-of-bool-fix-gcc

(defthm param-declor-aidentp-of-bool-fix-gcc
  (equal (param-declor-aidentp param-declor (bool-fix gcc))
         (param-declor-aidentp param-declor gcc)))

Theorem: tyname-aidentp-of-tyname-fix-tyname

(defthm tyname-aidentp-of-tyname-fix-tyname
  (equal (tyname-aidentp (tyname-fix tyname) gcc)
         (tyname-aidentp tyname gcc)))

Theorem: tyname-aidentp-of-bool-fix-gcc

(defthm tyname-aidentp-of-bool-fix-gcc
  (equal (tyname-aidentp tyname (bool-fix gcc))
         (tyname-aidentp tyname gcc)))

Theorem: struni-spec-aidentp-of-struni-spec-fix-struni-spec

(defthm struni-spec-aidentp-of-struni-spec-fix-struni-spec
  (equal (struni-spec-aidentp (struni-spec-fix struni-spec)
                              gcc)
         (struni-spec-aidentp struni-spec gcc)))

Theorem: struni-spec-aidentp-of-bool-fix-gcc

(defthm struni-spec-aidentp-of-bool-fix-gcc
  (equal (struni-spec-aidentp struni-spec (bool-fix gcc))
         (struni-spec-aidentp struni-spec gcc)))

Theorem: struct-declon-aidentp-of-struct-declon-fix-struct-declon

(defthm struct-declon-aidentp-of-struct-declon-fix-struct-declon
  (equal (struct-declon-aidentp (struct-declon-fix struct-declon)
                                gcc)
         (struct-declon-aidentp struct-declon gcc)))

Theorem: struct-declon-aidentp-of-bool-fix-gcc

(defthm struct-declon-aidentp-of-bool-fix-gcc
  (equal (struct-declon-aidentp struct-declon (bool-fix gcc))
         (struct-declon-aidentp struct-declon gcc)))

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

(defthm
 struct-declon-list-aidentp-of-struct-declon-list-fix-struct-declon-list
 (equal (struct-declon-list-aidentp
             (struct-declon-list-fix struct-declon-list)
             gcc)
        (struct-declon-list-aidentp struct-declon-list gcc)))

Theorem: struct-declon-list-aidentp-of-bool-fix-gcc

(defthm struct-declon-list-aidentp-of-bool-fix-gcc
 (equal
      (struct-declon-list-aidentp struct-declon-list (bool-fix gcc))
      (struct-declon-list-aidentp struct-declon-list gcc)))

Theorem: struct-declor-aidentp-of-struct-declor-fix-struct-declor

(defthm struct-declor-aidentp-of-struct-declor-fix-struct-declor
  (equal (struct-declor-aidentp (struct-declor-fix struct-declor)
                                gcc)
         (struct-declor-aidentp struct-declor gcc)))

Theorem: struct-declor-aidentp-of-bool-fix-gcc

(defthm struct-declor-aidentp-of-bool-fix-gcc
  (equal (struct-declor-aidentp struct-declor (bool-fix gcc))
         (struct-declor-aidentp struct-declor gcc)))

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

(defthm
 struct-declor-list-aidentp-of-struct-declor-list-fix-struct-declor-list
 (equal (struct-declor-list-aidentp
             (struct-declor-list-fix struct-declor-list)
             gcc)
        (struct-declor-list-aidentp struct-declor-list gcc)))

Theorem: struct-declor-list-aidentp-of-bool-fix-gcc

(defthm struct-declor-list-aidentp-of-bool-fix-gcc
 (equal
      (struct-declor-list-aidentp struct-declor-list (bool-fix gcc))
      (struct-declor-list-aidentp struct-declor-list gcc)))

Theorem: enum-spec-aidentp-of-enum-spec-fix-enum-spec

(defthm enum-spec-aidentp-of-enum-spec-fix-enum-spec
  (equal (enum-spec-aidentp (enum-spec-fix enum-spec)
                            gcc)
         (enum-spec-aidentp enum-spec gcc)))

Theorem: enum-spec-aidentp-of-bool-fix-gcc

(defthm enum-spec-aidentp-of-bool-fix-gcc
  (equal (enum-spec-aidentp enum-spec (bool-fix gcc))
         (enum-spec-aidentp enum-spec gcc)))

Theorem: enumer-aidentp-of-enumer-fix-enumer

(defthm enumer-aidentp-of-enumer-fix-enumer
  (equal (enumer-aidentp (enumer-fix enumer) gcc)
         (enumer-aidentp enumer gcc)))

Theorem: enumer-aidentp-of-bool-fix-gcc

(defthm enumer-aidentp-of-bool-fix-gcc
  (equal (enumer-aidentp enumer (bool-fix gcc))
         (enumer-aidentp enumer gcc)))

Theorem: enumer-list-aidentp-of-enumer-list-fix-enumer-list

(defthm enumer-list-aidentp-of-enumer-list-fix-enumer-list
  (equal (enumer-list-aidentp (enumer-list-fix enumer-list)
                              gcc)
         (enumer-list-aidentp enumer-list gcc)))

Theorem: enumer-list-aidentp-of-bool-fix-gcc

(defthm enumer-list-aidentp-of-bool-fix-gcc
  (equal (enumer-list-aidentp enumer-list (bool-fix gcc))
         (enumer-list-aidentp enumer-list gcc)))

Theorem: statassert-aidentp-of-statassert-fix-statassert

(defthm statassert-aidentp-of-statassert-fix-statassert
  (equal (statassert-aidentp (statassert-fix statassert)
                             gcc)
         (statassert-aidentp statassert gcc)))

Theorem: statassert-aidentp-of-bool-fix-gcc

(defthm statassert-aidentp-of-bool-fix-gcc
  (equal (statassert-aidentp statassert (bool-fix gcc))
         (statassert-aidentp statassert gcc)))

Theorem: attrib-aidentp-of-attrib-fix-attrib

(defthm attrib-aidentp-of-attrib-fix-attrib
  (equal (attrib-aidentp (attrib-fix attrib) gcc)
         (attrib-aidentp attrib gcc)))

Theorem: attrib-aidentp-of-bool-fix-gcc

(defthm attrib-aidentp-of-bool-fix-gcc
  (equal (attrib-aidentp attrib (bool-fix gcc))
         (attrib-aidentp attrib gcc)))

Theorem: attrib-list-aidentp-of-attrib-list-fix-attrib-list

(defthm attrib-list-aidentp-of-attrib-list-fix-attrib-list
  (equal (attrib-list-aidentp (attrib-list-fix attrib-list)
                              gcc)
         (attrib-list-aidentp attrib-list gcc)))

Theorem: attrib-list-aidentp-of-bool-fix-gcc

(defthm attrib-list-aidentp-of-bool-fix-gcc
  (equal (attrib-list-aidentp attrib-list (bool-fix gcc))
         (attrib-list-aidentp attrib-list gcc)))

Theorem: attrib-spec-aidentp-of-attrib-spec-fix-attrib-spec

(defthm attrib-spec-aidentp-of-attrib-spec-fix-attrib-spec
  (equal (attrib-spec-aidentp (attrib-spec-fix attrib-spec)
                              gcc)
         (attrib-spec-aidentp attrib-spec gcc)))

Theorem: attrib-spec-aidentp-of-bool-fix-gcc

(defthm attrib-spec-aidentp-of-bool-fix-gcc
  (equal (attrib-spec-aidentp attrib-spec (bool-fix gcc))
         (attrib-spec-aidentp attrib-spec gcc)))

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

(defthm
  attrib-spec-list-aidentp-of-attrib-spec-list-fix-attrib-spec-list
 (equal
   (attrib-spec-list-aidentp (attrib-spec-list-fix attrib-spec-list)
                             gcc)
   (attrib-spec-list-aidentp attrib-spec-list gcc)))

Theorem: attrib-spec-list-aidentp-of-bool-fix-gcc

(defthm attrib-spec-list-aidentp-of-bool-fix-gcc
  (equal (attrib-spec-list-aidentp attrib-spec-list (bool-fix gcc))
         (attrib-spec-list-aidentp attrib-spec-list gcc)))

Theorem: init-declor-aidentp-of-init-declor-fix-init-declor

(defthm init-declor-aidentp-of-init-declor-fix-init-declor
  (equal (init-declor-aidentp (init-declor-fix init-declor)
                              gcc)
         (init-declor-aidentp init-declor gcc)))

Theorem: init-declor-aidentp-of-bool-fix-gcc

(defthm init-declor-aidentp-of-bool-fix-gcc
  (equal (init-declor-aidentp init-declor (bool-fix gcc))
         (init-declor-aidentp init-declor gcc)))

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

(defthm
  init-declor-list-aidentp-of-init-declor-list-fix-init-declor-list
 (equal
   (init-declor-list-aidentp (init-declor-list-fix init-declor-list)
                             gcc)
   (init-declor-list-aidentp init-declor-list gcc)))

Theorem: init-declor-list-aidentp-of-bool-fix-gcc

(defthm init-declor-list-aidentp-of-bool-fix-gcc
  (equal (init-declor-list-aidentp init-declor-list (bool-fix gcc))
         (init-declor-list-aidentp init-declor-list gcc)))

Theorem: declon-aidentp-of-declon-fix-declon

(defthm declon-aidentp-of-declon-fix-declon
  (equal (declon-aidentp (declon-fix declon) gcc)
         (declon-aidentp declon gcc)))

Theorem: declon-aidentp-of-bool-fix-gcc

(defthm declon-aidentp-of-bool-fix-gcc
  (equal (declon-aidentp declon (bool-fix gcc))
         (declon-aidentp declon gcc)))

Theorem: declon-list-aidentp-of-declon-list-fix-declon-list

(defthm declon-list-aidentp-of-declon-list-fix-declon-list
  (equal (declon-list-aidentp (declon-list-fix declon-list)
                              gcc)
         (declon-list-aidentp declon-list gcc)))

Theorem: declon-list-aidentp-of-bool-fix-gcc

(defthm declon-list-aidentp-of-bool-fix-gcc
  (equal (declon-list-aidentp declon-list (bool-fix gcc))
         (declon-list-aidentp declon-list gcc)))

Theorem: label-aidentp-of-label-fix-label

(defthm label-aidentp-of-label-fix-label
  (equal (label-aidentp (label-fix label) gcc)
         (label-aidentp label gcc)))

Theorem: label-aidentp-of-bool-fix-gcc

(defthm label-aidentp-of-bool-fix-gcc
  (equal (label-aidentp label (bool-fix gcc))
         (label-aidentp label gcc)))

Theorem: asm-output-aidentp-of-asm-output-fix-asm-output

(defthm asm-output-aidentp-of-asm-output-fix-asm-output
  (equal (asm-output-aidentp (asm-output-fix asm-output)
                             gcc)
         (asm-output-aidentp asm-output gcc)))

Theorem: asm-output-aidentp-of-bool-fix-gcc

(defthm asm-output-aidentp-of-bool-fix-gcc
  (equal (asm-output-aidentp asm-output (bool-fix gcc))
         (asm-output-aidentp asm-output gcc)))

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

(defthm
     asm-output-list-aidentp-of-asm-output-list-fix-asm-output-list
 (equal
      (asm-output-list-aidentp (asm-output-list-fix asm-output-list)
                               gcc)
      (asm-output-list-aidentp asm-output-list gcc)))

Theorem: asm-output-list-aidentp-of-bool-fix-gcc

(defthm asm-output-list-aidentp-of-bool-fix-gcc
  (equal (asm-output-list-aidentp asm-output-list (bool-fix gcc))
         (asm-output-list-aidentp asm-output-list gcc)))

Theorem: asm-input-aidentp-of-asm-input-fix-asm-input

(defthm asm-input-aidentp-of-asm-input-fix-asm-input
  (equal (asm-input-aidentp (asm-input-fix asm-input)
                            gcc)
         (asm-input-aidentp asm-input gcc)))

Theorem: asm-input-aidentp-of-bool-fix-gcc

(defthm asm-input-aidentp-of-bool-fix-gcc
  (equal (asm-input-aidentp asm-input (bool-fix gcc))
         (asm-input-aidentp asm-input gcc)))

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

(defthm asm-input-list-aidentp-of-asm-input-list-fix-asm-input-list
  (equal (asm-input-list-aidentp (asm-input-list-fix asm-input-list)
                                 gcc)
         (asm-input-list-aidentp asm-input-list gcc)))

Theorem: asm-input-list-aidentp-of-bool-fix-gcc

(defthm asm-input-list-aidentp-of-bool-fix-gcc
  (equal (asm-input-list-aidentp asm-input-list (bool-fix gcc))
         (asm-input-list-aidentp asm-input-list gcc)))

Theorem: asm-stmt-aidentp-of-asm-stmt-fix-asm-stmt

(defthm asm-stmt-aidentp-of-asm-stmt-fix-asm-stmt
  (equal (asm-stmt-aidentp (asm-stmt-fix asm-stmt)
                           gcc)
         (asm-stmt-aidentp asm-stmt gcc)))

Theorem: asm-stmt-aidentp-of-bool-fix-gcc

(defthm asm-stmt-aidentp-of-bool-fix-gcc
  (equal (asm-stmt-aidentp asm-stmt (bool-fix gcc))
         (asm-stmt-aidentp asm-stmt gcc)))

Theorem: stmt-aidentp-of-stmt-fix-stmt

(defthm stmt-aidentp-of-stmt-fix-stmt
  (equal (stmt-aidentp (stmt-fix stmt) gcc)
         (stmt-aidentp stmt gcc)))

Theorem: stmt-aidentp-of-bool-fix-gcc

(defthm stmt-aidentp-of-bool-fix-gcc
  (equal (stmt-aidentp stmt (bool-fix gcc))
         (stmt-aidentp stmt gcc)))

Theorem: comp-stmt-aidentp-of-comp-stmt-fix-comp-stmt

(defthm comp-stmt-aidentp-of-comp-stmt-fix-comp-stmt
  (equal (comp-stmt-aidentp (comp-stmt-fix comp-stmt)
                            gcc)
         (comp-stmt-aidentp comp-stmt gcc)))

Theorem: comp-stmt-aidentp-of-bool-fix-gcc

(defthm comp-stmt-aidentp-of-bool-fix-gcc
  (equal (comp-stmt-aidentp comp-stmt (bool-fix gcc))
         (comp-stmt-aidentp comp-stmt gcc)))

Theorem: block-item-aidentp-of-block-item-fix-block-item

(defthm block-item-aidentp-of-block-item-fix-block-item
  (equal (block-item-aidentp (block-item-fix block-item)
                             gcc)
         (block-item-aidentp block-item gcc)))

Theorem: block-item-aidentp-of-bool-fix-gcc

(defthm block-item-aidentp-of-bool-fix-gcc
  (equal (block-item-aidentp block-item (bool-fix gcc))
         (block-item-aidentp block-item gcc)))

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

(defthm
     block-item-list-aidentp-of-block-item-list-fix-block-item-list
 (equal
      (block-item-list-aidentp (block-item-list-fix block-item-list)
                               gcc)
      (block-item-list-aidentp block-item-list gcc)))

Theorem: block-item-list-aidentp-of-bool-fix-gcc

(defthm block-item-list-aidentp-of-bool-fix-gcc
  (equal (block-item-list-aidentp block-item-list (bool-fix gcc))
         (block-item-list-aidentp block-item-list gcc)))

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

(defthm
     amb-expr/tyname-aidentp-of-amb-expr/tyname-fix-amb-expr/tyname
 (equal
      (amb-expr/tyname-aidentp (amb-expr/tyname-fix amb-expr/tyname)
                               gcc)
      (amb-expr/tyname-aidentp amb-expr/tyname gcc)))

Theorem: amb-expr/tyname-aidentp-of-bool-fix-gcc

(defthm amb-expr/tyname-aidentp-of-bool-fix-gcc
  (equal (amb-expr/tyname-aidentp amb-expr/tyname (bool-fix gcc))
         (amb-expr/tyname-aidentp amb-expr/tyname gcc)))

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

(defthm
 amb-declor/absdeclor-aidentp-of-amb-declor/absdeclor-fix-amb-declor/absdeclor
 (equal (amb-declor/absdeclor-aidentp
             (amb-declor/absdeclor-fix amb-declor/absdeclor)
             gcc)
        (amb-declor/absdeclor-aidentp amb-declor/absdeclor gcc)))

Theorem: amb-declor/absdeclor-aidentp-of-bool-fix-gcc

(defthm amb-declor/absdeclor-aidentp-of-bool-fix-gcc
 (equal
  (amb-declor/absdeclor-aidentp amb-declor/absdeclor (bool-fix gcc))
  (amb-declor/absdeclor-aidentp amb-declor/absdeclor gcc)))

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

(defthm
     amb-declon/stmt-aidentp-of-amb-declon/stmt-fix-amb-declon/stmt
 (equal
      (amb-declon/stmt-aidentp (amb-declon/stmt-fix amb-declon/stmt)
                               gcc)
      (amb-declon/stmt-aidentp amb-declon/stmt gcc)))

Theorem: amb-declon/stmt-aidentp-of-bool-fix-gcc

(defthm amb-declon/stmt-aidentp-of-bool-fix-gcc
  (equal (amb-declon/stmt-aidentp amb-declon/stmt (bool-fix gcc))
         (amb-declon/stmt-aidentp amb-declon/stmt gcc)))

Theorem: expr-aidentp-expr-equiv-congruence-on-expr

(defthm expr-aidentp-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (expr-aidentp expr gcc)
                  (expr-aidentp expr-equiv gcc)))
  :rule-classes :congruence)

Theorem: expr-aidentp-iff-congruence-on-gcc

(defthm expr-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (expr-aidentp expr gcc)
                  (expr-aidentp expr gcc-equiv)))
  :rule-classes :congruence)

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

(defthm expr-list-aidentp-expr-list-equiv-congruence-on-expr-list
  (implies (expr-list-equiv expr-list expr-list-equiv)
           (equal (expr-list-aidentp expr-list gcc)
                  (expr-list-aidentp expr-list-equiv gcc)))
  :rule-classes :congruence)

Theorem: expr-list-aidentp-iff-congruence-on-gcc

(defthm expr-list-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (expr-list-aidentp expr-list gcc)
                  (expr-list-aidentp expr-list gcc-equiv)))
  :rule-classes :congruence)

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

(defthm
    expr-option-aidentp-expr-option-equiv-congruence-on-expr-option
  (implies (expr-option-equiv expr-option expr-option-equiv)
           (equal (expr-option-aidentp expr-option gcc)
                  (expr-option-aidentp expr-option-equiv gcc)))
  :rule-classes :congruence)

Theorem: expr-option-aidentp-iff-congruence-on-gcc

(defthm expr-option-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (expr-option-aidentp expr-option gcc)
                  (expr-option-aidentp expr-option gcc-equiv)))
  :rule-classes :congruence)

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

(defthm const-expr-aidentp-const-expr-equiv-congruence-on-const-expr
  (implies (const-expr-equiv const-expr const-expr-equiv)
           (equal (const-expr-aidentp const-expr gcc)
                  (const-expr-aidentp const-expr-equiv gcc)))
  :rule-classes :congruence)

Theorem: const-expr-aidentp-iff-congruence-on-gcc

(defthm const-expr-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (const-expr-aidentp const-expr gcc)
                  (const-expr-aidentp const-expr gcc-equiv)))
  :rule-classes :congruence)

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

(defthm
 const-expr-option-aidentp-const-expr-option-equiv-congruence-on-const-expr-option
 (implies
    (const-expr-option-equiv const-expr-option
                             const-expr-option-equiv)
    (equal (const-expr-option-aidentp const-expr-option gcc)
           (const-expr-option-aidentp const-expr-option-equiv gcc)))
 :rule-classes :congruence)

Theorem: const-expr-option-aidentp-iff-congruence-on-gcc

(defthm const-expr-option-aidentp-iff-congruence-on-gcc
 (implies
    (iff gcc gcc-equiv)
    (equal (const-expr-option-aidentp const-expr-option gcc)
           (const-expr-option-aidentp const-expr-option gcc-equiv)))
 :rule-classes :congruence)

Theorem: genassoc-aidentp-genassoc-equiv-congruence-on-genassoc

(defthm genassoc-aidentp-genassoc-equiv-congruence-on-genassoc
  (implies (genassoc-equiv genassoc genassoc-equiv)
           (equal (genassoc-aidentp genassoc gcc)
                  (genassoc-aidentp genassoc-equiv gcc)))
  :rule-classes :congruence)

Theorem: genassoc-aidentp-iff-congruence-on-gcc

(defthm genassoc-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (genassoc-aidentp genassoc gcc)
                  (genassoc-aidentp genassoc gcc-equiv)))
  :rule-classes :congruence)

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

(defthm
 genassoc-list-aidentp-genassoc-list-equiv-congruence-on-genassoc-list
 (implies (genassoc-list-equiv genassoc-list genassoc-list-equiv)
          (equal (genassoc-list-aidentp genassoc-list gcc)
                 (genassoc-list-aidentp genassoc-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: genassoc-list-aidentp-iff-congruence-on-gcc

(defthm genassoc-list-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (genassoc-list-aidentp genassoc-list gcc)
                  (genassoc-list-aidentp genassoc-list gcc-equiv)))
  :rule-classes :congruence)

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

(defthm
 member-designor-aidentp-member-designor-equiv-congruence-on-member-designor
 (implies
      (member-designor-equiv member-designor member-designor-equiv)
      (equal (member-designor-aidentp member-designor gcc)
             (member-designor-aidentp member-designor-equiv gcc)))
 :rule-classes :congruence)

Theorem: member-designor-aidentp-iff-congruence-on-gcc

(defthm member-designor-aidentp-iff-congruence-on-gcc
  (implies
       (iff gcc gcc-equiv)
       (equal (member-designor-aidentp member-designor gcc)
              (member-designor-aidentp member-designor gcc-equiv)))
  :rule-classes :congruence)

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

(defthm type-spec-aidentp-type-spec-equiv-congruence-on-type-spec
  (implies (type-spec-equiv type-spec type-spec-equiv)
           (equal (type-spec-aidentp type-spec gcc)
                  (type-spec-aidentp type-spec-equiv gcc)))
  :rule-classes :congruence)

Theorem: type-spec-aidentp-iff-congruence-on-gcc

(defthm type-spec-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (type-spec-aidentp type-spec gcc)
                  (type-spec-aidentp type-spec gcc-equiv)))
  :rule-classes :congruence)

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

(defthm spec/qual-aidentp-spec/qual-equiv-congruence-on-spec/qual
  (implies (spec/qual-equiv spec/qual spec/qual-equiv)
           (equal (spec/qual-aidentp spec/qual gcc)
                  (spec/qual-aidentp spec/qual-equiv gcc)))
  :rule-classes :congruence)

Theorem: spec/qual-aidentp-iff-congruence-on-gcc

(defthm spec/qual-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (spec/qual-aidentp spec/qual gcc)
                  (spec/qual-aidentp spec/qual gcc-equiv)))
  :rule-classes :congruence)

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

(defthm
 spec/qual-list-aidentp-spec/qual-list-equiv-congruence-on-spec/qual-list
 (implies (spec/qual-list-equiv spec/qual-list spec/qual-list-equiv)
          (equal (spec/qual-list-aidentp spec/qual-list gcc)
                 (spec/qual-list-aidentp spec/qual-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: spec/qual-list-aidentp-iff-congruence-on-gcc

(defthm spec/qual-list-aidentp-iff-congruence-on-gcc
 (implies (iff gcc gcc-equiv)
          (equal (spec/qual-list-aidentp spec/qual-list gcc)
                 (spec/qual-list-aidentp spec/qual-list gcc-equiv)))
 :rule-classes :congruence)

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

(defthm align-spec-aidentp-align-spec-equiv-congruence-on-align-spec
  (implies (align-spec-equiv align-spec align-spec-equiv)
           (equal (align-spec-aidentp align-spec gcc)
                  (align-spec-aidentp align-spec-equiv gcc)))
  :rule-classes :congruence)

Theorem: align-spec-aidentp-iff-congruence-on-gcc

(defthm align-spec-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (align-spec-aidentp align-spec gcc)
                  (align-spec-aidentp align-spec gcc-equiv)))
  :rule-classes :congruence)

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

(defthm decl-spec-aidentp-decl-spec-equiv-congruence-on-decl-spec
  (implies (decl-spec-equiv decl-spec decl-spec-equiv)
           (equal (decl-spec-aidentp decl-spec gcc)
                  (decl-spec-aidentp decl-spec-equiv gcc)))
  :rule-classes :congruence)

Theorem: decl-spec-aidentp-iff-congruence-on-gcc

(defthm decl-spec-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (decl-spec-aidentp decl-spec gcc)
                  (decl-spec-aidentp decl-spec gcc-equiv)))
  :rule-classes :congruence)

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

(defthm
 decl-spec-list-aidentp-decl-spec-list-equiv-congruence-on-decl-spec-list
 (implies (decl-spec-list-equiv decl-spec-list decl-spec-list-equiv)
          (equal (decl-spec-list-aidentp decl-spec-list gcc)
                 (decl-spec-list-aidentp decl-spec-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: decl-spec-list-aidentp-iff-congruence-on-gcc

(defthm decl-spec-list-aidentp-iff-congruence-on-gcc
 (implies (iff gcc gcc-equiv)
          (equal (decl-spec-list-aidentp decl-spec-list gcc)
                 (decl-spec-list-aidentp decl-spec-list gcc-equiv)))
 :rule-classes :congruence)

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

(defthm
 typequal/attribspec-aidentp-typequal/attribspec-equiv-congruence-on-typequal/attribspec
 (implies
  (typequal/attribspec-equiv typequal/attribspec
                             typequal/attribspec-equiv)
  (equal
       (typequal/attribspec-aidentp typequal/attribspec gcc)
       (typequal/attribspec-aidentp typequal/attribspec-equiv gcc)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-aidentp-iff-congruence-on-gcc

(defthm typequal/attribspec-aidentp-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal
       (typequal/attribspec-aidentp typequal/attribspec gcc)
       (typequal/attribspec-aidentp typequal/attribspec gcc-equiv)))
 :rule-classes :congruence)

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

(defthm
 typequal/attribspec-list-aidentp-typequal/attribspec-list-equiv-congruence-on-typequal/attribspec-list
 (implies
  (typequal/attribspec-list-equiv typequal/attribspec-list
                                  typequal/attribspec-list-equiv)
  (equal
     (typequal/attribspec-list-aidentp typequal/attribspec-list gcc)
     (typequal/attribspec-list-aidentp
          typequal/attribspec-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-aidentp-iff-congruence-on-gcc

(defthm typequal/attribspec-list-aidentp-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal
     (typequal/attribspec-list-aidentp typequal/attribspec-list gcc)
     (typequal/attribspec-list-aidentp
          typequal/attribspec-list gcc-equiv)))
 :rule-classes :congruence)

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

(defthm
 typequal/attribspec-list-list-aidentp-typequal/attribspec-list-list-equiv-congruence-on-typequal/attribspec-list-list
 (implies (typequal/attribspec-list-list-equiv
               typequal/attribspec-list-list
               typequal/attribspec-list-list-equiv)
          (equal (typequal/attribspec-list-list-aidentp
                      typequal/attribspec-list-list gcc)
                 (typequal/attribspec-list-list-aidentp
                      typequal/attribspec-list-list-equiv
                      gcc)))
 :rule-classes :congruence)

Theorem: typequal/attribspec-list-list-aidentp-iff-congruence-on-gcc

(defthm typequal/attribspec-list-list-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (typequal/attribspec-list-list-aidentp
                       typequal/attribspec-list-list gcc)
                  (typequal/attribspec-list-list-aidentp
                       typequal/attribspec-list-list
                       gcc-equiv)))
  :rule-classes :congruence)

Theorem: initer-aidentp-initer-equiv-congruence-on-initer

(defthm initer-aidentp-initer-equiv-congruence-on-initer
  (implies (initer-equiv initer initer-equiv)
           (equal (initer-aidentp initer gcc)
                  (initer-aidentp initer-equiv gcc)))
  :rule-classes :congruence)

Theorem: initer-aidentp-iff-congruence-on-gcc

(defthm initer-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (initer-aidentp initer gcc)
                  (initer-aidentp initer gcc-equiv)))
  :rule-classes :congruence)

Theorem: initer-option-aidentp-initer-option-equiv-congruence-on-initer-option

(defthm
 initer-option-aidentp-initer-option-equiv-congruence-on-initer-option
 (implies (initer-option-equiv initer-option initer-option-equiv)
          (equal (initer-option-aidentp initer-option gcc)
                 (initer-option-aidentp initer-option-equiv gcc)))
 :rule-classes :congruence)

Theorem: initer-option-aidentp-iff-congruence-on-gcc

(defthm initer-option-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (initer-option-aidentp initer-option gcc)
                  (initer-option-aidentp initer-option gcc-equiv)))
  :rule-classes :congruence)

Theorem: desiniter-aidentp-desiniter-equiv-congruence-on-desiniter

(defthm desiniter-aidentp-desiniter-equiv-congruence-on-desiniter
  (implies (desiniter-equiv desiniter desiniter-equiv)
           (equal (desiniter-aidentp desiniter gcc)
                  (desiniter-aidentp desiniter-equiv gcc)))
  :rule-classes :congruence)

Theorem: desiniter-aidentp-iff-congruence-on-gcc

(defthm desiniter-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (desiniter-aidentp desiniter gcc)
                  (desiniter-aidentp desiniter gcc-equiv)))
  :rule-classes :congruence)

Theorem: desiniter-list-aidentp-desiniter-list-equiv-congruence-on-desiniter-list

(defthm
 desiniter-list-aidentp-desiniter-list-equiv-congruence-on-desiniter-list
 (implies (desiniter-list-equiv desiniter-list desiniter-list-equiv)
          (equal (desiniter-list-aidentp desiniter-list gcc)
                 (desiniter-list-aidentp desiniter-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: desiniter-list-aidentp-iff-congruence-on-gcc

(defthm desiniter-list-aidentp-iff-congruence-on-gcc
 (implies (iff gcc gcc-equiv)
          (equal (desiniter-list-aidentp desiniter-list gcc)
                 (desiniter-list-aidentp desiniter-list gcc-equiv)))
 :rule-classes :congruence)

Theorem: designor-aidentp-designor-equiv-congruence-on-designor

(defthm designor-aidentp-designor-equiv-congruence-on-designor
  (implies (designor-equiv designor designor-equiv)
           (equal (designor-aidentp designor gcc)
                  (designor-aidentp designor-equiv gcc)))
  :rule-classes :congruence)

Theorem: designor-aidentp-iff-congruence-on-gcc

(defthm designor-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (designor-aidentp designor gcc)
                  (designor-aidentp designor gcc-equiv)))
  :rule-classes :congruence)

Theorem: designor-list-aidentp-designor-list-equiv-congruence-on-designor-list

(defthm
 designor-list-aidentp-designor-list-equiv-congruence-on-designor-list
 (implies (designor-list-equiv designor-list designor-list-equiv)
          (equal (designor-list-aidentp designor-list gcc)
                 (designor-list-aidentp designor-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: designor-list-aidentp-iff-congruence-on-gcc

(defthm designor-list-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (designor-list-aidentp designor-list gcc)
                  (designor-list-aidentp designor-list gcc-equiv)))
  :rule-classes :congruence)

Theorem: declor-aidentp-declor-equiv-congruence-on-declor

(defthm declor-aidentp-declor-equiv-congruence-on-declor
  (implies (declor-equiv declor declor-equiv)
           (equal (declor-aidentp declor gcc)
                  (declor-aidentp declor-equiv gcc)))
  :rule-classes :congruence)

Theorem: declor-aidentp-iff-congruence-on-gcc

(defthm declor-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (declor-aidentp declor gcc)
                  (declor-aidentp declor gcc-equiv)))
  :rule-classes :congruence)

Theorem: declor-option-aidentp-declor-option-equiv-congruence-on-declor-option

(defthm
 declor-option-aidentp-declor-option-equiv-congruence-on-declor-option
 (implies (declor-option-equiv declor-option declor-option-equiv)
          (equal (declor-option-aidentp declor-option gcc)
                 (declor-option-aidentp declor-option-equiv gcc)))
 :rule-classes :congruence)

Theorem: declor-option-aidentp-iff-congruence-on-gcc

(defthm declor-option-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (declor-option-aidentp declor-option gcc)
                  (declor-option-aidentp declor-option gcc-equiv)))
  :rule-classes :congruence)

Theorem: dirdeclor-aidentp-dirdeclor-equiv-congruence-on-dirdeclor

(defthm dirdeclor-aidentp-dirdeclor-equiv-congruence-on-dirdeclor
  (implies (dirdeclor-equiv dirdeclor dirdeclor-equiv)
           (equal (dirdeclor-aidentp dirdeclor gcc)
                  (dirdeclor-aidentp dirdeclor-equiv gcc)))
  :rule-classes :congruence)

Theorem: dirdeclor-aidentp-iff-congruence-on-gcc

(defthm dirdeclor-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (dirdeclor-aidentp dirdeclor gcc)
                  (dirdeclor-aidentp dirdeclor gcc-equiv)))
  :rule-classes :congruence)

Theorem: absdeclor-aidentp-absdeclor-equiv-congruence-on-absdeclor

(defthm absdeclor-aidentp-absdeclor-equiv-congruence-on-absdeclor
  (implies (absdeclor-equiv absdeclor absdeclor-equiv)
           (equal (absdeclor-aidentp absdeclor gcc)
                  (absdeclor-aidentp absdeclor-equiv gcc)))
  :rule-classes :congruence)

Theorem: absdeclor-aidentp-iff-congruence-on-gcc

(defthm absdeclor-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (absdeclor-aidentp absdeclor gcc)
                  (absdeclor-aidentp absdeclor gcc-equiv)))
  :rule-classes :congruence)

Theorem: absdeclor-option-aidentp-absdeclor-option-equiv-congruence-on-absdeclor-option

(defthm
 absdeclor-option-aidentp-absdeclor-option-equiv-congruence-on-absdeclor-option
 (implies
    (absdeclor-option-equiv absdeclor-option absdeclor-option-equiv)
    (equal (absdeclor-option-aidentp absdeclor-option gcc)
           (absdeclor-option-aidentp absdeclor-option-equiv gcc)))
 :rule-classes :congruence)

Theorem: absdeclor-option-aidentp-iff-congruence-on-gcc

(defthm absdeclor-option-aidentp-iff-congruence-on-gcc
 (implies
      (iff gcc gcc-equiv)
      (equal (absdeclor-option-aidentp absdeclor-option gcc)
             (absdeclor-option-aidentp absdeclor-option gcc-equiv)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-aidentp-dirabsdeclor-equiv-congruence-on-dirabsdeclor

(defthm
 dirabsdeclor-aidentp-dirabsdeclor-equiv-congruence-on-dirabsdeclor
 (implies (dirabsdeclor-equiv dirabsdeclor dirabsdeclor-equiv)
          (equal (dirabsdeclor-aidentp dirabsdeclor gcc)
                 (dirabsdeclor-aidentp dirabsdeclor-equiv gcc)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-aidentp-iff-congruence-on-gcc

(defthm dirabsdeclor-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (dirabsdeclor-aidentp dirabsdeclor gcc)
                  (dirabsdeclor-aidentp dirabsdeclor gcc-equiv)))
  :rule-classes :congruence)

Theorem: dirabsdeclor-option-aidentp-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor-option

(defthm
 dirabsdeclor-option-aidentp-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor-option
 (implies
  (dirabsdeclor-option-equiv dirabsdeclor-option
                             dirabsdeclor-option-equiv)
  (equal
       (dirabsdeclor-option-aidentp dirabsdeclor-option gcc)
       (dirabsdeclor-option-aidentp dirabsdeclor-option-equiv gcc)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-option-aidentp-iff-congruence-on-gcc

(defthm dirabsdeclor-option-aidentp-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal
       (dirabsdeclor-option-aidentp dirabsdeclor-option gcc)
       (dirabsdeclor-option-aidentp dirabsdeclor-option gcc-equiv)))
 :rule-classes :congruence)

Theorem: param-declon-aidentp-param-declon-equiv-congruence-on-param-declon

(defthm
 param-declon-aidentp-param-declon-equiv-congruence-on-param-declon
 (implies (param-declon-equiv param-declon param-declon-equiv)
          (equal (param-declon-aidentp param-declon gcc)
                 (param-declon-aidentp param-declon-equiv gcc)))
 :rule-classes :congruence)

Theorem: param-declon-aidentp-iff-congruence-on-gcc

(defthm param-declon-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (param-declon-aidentp param-declon gcc)
                  (param-declon-aidentp param-declon gcc-equiv)))
  :rule-classes :congruence)

Theorem: param-declon-list-aidentp-param-declon-list-equiv-congruence-on-param-declon-list

(defthm
 param-declon-list-aidentp-param-declon-list-equiv-congruence-on-param-declon-list
 (implies
    (param-declon-list-equiv param-declon-list
                             param-declon-list-equiv)
    (equal (param-declon-list-aidentp param-declon-list gcc)
           (param-declon-list-aidentp param-declon-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: param-declon-list-aidentp-iff-congruence-on-gcc

(defthm param-declon-list-aidentp-iff-congruence-on-gcc
 (implies
    (iff gcc gcc-equiv)
    (equal (param-declon-list-aidentp param-declon-list gcc)
           (param-declon-list-aidentp param-declon-list gcc-equiv)))
 :rule-classes :congruence)

Theorem: param-declor-aidentp-param-declor-equiv-congruence-on-param-declor

(defthm
 param-declor-aidentp-param-declor-equiv-congruence-on-param-declor
 (implies (param-declor-equiv param-declor param-declor-equiv)
          (equal (param-declor-aidentp param-declor gcc)
                 (param-declor-aidentp param-declor-equiv gcc)))
 :rule-classes :congruence)

Theorem: param-declor-aidentp-iff-congruence-on-gcc

(defthm param-declor-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (param-declor-aidentp param-declor gcc)
                  (param-declor-aidentp param-declor gcc-equiv)))
  :rule-classes :congruence)

Theorem: tyname-aidentp-tyname-equiv-congruence-on-tyname

(defthm tyname-aidentp-tyname-equiv-congruence-on-tyname
  (implies (tyname-equiv tyname tyname-equiv)
           (equal (tyname-aidentp tyname gcc)
                  (tyname-aidentp tyname-equiv gcc)))
  :rule-classes :congruence)

Theorem: tyname-aidentp-iff-congruence-on-gcc

(defthm tyname-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (tyname-aidentp tyname gcc)
                  (tyname-aidentp tyname gcc-equiv)))
  :rule-classes :congruence)

Theorem: struni-spec-aidentp-struni-spec-equiv-congruence-on-struni-spec

(defthm
    struni-spec-aidentp-struni-spec-equiv-congruence-on-struni-spec
  (implies (struni-spec-equiv struni-spec struni-spec-equiv)
           (equal (struni-spec-aidentp struni-spec gcc)
                  (struni-spec-aidentp struni-spec-equiv gcc)))
  :rule-classes :congruence)

Theorem: struni-spec-aidentp-iff-congruence-on-gcc

(defthm struni-spec-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (struni-spec-aidentp struni-spec gcc)
                  (struni-spec-aidentp struni-spec gcc-equiv)))
  :rule-classes :congruence)

Theorem: struct-declon-aidentp-struct-declon-equiv-congruence-on-struct-declon

(defthm
 struct-declon-aidentp-struct-declon-equiv-congruence-on-struct-declon
 (implies (struct-declon-equiv struct-declon struct-declon-equiv)
          (equal (struct-declon-aidentp struct-declon gcc)
                 (struct-declon-aidentp struct-declon-equiv gcc)))
 :rule-classes :congruence)

Theorem: struct-declon-aidentp-iff-congruence-on-gcc

(defthm struct-declon-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (struct-declon-aidentp struct-declon gcc)
                  (struct-declon-aidentp struct-declon gcc-equiv)))
  :rule-classes :congruence)

Theorem: struct-declon-list-aidentp-struct-declon-list-equiv-congruence-on-struct-declon-list

(defthm
 struct-declon-list-aidentp-struct-declon-list-equiv-congruence-on-struct-declon-list
 (implies
  (struct-declon-list-equiv struct-declon-list
                            struct-declon-list-equiv)
  (equal (struct-declon-list-aidentp struct-declon-list gcc)
         (struct-declon-list-aidentp struct-declon-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: struct-declon-list-aidentp-iff-congruence-on-gcc

(defthm struct-declon-list-aidentp-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal (struct-declon-list-aidentp struct-declon-list gcc)
         (struct-declon-list-aidentp struct-declon-list gcc-equiv)))
 :rule-classes :congruence)

Theorem: struct-declor-aidentp-struct-declor-equiv-congruence-on-struct-declor

(defthm
 struct-declor-aidentp-struct-declor-equiv-congruence-on-struct-declor
 (implies (struct-declor-equiv struct-declor struct-declor-equiv)
          (equal (struct-declor-aidentp struct-declor gcc)
                 (struct-declor-aidentp struct-declor-equiv gcc)))
 :rule-classes :congruence)

Theorem: struct-declor-aidentp-iff-congruence-on-gcc

(defthm struct-declor-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (struct-declor-aidentp struct-declor gcc)
                  (struct-declor-aidentp struct-declor gcc-equiv)))
  :rule-classes :congruence)

Theorem: struct-declor-list-aidentp-struct-declor-list-equiv-congruence-on-struct-declor-list

(defthm
 struct-declor-list-aidentp-struct-declor-list-equiv-congruence-on-struct-declor-list
 (implies
  (struct-declor-list-equiv struct-declor-list
                            struct-declor-list-equiv)
  (equal (struct-declor-list-aidentp struct-declor-list gcc)
         (struct-declor-list-aidentp struct-declor-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: struct-declor-list-aidentp-iff-congruence-on-gcc

(defthm struct-declor-list-aidentp-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal (struct-declor-list-aidentp struct-declor-list gcc)
         (struct-declor-list-aidentp struct-declor-list gcc-equiv)))
 :rule-classes :congruence)

Theorem: enum-spec-aidentp-enum-spec-equiv-congruence-on-enum-spec

(defthm enum-spec-aidentp-enum-spec-equiv-congruence-on-enum-spec
  (implies (enum-spec-equiv enum-spec enum-spec-equiv)
           (equal (enum-spec-aidentp enum-spec gcc)
                  (enum-spec-aidentp enum-spec-equiv gcc)))
  :rule-classes :congruence)

Theorem: enum-spec-aidentp-iff-congruence-on-gcc

(defthm enum-spec-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (enum-spec-aidentp enum-spec gcc)
                  (enum-spec-aidentp enum-spec gcc-equiv)))
  :rule-classes :congruence)

Theorem: enumer-aidentp-enumer-equiv-congruence-on-enumer

(defthm enumer-aidentp-enumer-equiv-congruence-on-enumer
  (implies (enumer-equiv enumer enumer-equiv)
           (equal (enumer-aidentp enumer gcc)
                  (enumer-aidentp enumer-equiv gcc)))
  :rule-classes :congruence)

Theorem: enumer-aidentp-iff-congruence-on-gcc

(defthm enumer-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (enumer-aidentp enumer gcc)
                  (enumer-aidentp enumer gcc-equiv)))
  :rule-classes :congruence)

Theorem: enumer-list-aidentp-enumer-list-equiv-congruence-on-enumer-list

(defthm
    enumer-list-aidentp-enumer-list-equiv-congruence-on-enumer-list
  (implies (enumer-list-equiv enumer-list enumer-list-equiv)
           (equal (enumer-list-aidentp enumer-list gcc)
                  (enumer-list-aidentp enumer-list-equiv gcc)))
  :rule-classes :congruence)

Theorem: enumer-list-aidentp-iff-congruence-on-gcc

(defthm enumer-list-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (enumer-list-aidentp enumer-list gcc)
                  (enumer-list-aidentp enumer-list gcc-equiv)))
  :rule-classes :congruence)

Theorem: statassert-aidentp-statassert-equiv-congruence-on-statassert

(defthm statassert-aidentp-statassert-equiv-congruence-on-statassert
  (implies (statassert-equiv statassert statassert-equiv)
           (equal (statassert-aidentp statassert gcc)
                  (statassert-aidentp statassert-equiv gcc)))
  :rule-classes :congruence)

Theorem: statassert-aidentp-iff-congruence-on-gcc

(defthm statassert-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (statassert-aidentp statassert gcc)
                  (statassert-aidentp statassert gcc-equiv)))
  :rule-classes :congruence)

Theorem: attrib-aidentp-attrib-equiv-congruence-on-attrib

(defthm attrib-aidentp-attrib-equiv-congruence-on-attrib
  (implies (attrib-equiv attrib attrib-equiv)
           (equal (attrib-aidentp attrib gcc)
                  (attrib-aidentp attrib-equiv gcc)))
  :rule-classes :congruence)

Theorem: attrib-aidentp-iff-congruence-on-gcc

(defthm attrib-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (attrib-aidentp attrib gcc)
                  (attrib-aidentp attrib gcc-equiv)))
  :rule-classes :congruence)

Theorem: attrib-list-aidentp-attrib-list-equiv-congruence-on-attrib-list

(defthm
    attrib-list-aidentp-attrib-list-equiv-congruence-on-attrib-list
  (implies (attrib-list-equiv attrib-list attrib-list-equiv)
           (equal (attrib-list-aidentp attrib-list gcc)
                  (attrib-list-aidentp attrib-list-equiv gcc)))
  :rule-classes :congruence)

Theorem: attrib-list-aidentp-iff-congruence-on-gcc

(defthm attrib-list-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (attrib-list-aidentp attrib-list gcc)
                  (attrib-list-aidentp attrib-list gcc-equiv)))
  :rule-classes :congruence)

Theorem: attrib-spec-aidentp-attrib-spec-equiv-congruence-on-attrib-spec

(defthm
    attrib-spec-aidentp-attrib-spec-equiv-congruence-on-attrib-spec
  (implies (attrib-spec-equiv attrib-spec attrib-spec-equiv)
           (equal (attrib-spec-aidentp attrib-spec gcc)
                  (attrib-spec-aidentp attrib-spec-equiv gcc)))
  :rule-classes :congruence)

Theorem: attrib-spec-aidentp-iff-congruence-on-gcc

(defthm attrib-spec-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (attrib-spec-aidentp attrib-spec gcc)
                  (attrib-spec-aidentp attrib-spec gcc-equiv)))
  :rule-classes :congruence)

Theorem: attrib-spec-list-aidentp-attrib-spec-list-equiv-congruence-on-attrib-spec-list

(defthm
 attrib-spec-list-aidentp-attrib-spec-list-equiv-congruence-on-attrib-spec-list
 (implies
    (attrib-spec-list-equiv attrib-spec-list attrib-spec-list-equiv)
    (equal (attrib-spec-list-aidentp attrib-spec-list gcc)
           (attrib-spec-list-aidentp attrib-spec-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: attrib-spec-list-aidentp-iff-congruence-on-gcc

(defthm attrib-spec-list-aidentp-iff-congruence-on-gcc
 (implies
      (iff gcc gcc-equiv)
      (equal (attrib-spec-list-aidentp attrib-spec-list gcc)
             (attrib-spec-list-aidentp attrib-spec-list gcc-equiv)))
 :rule-classes :congruence)

Theorem: init-declor-aidentp-init-declor-equiv-congruence-on-init-declor

(defthm
    init-declor-aidentp-init-declor-equiv-congruence-on-init-declor
  (implies (init-declor-equiv init-declor init-declor-equiv)
           (equal (init-declor-aidentp init-declor gcc)
                  (init-declor-aidentp init-declor-equiv gcc)))
  :rule-classes :congruence)

Theorem: init-declor-aidentp-iff-congruence-on-gcc

(defthm init-declor-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (init-declor-aidentp init-declor gcc)
                  (init-declor-aidentp init-declor gcc-equiv)))
  :rule-classes :congruence)

Theorem: init-declor-list-aidentp-init-declor-list-equiv-congruence-on-init-declor-list

(defthm
 init-declor-list-aidentp-init-declor-list-equiv-congruence-on-init-declor-list
 (implies
    (init-declor-list-equiv init-declor-list init-declor-list-equiv)
    (equal (init-declor-list-aidentp init-declor-list gcc)
           (init-declor-list-aidentp init-declor-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: init-declor-list-aidentp-iff-congruence-on-gcc

(defthm init-declor-list-aidentp-iff-congruence-on-gcc
 (implies
      (iff gcc gcc-equiv)
      (equal (init-declor-list-aidentp init-declor-list gcc)
             (init-declor-list-aidentp init-declor-list gcc-equiv)))
 :rule-classes :congruence)

Theorem: declon-aidentp-declon-equiv-congruence-on-declon

(defthm declon-aidentp-declon-equiv-congruence-on-declon
  (implies (declon-equiv declon declon-equiv)
           (equal (declon-aidentp declon gcc)
                  (declon-aidentp declon-equiv gcc)))
  :rule-classes :congruence)

Theorem: declon-aidentp-iff-congruence-on-gcc

(defthm declon-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (declon-aidentp declon gcc)
                  (declon-aidentp declon gcc-equiv)))
  :rule-classes :congruence)

Theorem: declon-list-aidentp-declon-list-equiv-congruence-on-declon-list

(defthm
    declon-list-aidentp-declon-list-equiv-congruence-on-declon-list
  (implies (declon-list-equiv declon-list declon-list-equiv)
           (equal (declon-list-aidentp declon-list gcc)
                  (declon-list-aidentp declon-list-equiv gcc)))
  :rule-classes :congruence)

Theorem: declon-list-aidentp-iff-congruence-on-gcc

(defthm declon-list-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (declon-list-aidentp declon-list gcc)
                  (declon-list-aidentp declon-list gcc-equiv)))
  :rule-classes :congruence)

Theorem: label-aidentp-label-equiv-congruence-on-label

(defthm label-aidentp-label-equiv-congruence-on-label
  (implies (label-equiv label label-equiv)
           (equal (label-aidentp label gcc)
                  (label-aidentp label-equiv gcc)))
  :rule-classes :congruence)

Theorem: label-aidentp-iff-congruence-on-gcc

(defthm label-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (label-aidentp label gcc)
                  (label-aidentp label gcc-equiv)))
  :rule-classes :congruence)

Theorem: asm-output-aidentp-asm-output-equiv-congruence-on-asm-output

(defthm asm-output-aidentp-asm-output-equiv-congruence-on-asm-output
  (implies (asm-output-equiv asm-output asm-output-equiv)
           (equal (asm-output-aidentp asm-output gcc)
                  (asm-output-aidentp asm-output-equiv gcc)))
  :rule-classes :congruence)

Theorem: asm-output-aidentp-iff-congruence-on-gcc

(defthm asm-output-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (asm-output-aidentp asm-output gcc)
                  (asm-output-aidentp asm-output gcc-equiv)))
  :rule-classes :congruence)

Theorem: asm-output-list-aidentp-asm-output-list-equiv-congruence-on-asm-output-list

(defthm
 asm-output-list-aidentp-asm-output-list-equiv-congruence-on-asm-output-list
 (implies
      (asm-output-list-equiv asm-output-list asm-output-list-equiv)
      (equal (asm-output-list-aidentp asm-output-list gcc)
             (asm-output-list-aidentp asm-output-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: asm-output-list-aidentp-iff-congruence-on-gcc

(defthm asm-output-list-aidentp-iff-congruence-on-gcc
  (implies
       (iff gcc gcc-equiv)
       (equal (asm-output-list-aidentp asm-output-list gcc)
              (asm-output-list-aidentp asm-output-list gcc-equiv)))
  :rule-classes :congruence)

Theorem: asm-input-aidentp-asm-input-equiv-congruence-on-asm-input

(defthm asm-input-aidentp-asm-input-equiv-congruence-on-asm-input
  (implies (asm-input-equiv asm-input asm-input-equiv)
           (equal (asm-input-aidentp asm-input gcc)
                  (asm-input-aidentp asm-input-equiv gcc)))
  :rule-classes :congruence)

Theorem: asm-input-aidentp-iff-congruence-on-gcc

(defthm asm-input-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (asm-input-aidentp asm-input gcc)
                  (asm-input-aidentp asm-input gcc-equiv)))
  :rule-classes :congruence)

Theorem: asm-input-list-aidentp-asm-input-list-equiv-congruence-on-asm-input-list

(defthm
 asm-input-list-aidentp-asm-input-list-equiv-congruence-on-asm-input-list
 (implies (asm-input-list-equiv asm-input-list asm-input-list-equiv)
          (equal (asm-input-list-aidentp asm-input-list gcc)
                 (asm-input-list-aidentp asm-input-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: asm-input-list-aidentp-iff-congruence-on-gcc

(defthm asm-input-list-aidentp-iff-congruence-on-gcc
 (implies (iff gcc gcc-equiv)
          (equal (asm-input-list-aidentp asm-input-list gcc)
                 (asm-input-list-aidentp asm-input-list gcc-equiv)))
 :rule-classes :congruence)

Theorem: asm-stmt-aidentp-asm-stmt-equiv-congruence-on-asm-stmt

(defthm asm-stmt-aidentp-asm-stmt-equiv-congruence-on-asm-stmt
  (implies (asm-stmt-equiv asm-stmt asm-stmt-equiv)
           (equal (asm-stmt-aidentp asm-stmt gcc)
                  (asm-stmt-aidentp asm-stmt-equiv gcc)))
  :rule-classes :congruence)

Theorem: asm-stmt-aidentp-iff-congruence-on-gcc

(defthm asm-stmt-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (asm-stmt-aidentp asm-stmt gcc)
                  (asm-stmt-aidentp asm-stmt gcc-equiv)))
  :rule-classes :congruence)

Theorem: stmt-aidentp-stmt-equiv-congruence-on-stmt

(defthm stmt-aidentp-stmt-equiv-congruence-on-stmt
  (implies (stmt-equiv stmt stmt-equiv)
           (equal (stmt-aidentp stmt gcc)
                  (stmt-aidentp stmt-equiv gcc)))
  :rule-classes :congruence)

Theorem: stmt-aidentp-iff-congruence-on-gcc

(defthm stmt-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (stmt-aidentp stmt gcc)
                  (stmt-aidentp stmt gcc-equiv)))
  :rule-classes :congruence)

Theorem: comp-stmt-aidentp-comp-stmt-equiv-congruence-on-comp-stmt

(defthm comp-stmt-aidentp-comp-stmt-equiv-congruence-on-comp-stmt
  (implies (comp-stmt-equiv comp-stmt comp-stmt-equiv)
           (equal (comp-stmt-aidentp comp-stmt gcc)
                  (comp-stmt-aidentp comp-stmt-equiv gcc)))
  :rule-classes :congruence)

Theorem: comp-stmt-aidentp-iff-congruence-on-gcc

(defthm comp-stmt-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (comp-stmt-aidentp comp-stmt gcc)
                  (comp-stmt-aidentp comp-stmt gcc-equiv)))
  :rule-classes :congruence)

Theorem: block-item-aidentp-block-item-equiv-congruence-on-block-item

(defthm block-item-aidentp-block-item-equiv-congruence-on-block-item
  (implies (block-item-equiv block-item block-item-equiv)
           (equal (block-item-aidentp block-item gcc)
                  (block-item-aidentp block-item-equiv gcc)))
  :rule-classes :congruence)

Theorem: block-item-aidentp-iff-congruence-on-gcc

(defthm block-item-aidentp-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (block-item-aidentp block-item gcc)
                  (block-item-aidentp block-item gcc-equiv)))
  :rule-classes :congruence)

Theorem: block-item-list-aidentp-block-item-list-equiv-congruence-on-block-item-list

(defthm
 block-item-list-aidentp-block-item-list-equiv-congruence-on-block-item-list
 (implies
      (block-item-list-equiv block-item-list block-item-list-equiv)
      (equal (block-item-list-aidentp block-item-list gcc)
             (block-item-list-aidentp block-item-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: block-item-list-aidentp-iff-congruence-on-gcc

(defthm block-item-list-aidentp-iff-congruence-on-gcc
  (implies
       (iff gcc gcc-equiv)
       (equal (block-item-list-aidentp block-item-list gcc)
              (block-item-list-aidentp block-item-list gcc-equiv)))
  :rule-classes :congruence)

Theorem: amb-expr/tyname-aidentp-amb-expr/tyname-equiv-congruence-on-amb-expr/tyname

(defthm
 amb-expr/tyname-aidentp-amb-expr/tyname-equiv-congruence-on-amb-expr/tyname
 (implies
      (amb-expr/tyname-equiv amb-expr/tyname amb-expr/tyname-equiv)
      (equal (amb-expr/tyname-aidentp amb-expr/tyname gcc)
             (amb-expr/tyname-aidentp amb-expr/tyname-equiv gcc)))
 :rule-classes :congruence)

Theorem: amb-expr/tyname-aidentp-iff-congruence-on-gcc

(defthm amb-expr/tyname-aidentp-iff-congruence-on-gcc
  (implies
       (iff gcc gcc-equiv)
       (equal (amb-expr/tyname-aidentp amb-expr/tyname gcc)
              (amb-expr/tyname-aidentp amb-expr/tyname gcc-equiv)))
  :rule-classes :congruence)

Theorem: amb-declor/absdeclor-aidentp-amb-declor/absdeclor-equiv-congruence-on-amb-declor/absdeclor

(defthm
 amb-declor/absdeclor-aidentp-amb-declor/absdeclor-equiv-congruence-on-amb-declor/absdeclor
 (implies
  (amb-declor/absdeclor-equiv amb-declor/absdeclor
                              amb-declor/absdeclor-equiv)
  (equal
     (amb-declor/absdeclor-aidentp amb-declor/absdeclor gcc)
     (amb-declor/absdeclor-aidentp amb-declor/absdeclor-equiv gcc)))
 :rule-classes :congruence)

Theorem: amb-declor/absdeclor-aidentp-iff-congruence-on-gcc

(defthm amb-declor/absdeclor-aidentp-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal
     (amb-declor/absdeclor-aidentp amb-declor/absdeclor gcc)
     (amb-declor/absdeclor-aidentp amb-declor/absdeclor gcc-equiv)))
 :rule-classes :congruence)

Theorem: amb-declon/stmt-aidentp-amb-declon/stmt-equiv-congruence-on-amb-declon/stmt

(defthm
 amb-declon/stmt-aidentp-amb-declon/stmt-equiv-congruence-on-amb-declon/stmt
 (implies
      (amb-declon/stmt-equiv amb-declon/stmt amb-declon/stmt-equiv)
      (equal (amb-declon/stmt-aidentp amb-declon/stmt gcc)
             (amb-declon/stmt-aidentp amb-declon/stmt-equiv gcc)))
 :rule-classes :congruence)

Theorem: amb-declon/stmt-aidentp-iff-congruence-on-gcc

(defthm amb-declon/stmt-aidentp-iff-congruence-on-gcc
  (implies
       (iff gcc gcc-equiv)
       (equal (amb-declon/stmt-aidentp amb-declon/stmt gcc)
              (amb-declon/stmt-aidentp amb-declon/stmt gcc-equiv)))
  :rule-classes :congruence)