		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-annop

Exprs/decls/stmts-annop

Definitions and Theorems

Function: expr-annop

(defun expr-annop (expr)
 (declare (xargs :guard (exprp expr)))
 (declare (ignorable expr))
 (let ((__function__ 'expr-annop))
  (declare (ignorable __function__))
  (expr-case
    expr
    :ident (var-infop expr.info)
    :const (and (const-annop expr.const)
                (expr-const-infop expr.info))
    :string (expr-string-infop expr.info)
    :paren (expr-annop (expr-paren->inner expr))
    :gensel (and (expr-annop (expr-gensel->control expr))
                 (genassoc-list-annop (expr-gensel->assocs expr)))
    :arrsub (and (expr-annop expr.arg1)
                 (expr-annop expr.arg2)
                 (expr-arrsub-infop expr.info))
    :funcall (and (expr-annop expr.fun)
                  (expr-list-annop expr.args)
                  (expr-funcall-infop expr.info))
    :member (and (expr-annop (expr-member->arg expr))
                 (ident-annop (expr-member->name expr)))
    :memberp (and (expr-annop (expr-memberp->arg expr))
                  (ident-annop (expr-memberp->name expr)))
    :complit (and (tyname-annop (expr-complit->type expr))
                  (desiniter-list-annop (expr-complit->elems expr)))
    :unary (and (expr-annop expr.arg)
                (expr-unary-infop expr.info))
    :label-addr (ident-annop (expr-label-addr->arg expr))
    :sizeof (tyname-annop (expr-sizeof->type expr))
    :sizeof-ambig (raise "Internal error: ambiguous ~x0."
                         (expr-fix expr))
    :alignof (tyname-annop (expr-alignof->type expr))
    :alignof-ambig (raise "Internal error: ambiguous ~x0."
                          (expr-fix expr))
    :cast (and (tyname-annop (expr-cast->type expr))
               (expr-annop (expr-cast->arg expr)))
    :binary (and (expr-annop expr.arg1)
                 (expr-annop expr.arg2)
                 (expr-binary-infop expr.info))
    :cond (and (expr-annop (expr-cond->test expr))
               (and (expr-option-annop (expr-cond->then expr))
                    (expr-annop (expr-cond->else expr))))
    :comma (and (expr-annop (expr-comma->first expr))
                (expr-annop (expr-comma->next expr)))
    :cast/call-ambig (raise "Internal error: ambiguous ~x0."
                            (expr-fix expr))
    :cast/mul-ambig (raise "Internal error: ambiguous ~x0."
                           (expr-fix expr))
    :cast/add-ambig (raise "Internal error: ambiguous ~x0."
                           (expr-fix expr))
    :cast/sub-ambig (raise "Internal error: ambiguous ~x0."
                           (expr-fix expr))
    :cast/and-ambig (raise "Internal error: ambiguous ~x0."
                           (expr-fix expr))
    :cast/logand-ambig (raise "Internal error: ambiguous ~x0."
                              (expr-fix expr))
    :stmt (comp-stmt-annop (expr-stmt->stmt expr))
    :tycompat (and (tyname-annop (expr-tycompat->type1 expr))
                   (tyname-annop (expr-tycompat->type2 expr)))
    :offsetof
    (and (tyname-annop (expr-offsetof->type expr))
         (member-designor-annop (expr-offsetof->member expr)))
    :va-arg (and (expr-annop (expr-va-arg->list expr))
                 (tyname-annop (expr-va-arg->type expr)))
    :extension (expr-annop (expr-extension->expr expr)))))

Function: expr-list-annop

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

Function: expr-option-annop

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

Function: const-expr-annop

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

Function: const-expr-option-annop

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

Function: genassoc-annop

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

Function: genassoc-list-annop

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

Function: member-designor-annop

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

Function: type-spec-annop

(defun type-spec-annop (type-spec)
 (declare (xargs :guard (type-specp type-spec)))
 (declare (ignorable type-spec))
 (let ((__function__ 'type-spec-annop))
  (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-annop (type-spec-atomic->type type-spec))
   :struct (struni-spec-annop (type-spec-struct->spec type-spec))
   :union (struni-spec-annop (type-spec-union->spec type-spec))
   :enum (enum-spec-annop (type-spec-enum->spec type-spec))
   :typedef (ident-annop (type-spec-typedef->name type-spec))
   :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-annop
          (type-spec-struct-empty->attribs type-spec))
     (ident-option-annop (type-spec-struct-empty->name? type-spec)))
   :typeof-expr (expr-annop (type-spec-typeof-expr->expr type-spec))
   :typeof-type
   (tyname-annop (type-spec-typeof-type->type type-spec))
   :typeof-ambig (raise "Internal error: ambiguous ~x0."
                        (type-spec-fix type-spec))
   :auto-type t)))

Function: spec/qual-annop

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

Function: spec/qual-list-annop

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

Function: align-spec-annop

(defun align-spec-annop (align-spec)
 (declare (xargs :guard (align-specp align-spec)))
 (declare (ignorable align-spec))
 (let ((__function__ 'align-spec-annop))
  (declare (ignorable __function__))
  (align-spec-case
       align-spec
       :alignas-type
       (tyname-annop (align-spec-alignas-type->type align-spec))
       :alignas-expr
       (const-expr-annop (align-spec-alignas-expr->expr align-spec))
       :alignas-ambig (raise "Internal error: ambiguous ~x0."
                             (align-spec-fix align-spec)))))

Function: decl-spec-annop

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

Function: decl-spec-list-annop

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

Function: typequal/attribspec-annop

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

Function: typequal/attribspec-list-annop

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

Function: typequal/attribspec-list-list-annop

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

Function: initer-annop

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

Function: initer-option-annop

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

Function: desiniter-annop

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

Function: desiniter-list-annop

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

Function: designor-annop

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

Function: designor-list-annop

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

Function: declor-annop

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

Function: declor-option-annop

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

Function: dirdeclor-annop

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

Function: absdeclor-annop

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

Function: absdeclor-option-annop

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

Function: dirabsdeclor-annop

(defun dirabsdeclor-annop (dirabsdeclor)
 (declare (xargs :guard (dirabsdeclorp dirabsdeclor)))
 (declare (ignorable dirabsdeclor))
 (let ((__function__ 'dirabsdeclor-annop))
  (declare (ignorable __function__))
  (dirabsdeclor-case
   dirabsdeclor
   :dummy-base
   (raise
    "Internal error: ~
                                       dummy base case of ~
                                       direct abstract declarator.")
   :paren (absdeclor-annop (dirabsdeclor-paren->inner dirabsdeclor))
   :array
   (and
    (dirabsdeclor-option-annop
         (dirabsdeclor-array->declor? dirabsdeclor))
    (and
      (typequal/attribspec-list-annop
           (dirabsdeclor-array->qualspecs dirabsdeclor))
      (expr-option-annop (dirabsdeclor-array->size? dirabsdeclor))))
   :array-static1
   (and
    (dirabsdeclor-option-annop
         (dirabsdeclor-array-static1->declor? dirabsdeclor))
    (and
      (typequal/attribspec-list-annop
           (dirabsdeclor-array-static1->qualspecs dirabsdeclor))
      (expr-annop (dirabsdeclor-array-static1->size dirabsdeclor))))
   :array-static2
   (and
    (dirabsdeclor-option-annop
         (dirabsdeclor-array-static2->declor? dirabsdeclor))
    (and
      (typequal/attribspec-list-annop
           (dirabsdeclor-array-static2->qualspecs dirabsdeclor))
      (expr-annop (dirabsdeclor-array-static2->size dirabsdeclor))))
   :array-star (dirabsdeclor-option-annop
                    (dirabsdeclor-array-star->declor? dirabsdeclor))
   :function
   (and (dirabsdeclor-option-annop
             (dirabsdeclor-function->declor? dirabsdeclor))
        (param-declon-list-annop
             (dirabsdeclor-function->params dirabsdeclor))))))

Function: dirabsdeclor-option-annop

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

Function: param-declon-annop

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

Function: param-declon-list-annop

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

Function: param-declor-annop

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

Function: tyname-annop

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

Function: struni-spec-annop

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

Function: struct-declon-annop

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

Function: struct-declon-list-annop

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

Function: struct-declor-annop

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

Function: struct-declor-list-annop

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

Function: enum-spec-annop

(defun enum-spec-annop (enum-spec)
  (declare (xargs :guard (enum-specp enum-spec)))
  (declare (ignorable enum-spec))
  (let ((__function__ 'enum-spec-annop))
    (declare (ignorable __function__))
    (and (ident-option-annop (enum-spec->name enum-spec))
         (enumer-list-annop (enum-spec->list enum-spec)))))

Function: enumer-annop

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

Function: enumer-list-annop

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

Function: statassert-annop

(defun statassert-annop (statassert)
  (declare (xargs :guard (statassertp statassert)))
  (declare (ignorable statassert))
  (let ((__function__ 'statassert-annop))
    (declare (ignorable __function__))
    (const-expr-annop (statassert->test statassert))))

Function: attrib-annop

(defun attrib-annop (attrib)
  (declare (xargs :guard (attribp attrib)))
  (declare (ignorable attrib))
  (let ((__function__ 'attrib-annop))
    (declare (ignorable __function__))
    t))

Function: attrib-list-annop

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

Function: attrib-spec-annop

(defun attrib-spec-annop (attrib-spec)
  (declare (xargs :guard (attrib-specp attrib-spec)))
  (declare (ignorable attrib-spec))
  (let ((__function__ 'attrib-spec-annop))
    (declare (ignorable __function__))
    t))

Function: attrib-spec-list-annop

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

Function: initdeclor-annop

(defun initdeclor-annop (initdeclor)
  (declare (xargs :guard (initdeclorp initdeclor)))
  (declare (ignorable initdeclor))
  (let ((__function__ 'initdeclor-annop))
    (declare (ignorable __function__))
    (and (declor-annop (initdeclor->declor initdeclor))
         (initer-option-annop (initdeclor->init? initdeclor))
         (initdeclor-infop (initdeclor->info initdeclor)))))

Function: initdeclor-list-annop

(defun initdeclor-list-annop (initdeclor-list)
  (declare (xargs :guard (initdeclor-listp initdeclor-list)))
  (let ((__function__ 'initdeclor-list-annop))
    (declare (ignorable __function__))
    (cond ((endp initdeclor-list) t)
          (t (and (initdeclor-annop (car initdeclor-list))
                  (initdeclor-list-annop (cdr initdeclor-list)))))))

Function: decl-annop

(defun decl-annop (decl)
  (declare (xargs :guard (declp decl)))
  (declare (ignorable decl))
  (let ((__function__ 'decl-annop))
    (declare (ignorable __function__))
    (decl-case
         decl
         :decl (and (decl-spec-list-annop (decl-decl->specs decl))
                    (initdeclor-list-annop (decl-decl->init decl)))
         :statassert
         (statassert-annop (decl-statassert->statassert decl)))))

Function: decl-list-annop

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

Function: label-annop

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

Function: asm-output-annop

(defun asm-output-annop (asm-output)
  (declare (xargs :guard (asm-outputp asm-output)))
  (declare (ignorable asm-output))
  (let ((__function__ 'asm-output-annop))
    (declare (ignorable __function__))
    t))

Function: asm-output-list-annop

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

Function: asm-input-annop

(defun asm-input-annop (asm-input)
  (declare (xargs :guard (asm-inputp asm-input)))
  (declare (ignorable asm-input))
  (let ((__function__ 'asm-input-annop))
    (declare (ignorable __function__))
    t))

Function: asm-input-list-annop

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

Function: asm-stmt-annop

(defun asm-stmt-annop (asm-stmt)
  (declare (xargs :guard (asm-stmtp asm-stmt)))
  (declare (ignorable asm-stmt))
  (let ((__function__ 'asm-stmt-annop))
    (declare (ignorable __function__))
    t))

Function: stmt-annop

(defun stmt-annop (stmt)
 (declare (xargs :guard (stmtp stmt)))
 (declare (ignorable stmt))
 (let ((__function__ 'stmt-annop))
  (declare (ignorable __function__))
  (stmt-case
       stmt
       :labeled (and (label-annop (stmt-labeled->label stmt))
                     (stmt-annop (stmt-labeled->stmt stmt)))
       :compound (comp-stmt-annop (stmt-compound->stmt stmt))
       :expr (expr-option-annop (stmt-expr->expr? stmt))
       :if (and (expr-annop (stmt-if->test stmt))
                (stmt-annop (stmt-if->then stmt)))
       :ifelse (and (expr-annop (stmt-ifelse->test stmt))
                    (and (stmt-annop (stmt-ifelse->then stmt))
                         (stmt-annop (stmt-ifelse->else stmt))))
       :switch (and (expr-annop (stmt-switch->target stmt))
                    (stmt-annop (stmt-switch->body stmt)))
       :while (and (expr-annop (stmt-while->test stmt))
                   (stmt-annop (stmt-while->body stmt)))
       :dowhile (and (stmt-annop (stmt-dowhile->body stmt))
                     (expr-annop (stmt-dowhile->test stmt)))
       :for-expr
       (and (expr-option-annop (stmt-for-expr->init stmt))
            (and (expr-option-annop (stmt-for-expr->test stmt))
                 (and (expr-option-annop (stmt-for-expr->next stmt))
                      (stmt-annop (stmt-for-expr->body stmt)))))
       :for-decl
       (and (decl-annop (stmt-for-decl->init stmt))
            (and (expr-option-annop (stmt-for-decl->test stmt))
                 (and (expr-option-annop (stmt-for-decl->next stmt))
                      (stmt-annop (stmt-for-decl->body stmt)))))
       :for-ambig (raise "Internal error: ambiguous ~x0."
                         (stmt-fix stmt))
       :goto (ident-annop (stmt-goto->label stmt))
       :gotoe (expr-annop (stmt-gotoe->label stmt))
       :continue t
       :break t
       :return (expr-option-annop (stmt-return->expr? stmt))
       :asm (asm-stmt-annop (stmt-asm->stmt stmt)))))

Function: comp-stmt-annop

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

Function: block-item-annop

(defun block-item-annop (block-item)
  (declare (xargs :guard (block-itemp block-item)))
  (declare (ignorable block-item))
  (let ((__function__ 'block-item-annop))
    (declare (ignorable __function__))
    (block-item-case
         block-item
         :decl (decl-annop (block-item-decl->decl block-item))
         :stmt (stmt-annop (block-item-stmt->stmt block-item))
         :ambig (raise "Internal error: ambiguous ~x0."
                       (block-item-fix block-item)))))

Function: block-item-list-annop

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

Function: amb-expr/tyname-annop

(defun amb-expr/tyname-annop (amb-expr/tyname)
  (declare (xargs :guard (amb-expr/tyname-p amb-expr/tyname)))
  (declare (ignorable amb-expr/tyname))
  (let ((__function__ 'amb-expr/tyname-annop))
    (declare (ignorable __function__))
    (raise "Internal error: ambiguous ~x0."
           (amb-expr/tyname-fix amb-expr/tyname))))

Function: amb-declor/absdeclor-annop

(defun amb-declor/absdeclor-annop (amb-declor/absdeclor)
  (declare
       (xargs :guard (amb-declor/absdeclor-p amb-declor/absdeclor)))
  (declare (ignorable amb-declor/absdeclor))
  (let ((__function__ 'amb-declor/absdeclor-annop))
    (declare (ignorable __function__))
    (raise "Internal error: ambiguous ~x0."
           (amb-declor/absdeclor-fix amb-declor/absdeclor))))

Function: amb-decl/stmt-annop

(defun amb-decl/stmt-annop (amb-decl/stmt)
  (declare (xargs :guard (amb-decl/stmt-p amb-decl/stmt)))
  (declare (ignorable amb-decl/stmt))
  (let ((__function__ 'amb-decl/stmt-annop))
    (declare (ignorable __function__))
    (raise "Internal error: ambiguous ~x0."
           (amb-decl/stmt-fix amb-decl/stmt))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: return-type-of-initdeclor-annop.result

(defthm return-type-of-initdeclor-annop.result
  (b* ((fty::?result (initdeclor-annop initdeclor)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-initdeclor-list-annop.result

(defthm return-type-of-initdeclor-list-annop.result
  (b* ((fty::?result (initdeclor-list-annop initdeclor-list)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: return-type-of-decl-annop.result

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

Theorem: return-type-of-decl-list-annop.result

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: expr-annop-of-expr-fix-expr

(defthm expr-annop-of-expr-fix-expr
  (equal (expr-annop (expr-fix expr))
         (expr-annop expr)))

Theorem: expr-list-annop-of-expr-list-fix-expr-list

(defthm expr-list-annop-of-expr-list-fix-expr-list
  (equal (expr-list-annop (expr-list-fix expr-list))
         (expr-list-annop expr-list)))

Theorem: expr-option-annop-of-expr-option-fix-expr-option

(defthm expr-option-annop-of-expr-option-fix-expr-option
  (equal (expr-option-annop (expr-option-fix expr-option))
         (expr-option-annop expr-option)))

Theorem: const-expr-annop-of-const-expr-fix-const-expr

(defthm const-expr-annop-of-const-expr-fix-const-expr
  (equal (const-expr-annop (const-expr-fix const-expr))
         (const-expr-annop const-expr)))

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

(defthm
 const-expr-option-annop-of-const-expr-option-fix-const-expr-option
 (equal (const-expr-option-annop
             (const-expr-option-fix const-expr-option))
        (const-expr-option-annop const-expr-option)))

Theorem: genassoc-annop-of-genassoc-fix-genassoc

(defthm genassoc-annop-of-genassoc-fix-genassoc
  (equal (genassoc-annop (genassoc-fix genassoc))
         (genassoc-annop genassoc)))

Theorem: genassoc-list-annop-of-genassoc-list-fix-genassoc-list

(defthm genassoc-list-annop-of-genassoc-list-fix-genassoc-list
  (equal (genassoc-list-annop (genassoc-list-fix genassoc-list))
         (genassoc-list-annop genassoc-list)))

Theorem: member-designor-annop-of-member-designor-fix-member-designor

(defthm member-designor-annop-of-member-designor-fix-member-designor
  (equal
       (member-designor-annop (member-designor-fix member-designor))
       (member-designor-annop member-designor)))

Theorem: type-spec-annop-of-type-spec-fix-type-spec

(defthm type-spec-annop-of-type-spec-fix-type-spec
  (equal (type-spec-annop (type-spec-fix type-spec))
         (type-spec-annop type-spec)))

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

(defthm spec/qual-annop-of-spec/qual-fix-spec/qual
  (equal (spec/qual-annop (spec/qual-fix spec/qual))
         (spec/qual-annop spec/qual)))

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

(defthm spec/qual-list-annop-of-spec/qual-list-fix-spec/qual-list
  (equal (spec/qual-list-annop (spec/qual-list-fix spec/qual-list))
         (spec/qual-list-annop spec/qual-list)))

Theorem: align-spec-annop-of-align-spec-fix-align-spec

(defthm align-spec-annop-of-align-spec-fix-align-spec
  (equal (align-spec-annop (align-spec-fix align-spec))
         (align-spec-annop align-spec)))

Theorem: decl-spec-annop-of-decl-spec-fix-decl-spec

(defthm decl-spec-annop-of-decl-spec-fix-decl-spec
  (equal (decl-spec-annop (decl-spec-fix decl-spec))
         (decl-spec-annop decl-spec)))

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

(defthm decl-spec-list-annop-of-decl-spec-list-fix-decl-spec-list
  (equal (decl-spec-list-annop (decl-spec-list-fix decl-spec-list))
         (decl-spec-list-annop decl-spec-list)))

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

(defthm
 typequal/attribspec-annop-of-typequal/attribspec-fix-typequal/attribspec
 (equal (typequal/attribspec-annop
             (typequal/attribspec-fix typequal/attribspec))
        (typequal/attribspec-annop typequal/attribspec)))

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

(defthm
 typequal/attribspec-list-annop-of-typequal/attribspec-list-fix-typequal/attribspec-list
 (equal
      (typequal/attribspec-list-annop
           (typequal/attribspec-list-fix typequal/attribspec-list))
      (typequal/attribspec-list-annop typequal/attribspec-list)))

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

(defthm
 typequal/attribspec-list-list-annop-of-typequal/attribspec-list-list-fix-typequal/attribspec-list-list
 (equal (typequal/attribspec-list-list-annop
             (typequal/attribspec-list-list-fix
                  typequal/attribspec-list-list))
        (typequal/attribspec-list-list-annop
             typequal/attribspec-list-list)))

Theorem: initer-annop-of-initer-fix-initer

(defthm initer-annop-of-initer-fix-initer
  (equal (initer-annop (initer-fix initer))
         (initer-annop initer)))

Theorem: initer-option-annop-of-initer-option-fix-initer-option

(defthm initer-option-annop-of-initer-option-fix-initer-option
  (equal (initer-option-annop (initer-option-fix initer-option))
         (initer-option-annop initer-option)))

Theorem: desiniter-annop-of-desiniter-fix-desiniter

(defthm desiniter-annop-of-desiniter-fix-desiniter
  (equal (desiniter-annop (desiniter-fix desiniter))
         (desiniter-annop desiniter)))

Theorem: desiniter-list-annop-of-desiniter-list-fix-desiniter-list

(defthm desiniter-list-annop-of-desiniter-list-fix-desiniter-list
  (equal (desiniter-list-annop (desiniter-list-fix desiniter-list))
         (desiniter-list-annop desiniter-list)))

Theorem: designor-annop-of-designor-fix-designor

(defthm designor-annop-of-designor-fix-designor
  (equal (designor-annop (designor-fix designor))
         (designor-annop designor)))

Theorem: designor-list-annop-of-designor-list-fix-designor-list

(defthm designor-list-annop-of-designor-list-fix-designor-list
  (equal (designor-list-annop (designor-list-fix designor-list))
         (designor-list-annop designor-list)))

Theorem: declor-annop-of-declor-fix-declor

(defthm declor-annop-of-declor-fix-declor
  (equal (declor-annop (declor-fix declor))
         (declor-annop declor)))

Theorem: declor-option-annop-of-declor-option-fix-declor-option

(defthm declor-option-annop-of-declor-option-fix-declor-option
  (equal (declor-option-annop (declor-option-fix declor-option))
         (declor-option-annop declor-option)))

Theorem: dirdeclor-annop-of-dirdeclor-fix-dirdeclor

(defthm dirdeclor-annop-of-dirdeclor-fix-dirdeclor
  (equal (dirdeclor-annop (dirdeclor-fix dirdeclor))
         (dirdeclor-annop dirdeclor)))

Theorem: absdeclor-annop-of-absdeclor-fix-absdeclor

(defthm absdeclor-annop-of-absdeclor-fix-absdeclor
  (equal (absdeclor-annop (absdeclor-fix absdeclor))
         (absdeclor-annop absdeclor)))

Theorem: absdeclor-option-annop-of-absdeclor-option-fix-absdeclor-option

(defthm
    absdeclor-option-annop-of-absdeclor-option-fix-absdeclor-option
 (equal
    (absdeclor-option-annop (absdeclor-option-fix absdeclor-option))
    (absdeclor-option-annop absdeclor-option)))

Theorem: dirabsdeclor-annop-of-dirabsdeclor-fix-dirabsdeclor

(defthm dirabsdeclor-annop-of-dirabsdeclor-fix-dirabsdeclor
  (equal (dirabsdeclor-annop (dirabsdeclor-fix dirabsdeclor))
         (dirabsdeclor-annop dirabsdeclor)))

Theorem: dirabsdeclor-option-annop-of-dirabsdeclor-option-fix-dirabsdeclor-option

(defthm
 dirabsdeclor-option-annop-of-dirabsdeclor-option-fix-dirabsdeclor-option
 (equal (dirabsdeclor-option-annop
             (dirabsdeclor-option-fix dirabsdeclor-option))
        (dirabsdeclor-option-annop dirabsdeclor-option)))

Theorem: param-declon-annop-of-param-declon-fix-param-declon

(defthm param-declon-annop-of-param-declon-fix-param-declon
  (equal (param-declon-annop (param-declon-fix param-declon))
         (param-declon-annop param-declon)))

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

(defthm
 param-declon-list-annop-of-param-declon-list-fix-param-declon-list
 (equal (param-declon-list-annop
             (param-declon-list-fix param-declon-list))
        (param-declon-list-annop param-declon-list)))

Theorem: param-declor-annop-of-param-declor-fix-param-declor

(defthm param-declor-annop-of-param-declor-fix-param-declor
  (equal (param-declor-annop (param-declor-fix param-declor))
         (param-declor-annop param-declor)))

Theorem: tyname-annop-of-tyname-fix-tyname

(defthm tyname-annop-of-tyname-fix-tyname
  (equal (tyname-annop (tyname-fix tyname))
         (tyname-annop tyname)))

Theorem: struni-spec-annop-of-struni-spec-fix-struni-spec

(defthm struni-spec-annop-of-struni-spec-fix-struni-spec
  (equal (struni-spec-annop (struni-spec-fix struni-spec))
         (struni-spec-annop struni-spec)))

Theorem: struct-declon-annop-of-struct-declon-fix-struct-declon

(defthm struct-declon-annop-of-struct-declon-fix-struct-declon
  (equal (struct-declon-annop (struct-declon-fix struct-declon))
         (struct-declon-annop struct-declon)))

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

(defthm
 struct-declon-list-annop-of-struct-declon-list-fix-struct-declon-list
 (equal (struct-declon-list-annop
             (struct-declon-list-fix struct-declon-list))
        (struct-declon-list-annop struct-declon-list)))

Theorem: struct-declor-annop-of-struct-declor-fix-struct-declor

(defthm struct-declor-annop-of-struct-declor-fix-struct-declor
  (equal (struct-declor-annop (struct-declor-fix struct-declor))
         (struct-declor-annop struct-declor)))

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

(defthm
 struct-declor-list-annop-of-struct-declor-list-fix-struct-declor-list
 (equal (struct-declor-list-annop
             (struct-declor-list-fix struct-declor-list))
        (struct-declor-list-annop struct-declor-list)))

Theorem: enum-spec-annop-of-enum-spec-fix-enum-spec

(defthm enum-spec-annop-of-enum-spec-fix-enum-spec
  (equal (enum-spec-annop (enum-spec-fix enum-spec))
         (enum-spec-annop enum-spec)))

Theorem: enumer-annop-of-enumer-fix-enumer

(defthm enumer-annop-of-enumer-fix-enumer
  (equal (enumer-annop (enumer-fix enumer))
         (enumer-annop enumer)))

Theorem: enumer-list-annop-of-enumer-list-fix-enumer-list

(defthm enumer-list-annop-of-enumer-list-fix-enumer-list
  (equal (enumer-list-annop (enumer-list-fix enumer-list))
         (enumer-list-annop enumer-list)))

Theorem: statassert-annop-of-statassert-fix-statassert

(defthm statassert-annop-of-statassert-fix-statassert
  (equal (statassert-annop (statassert-fix statassert))
         (statassert-annop statassert)))

Theorem: attrib-annop-of-attrib-fix-attrib

(defthm attrib-annop-of-attrib-fix-attrib
  (equal (attrib-annop (attrib-fix attrib))
         (attrib-annop attrib)))

Theorem: attrib-list-annop-of-attrib-list-fix-attrib-list

(defthm attrib-list-annop-of-attrib-list-fix-attrib-list
  (equal (attrib-list-annop (attrib-list-fix attrib-list))
         (attrib-list-annop attrib-list)))

Theorem: attrib-spec-annop-of-attrib-spec-fix-attrib-spec

(defthm attrib-spec-annop-of-attrib-spec-fix-attrib-spec
  (equal (attrib-spec-annop (attrib-spec-fix attrib-spec))
         (attrib-spec-annop attrib-spec)))

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

(defthm
    attrib-spec-list-annop-of-attrib-spec-list-fix-attrib-spec-list
 (equal
    (attrib-spec-list-annop (attrib-spec-list-fix attrib-spec-list))
    (attrib-spec-list-annop attrib-spec-list)))

Theorem: initdeclor-annop-of-initdeclor-fix-initdeclor

(defthm initdeclor-annop-of-initdeclor-fix-initdeclor
  (equal (initdeclor-annop (initdeclor-fix initdeclor))
         (initdeclor-annop initdeclor)))

Theorem: initdeclor-list-annop-of-initdeclor-list-fix-initdeclor-list

(defthm initdeclor-list-annop-of-initdeclor-list-fix-initdeclor-list
  (equal
       (initdeclor-list-annop (initdeclor-list-fix initdeclor-list))
       (initdeclor-list-annop initdeclor-list)))

Theorem: decl-annop-of-decl-fix-decl

(defthm decl-annop-of-decl-fix-decl
  (equal (decl-annop (decl-fix decl))
         (decl-annop decl)))

Theorem: decl-list-annop-of-decl-list-fix-decl-list

(defthm decl-list-annop-of-decl-list-fix-decl-list
  (equal (decl-list-annop (decl-list-fix decl-list))
         (decl-list-annop decl-list)))

Theorem: label-annop-of-label-fix-label

(defthm label-annop-of-label-fix-label
  (equal (label-annop (label-fix label))
         (label-annop label)))

Theorem: asm-output-annop-of-asm-output-fix-asm-output

(defthm asm-output-annop-of-asm-output-fix-asm-output
  (equal (asm-output-annop (asm-output-fix asm-output))
         (asm-output-annop asm-output)))

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

(defthm asm-output-list-annop-of-asm-output-list-fix-asm-output-list
  (equal
       (asm-output-list-annop (asm-output-list-fix asm-output-list))
       (asm-output-list-annop asm-output-list)))

Theorem: asm-input-annop-of-asm-input-fix-asm-input

(defthm asm-input-annop-of-asm-input-fix-asm-input
  (equal (asm-input-annop (asm-input-fix asm-input))
         (asm-input-annop asm-input)))

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

(defthm asm-input-list-annop-of-asm-input-list-fix-asm-input-list
  (equal (asm-input-list-annop (asm-input-list-fix asm-input-list))
         (asm-input-list-annop asm-input-list)))

Theorem: asm-stmt-annop-of-asm-stmt-fix-asm-stmt

(defthm asm-stmt-annop-of-asm-stmt-fix-asm-stmt
  (equal (asm-stmt-annop (asm-stmt-fix asm-stmt))
         (asm-stmt-annop asm-stmt)))

Theorem: stmt-annop-of-stmt-fix-stmt

(defthm stmt-annop-of-stmt-fix-stmt
  (equal (stmt-annop (stmt-fix stmt))
         (stmt-annop stmt)))

Theorem: comp-stmt-annop-of-comp-stmt-fix-comp-stmt

(defthm comp-stmt-annop-of-comp-stmt-fix-comp-stmt
  (equal (comp-stmt-annop (comp-stmt-fix comp-stmt))
         (comp-stmt-annop comp-stmt)))

Theorem: block-item-annop-of-block-item-fix-block-item

(defthm block-item-annop-of-block-item-fix-block-item
  (equal (block-item-annop (block-item-fix block-item))
         (block-item-annop block-item)))

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

(defthm block-item-list-annop-of-block-item-list-fix-block-item-list
  (equal
       (block-item-list-annop (block-item-list-fix block-item-list))
       (block-item-list-annop block-item-list)))

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

(defthm amb-expr/tyname-annop-of-amb-expr/tyname-fix-amb-expr/tyname
  (equal
       (amb-expr/tyname-annop (amb-expr/tyname-fix amb-expr/tyname))
       (amb-expr/tyname-annop amb-expr/tyname)))

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

(defthm
 amb-declor/absdeclor-annop-of-amb-declor/absdeclor-fix-amb-declor/absdeclor
 (equal (amb-declor/absdeclor-annop
             (amb-declor/absdeclor-fix amb-declor/absdeclor))
        (amb-declor/absdeclor-annop amb-declor/absdeclor)))

Theorem: amb-decl/stmt-annop-of-amb-decl/stmt-fix-amb-decl/stmt

(defthm amb-decl/stmt-annop-of-amb-decl/stmt-fix-amb-decl/stmt
  (equal (amb-decl/stmt-annop (amb-decl/stmt-fix amb-decl/stmt))
         (amb-decl/stmt-annop amb-decl/stmt)))

Theorem: expr-annop-expr-equiv-congruence-on-expr

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

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

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

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

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

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

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

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

(defthm
 const-expr-option-annop-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-annop const-expr-option)
                 (const-expr-option-annop const-expr-option-equiv)))
 :rule-classes :congruence)

Theorem: genassoc-annop-genassoc-equiv-congruence-on-genassoc

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defthm
 decl-spec-list-annop-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-annop decl-spec-list)
                 (decl-spec-list-annop decl-spec-list-equiv)))
 :rule-classes :congruence)

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

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

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

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

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

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

Theorem: initer-annop-initer-equiv-congruence-on-initer

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

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

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

Theorem: desiniter-annop-desiniter-equiv-congruence-on-desiniter

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

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

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

Theorem: designor-annop-designor-equiv-congruence-on-designor

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

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

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

Theorem: declor-annop-declor-equiv-congruence-on-declor

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

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

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

Theorem: dirdeclor-annop-dirdeclor-equiv-congruence-on-dirdeclor

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

Theorem: absdeclor-annop-absdeclor-equiv-congruence-on-absdeclor

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

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

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

Theorem: dirabsdeclor-annop-dirabsdeclor-equiv-congruence-on-dirabsdeclor

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

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

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

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

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

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

(defthm
 param-declon-list-annop-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-annop param-declon-list)
                 (param-declon-list-annop param-declon-list-equiv)))
 :rule-classes :congruence)

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

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

Theorem: tyname-annop-tyname-equiv-congruence-on-tyname

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

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

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

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

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

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

(defthm
 struct-declon-list-annop-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-annop struct-declon-list)
             (struct-declon-list-annop struct-declon-list-equiv)))
 :rule-classes :congruence)

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

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

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

(defthm
 struct-declor-list-annop-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-annop struct-declor-list)
             (struct-declor-list-annop struct-declor-list-equiv)))
 :rule-classes :congruence)

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

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

Theorem: enumer-annop-enumer-equiv-congruence-on-enumer

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

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

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

Theorem: statassert-annop-statassert-equiv-congruence-on-statassert

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

Theorem: attrib-annop-attrib-equiv-congruence-on-attrib

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

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

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

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

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

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

(defthm
 attrib-spec-list-annop-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-annop attrib-spec-list)
           (attrib-spec-list-annop attrib-spec-list-equiv)))
 :rule-classes :congruence)

Theorem: initdeclor-annop-initdeclor-equiv-congruence-on-initdeclor

(defthm initdeclor-annop-initdeclor-equiv-congruence-on-initdeclor
  (implies (initdeclor-equiv initdeclor initdeclor-equiv)
           (equal (initdeclor-annop initdeclor)
                  (initdeclor-annop initdeclor-equiv)))
  :rule-classes :congruence)

Theorem: initdeclor-list-annop-initdeclor-list-equiv-congruence-on-initdeclor-list

(defthm
 initdeclor-list-annop-initdeclor-list-equiv-congruence-on-initdeclor-list
 (implies
      (initdeclor-list-equiv initdeclor-list initdeclor-list-equiv)
      (equal (initdeclor-list-annop initdeclor-list)
             (initdeclor-list-annop initdeclor-list-equiv)))
 :rule-classes :congruence)

Theorem: decl-annop-decl-equiv-congruence-on-decl

(defthm decl-annop-decl-equiv-congruence-on-decl
  (implies (decl-equiv decl decl-equiv)
           (equal (decl-annop decl)
                  (decl-annop decl-equiv)))
  :rule-classes :congruence)

Theorem: decl-list-annop-decl-list-equiv-congruence-on-decl-list

(defthm decl-list-annop-decl-list-equiv-congruence-on-decl-list
  (implies (decl-list-equiv decl-list decl-list-equiv)
           (equal (decl-list-annop decl-list)
                  (decl-list-annop decl-list-equiv)))
  :rule-classes :congruence)

Theorem: label-annop-label-equiv-congruence-on-label

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

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

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

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

(defthm
 asm-output-list-annop-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-annop asm-output-list)
             (asm-output-list-annop asm-output-list-equiv)))
 :rule-classes :congruence)

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

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

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

(defthm
 asm-input-list-annop-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-annop asm-input-list)
                 (asm-input-list-annop asm-input-list-equiv)))
 :rule-classes :congruence)

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

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

Theorem: stmt-annop-stmt-equiv-congruence-on-stmt

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

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

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

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

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

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

(defthm
 block-item-list-annop-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-annop block-item-list)
             (block-item-list-annop block-item-list-equiv)))
 :rule-classes :congruence)

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

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

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

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

Theorem: amb-decl/stmt-annop-amb-decl/stmt-equiv-congruence-on-amb-decl/stmt

(defthm
 amb-decl/stmt-annop-amb-decl/stmt-equiv-congruence-on-amb-decl/stmt
 (implies (amb-decl/stmt-equiv amb-decl/stmt amb-decl/stmt-equiv)
          (equal (amb-decl/stmt-annop amb-decl/stmt)
                 (amb-decl/stmt-annop amb-decl/stmt-equiv)))
 :rule-classes :congruence)