		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-purep

Exprs/decls/stmts-purep

Definitions and Theorems

Function: expr-purep

(defun expr-purep (expr)
 (declare (xargs :guard (exprp expr)))
 (declare (ignorable expr))
 (let ((__function__ 'expr-purep))
  (declare (ignorable __function__))
  (expr-case
    expr
    :ident t
    :const t
    :string t
    :paren (expr-purep (expr-paren->inner expr))
    :gensel (and (expr-purep (expr-gensel->control expr))
                 (genassoc-list-purep (expr-gensel->assocs expr)))
    :arrsub (and (expr-purep (expr-arrsub->arg1 expr))
                 (expr-purep (expr-arrsub->arg2 expr)))
    :funcall nil
    :member (expr-purep (expr-member->arg expr))
    :memberp (expr-purep (expr-memberp->arg expr))
    :complit (and (tyname-purep (expr-complit->type expr))
                  (desiniter-list-purep (expr-complit->elems expr)))
    :unary (and (unop-purep (expr-unary->op expr))
                (expr-purep (expr-unary->arg expr)))
    :label-addr t
    :sizeof (tyname-purep (expr-sizeof->type expr))
    :sizeof-ambig (raise "Internal error: ambiguous ~x0."
                         (expr-fix expr))
    :alignof (tyname-purep (expr-alignof->type expr))
    :alignof-ambig (raise "Internal error: ambiguous ~x0."
                          (expr-fix expr))
    :cast (and (tyname-purep (expr-cast->type expr))
               (expr-purep (expr-cast->arg expr)))
    :binary (and (binop-purep (expr-binary->op expr))
                 (and (expr-purep (expr-binary->arg1 expr))
                      (expr-purep (expr-binary->arg2 expr))))
    :cond (and (expr-purep (expr-cond->test expr))
               (and (expr-option-purep (expr-cond->then expr))
                    (expr-purep (expr-cond->else expr))))
    :comma (and (expr-purep (expr-comma->first expr))
                (expr-purep (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-purep (expr-stmt->stmt expr))
    :tycompat (and (tyname-purep (expr-tycompat->type1 expr))
                   (tyname-purep (expr-tycompat->type2 expr)))
    :offsetof
    (and (tyname-purep (expr-offsetof->type expr))
         (member-designor-purep (expr-offsetof->member expr)))
    :va-arg (and (expr-purep (expr-va-arg->list expr))
                 (tyname-purep (expr-va-arg->type expr)))
    :extension (expr-purep (expr-extension->expr expr)))))

Function: expr-list-purep

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

Function: expr-option-purep

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

Function: const-expr-purep

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

Function: const-expr-option-purep

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

Function: genassoc-purep

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

Function: genassoc-list-purep

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

Function: member-designor-purep

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

Function: type-spec-purep

(defun type-spec-purep (type-spec)
 (declare (xargs :guard (type-specp type-spec)))
 (declare (ignorable type-spec))
 (let ((__function__ 'type-spec-purep))
  (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-purep (type-spec-atomic->type type-spec))
   :struct nil
   :union nil
   :enum nil
   :typedef t
   :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 nil
   :typeof-expr (expr-purep (type-spec-typeof-expr->expr type-spec))
   :typeof-type
   (tyname-purep (type-spec-typeof-type->type type-spec))
   :typeof-ambig (amb-expr/tyname-purep
                      (type-spec-typeof-ambig->expr/type type-spec))
   :auto-type t)))

Function: spec/qual-purep

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

Function: spec/qual-list-purep

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

Function: align-spec-purep

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

Function: decl-spec-purep

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

Function: decl-spec-list-purep

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

Function: typequal/attribspec-purep

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

Function: typequal/attribspec-list-purep

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

Function: typequal/attribspec-list-list-purep

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

Function: initer-purep

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

Function: initer-option-purep

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

Function: desiniter-purep

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

Function: desiniter-list-purep

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

Function: designor-purep

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

Function: designor-list-purep

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

Function: declor-purep

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

Function: declor-option-purep

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

Function: dirdeclor-purep

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

Function: absdeclor-purep

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

Function: absdeclor-option-purep

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

Function: dirabsdeclor-purep

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

Function: dirabsdeclor-option-purep

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

Function: param-declon-purep

(defun param-declon-purep (param-declon)
  (declare (xargs :guard (param-declonp param-declon)))
  (declare (ignorable param-declon))
  (let ((__function__ 'param-declon-purep))
    (declare (ignorable __function__))
    nil))

Function: param-declon-list-purep

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

Function: param-declor-purep

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

Function: tyname-purep

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

Function: struni-spec-purep

(defun struni-spec-purep (struni-spec)
 (declare (xargs :guard (struni-specp struni-spec)))
 (declare (ignorable struni-spec))
 (let ((__function__ 'struni-spec-purep))
  (declare (ignorable __function__))
  (and
    (attrib-spec-list-purep (struni-spec->attribs struni-spec))
    (struct-declon-list-purep (struni-spec->members struni-spec)))))

Function: struct-declon-purep

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

Function: struct-declon-list-purep

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

Function: struct-declor-purep

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

Function: struct-declor-list-purep

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

Function: enum-spec-purep

(defun enum-spec-purep (enum-spec)
  (declare (xargs :guard (enum-specp enum-spec)))
  (declare (ignorable enum-spec))
  (let ((__function__ 'enum-spec-purep))
    (declare (ignorable __function__))
    (enumer-list-purep (enum-spec->enumers enum-spec))))

Function: enumer-purep

(defun enumer-purep (enumer)
  (declare (xargs :guard (enumerp enumer)))
  (declare (ignorable enumer))
  (let ((__function__ 'enumer-purep))
    (declare (ignorable __function__))
    (const-expr-option-purep (enumer->value? enumer))))

Function: enumer-list-purep

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

Function: statassert-purep

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

Function: attrib-purep

(defun attrib-purep (attrib)
  (declare (xargs :guard (attribp attrib)))
  (declare (ignorable attrib))
  (let ((__function__ 'attrib-purep))
    (declare (ignorable __function__))
    (attrib-case
         attrib
         :name t
         :name-params
         (expr-list-purep (attrib-name-params->params attrib)))))

Function: attrib-list-purep

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

Function: attrib-spec-purep

(defun attrib-spec-purep (attrib-spec)
  (declare (xargs :guard (attrib-specp attrib-spec)))
  (declare (ignorable attrib-spec))
  (let ((__function__ 'attrib-spec-purep))
    (declare (ignorable __function__))
    (attrib-list-purep (attrib-spec->attribs attrib-spec))))

Function: attrib-spec-list-purep

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

Function: init-declor-purep

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

Function: init-declor-list-purep

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

Function: declon-purep

(defun declon-purep (declon)
  (declare (xargs :guard (declonp declon)))
  (declare (ignorable declon))
  (let ((__function__ 'declon-purep))
    (declare (ignorable __function__))
    nil))

Function: declon-list-purep

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

Function: label-purep

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

Function: asm-output-purep

(defun asm-output-purep (asm-output)
  (declare (xargs :guard (asm-outputp asm-output)))
  (declare (ignorable asm-output))
  (let ((__function__ 'asm-output-purep))
    (declare (ignorable __function__))
    (expr-purep (asm-output->lvalue asm-output))))

Function: asm-output-list-purep

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

Function: asm-input-purep

(defun asm-input-purep (asm-input)
  (declare (xargs :guard (asm-inputp asm-input)))
  (declare (ignorable asm-input))
  (let ((__function__ 'asm-input-purep))
    (declare (ignorable __function__))
    (expr-purep (asm-input->rvalue asm-input))))

Function: asm-input-list-purep

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

Function: asm-stmt-purep

(defun asm-stmt-purep (asm-stmt)
  (declare (xargs :guard (asm-stmtp asm-stmt)))
  (declare (ignorable asm-stmt))
  (let ((__function__ 'asm-stmt-purep))
    (declare (ignorable __function__))
    nil))

Function: stmt-purep

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

Function: comp-stmt-purep

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

Function: block-item-purep

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

Function: block-item-list-purep

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

Function: amb-expr/tyname-purep

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

Function: amb-declor/absdeclor-purep

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

Function: amb-declon/stmt-purep

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: expr-purep-of-expr-fix-expr

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

Theorem: expr-list-purep-of-expr-list-fix-expr-list

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

Theorem: expr-option-purep-of-expr-option-fix-expr-option

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

Theorem: const-expr-purep-of-const-expr-fix-const-expr

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

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

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

Theorem: genassoc-purep-of-genassoc-fix-genassoc

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

Theorem: genassoc-list-purep-of-genassoc-list-fix-genassoc-list

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

Theorem: member-designor-purep-of-member-designor-fix-member-designor

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

Theorem: type-spec-purep-of-type-spec-fix-type-spec

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

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

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

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

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

Theorem: align-spec-purep-of-align-spec-fix-align-spec

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

Theorem: decl-spec-purep-of-decl-spec-fix-decl-spec

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

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

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

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

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

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

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

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

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

Theorem: initer-purep-of-initer-fix-initer

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

Theorem: initer-option-purep-of-initer-option-fix-initer-option

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

Theorem: desiniter-purep-of-desiniter-fix-desiniter

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

Theorem: desiniter-list-purep-of-desiniter-list-fix-desiniter-list

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

Theorem: designor-purep-of-designor-fix-designor

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

Theorem: designor-list-purep-of-designor-list-fix-designor-list

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

Theorem: declor-purep-of-declor-fix-declor

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

Theorem: declor-option-purep-of-declor-option-fix-declor-option

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

Theorem: dirdeclor-purep-of-dirdeclor-fix-dirdeclor

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

Theorem: absdeclor-purep-of-absdeclor-fix-absdeclor

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

Theorem: absdeclor-option-purep-of-absdeclor-option-fix-absdeclor-option

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

Theorem: dirabsdeclor-purep-of-dirabsdeclor-fix-dirabsdeclor

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

Theorem: dirabsdeclor-option-purep-of-dirabsdeclor-option-fix-dirabsdeclor-option

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

Theorem: param-declon-purep-of-param-declon-fix-param-declon

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

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

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

Theorem: param-declor-purep-of-param-declor-fix-param-declor

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

Theorem: tyname-purep-of-tyname-fix-tyname

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

Theorem: struni-spec-purep-of-struni-spec-fix-struni-spec

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

Theorem: struct-declon-purep-of-struct-declon-fix-struct-declon

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

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

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

Theorem: struct-declor-purep-of-struct-declor-fix-struct-declor

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

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

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

Theorem: enum-spec-purep-of-enum-spec-fix-enum-spec

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

Theorem: enumer-purep-of-enumer-fix-enumer

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

Theorem: enumer-list-purep-of-enumer-list-fix-enumer-list

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

Theorem: statassert-purep-of-statassert-fix-statassert

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

Theorem: attrib-purep-of-attrib-fix-attrib

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

Theorem: attrib-list-purep-of-attrib-list-fix-attrib-list

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

Theorem: attrib-spec-purep-of-attrib-spec-fix-attrib-spec

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

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

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

Theorem: init-declor-purep-of-init-declor-fix-init-declor

(defthm init-declor-purep-of-init-declor-fix-init-declor
  (equal (init-declor-purep (init-declor-fix init-declor))
         (init-declor-purep init-declor)))

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

(defthm
    init-declor-list-purep-of-init-declor-list-fix-init-declor-list
 (equal
    (init-declor-list-purep (init-declor-list-fix init-declor-list))
    (init-declor-list-purep init-declor-list)))

Theorem: declon-purep-of-declon-fix-declon

(defthm declon-purep-of-declon-fix-declon
  (equal (declon-purep (declon-fix declon))
         (declon-purep declon)))

Theorem: declon-list-purep-of-declon-list-fix-declon-list

(defthm declon-list-purep-of-declon-list-fix-declon-list
  (equal (declon-list-purep (declon-list-fix declon-list))
         (declon-list-purep declon-list)))

Theorem: label-purep-of-label-fix-label

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

Theorem: asm-output-purep-of-asm-output-fix-asm-output

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

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

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

Theorem: asm-input-purep-of-asm-input-fix-asm-input

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

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

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

Theorem: asm-stmt-purep-of-asm-stmt-fix-asm-stmt

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

Theorem: stmt-purep-of-stmt-fix-stmt

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

Theorem: comp-stmt-purep-of-comp-stmt-fix-comp-stmt

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

Theorem: block-item-purep-of-block-item-fix-block-item

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

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

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

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

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

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

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

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

(defthm amb-declon/stmt-purep-of-amb-declon/stmt-fix-amb-declon/stmt
  (equal
       (amb-declon/stmt-purep (amb-declon/stmt-fix amb-declon/stmt))
       (amb-declon/stmt-purep amb-declon/stmt)))

Theorem: expr-purep-expr-equiv-congruence-on-expr

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

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

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

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

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

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

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

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

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

Theorem: genassoc-purep-genassoc-equiv-congruence-on-genassoc

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: initer-purep-initer-equiv-congruence-on-initer

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

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

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

Theorem: desiniter-purep-desiniter-equiv-congruence-on-desiniter

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

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

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

Theorem: designor-purep-designor-equiv-congruence-on-designor

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

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

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

Theorem: declor-purep-declor-equiv-congruence-on-declor

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

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

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

Theorem: dirdeclor-purep-dirdeclor-equiv-congruence-on-dirdeclor

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

Theorem: absdeclor-purep-absdeclor-equiv-congruence-on-absdeclor

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

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

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

Theorem: dirabsdeclor-purep-dirabsdeclor-equiv-congruence-on-dirabsdeclor

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

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

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

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

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

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

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

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

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

Theorem: tyname-purep-tyname-equiv-congruence-on-tyname

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: enumer-purep-enumer-equiv-congruence-on-enumer

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

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

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

Theorem: statassert-purep-statassert-equiv-congruence-on-statassert

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

Theorem: attrib-purep-attrib-equiv-congruence-on-attrib

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

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

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

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

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

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

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

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

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

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

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

Theorem: declon-purep-declon-equiv-congruence-on-declon

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

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

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

Theorem: label-purep-label-equiv-congruence-on-label

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

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

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

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

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

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

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

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

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

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

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

Theorem: stmt-purep-stmt-equiv-congruence-on-stmt

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

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

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

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

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

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

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

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

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

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

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

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

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