• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
          • Formalized-subset
          • Mapping-to-language-definition
          • Input-files
          • Compilation-database
          • Printer
          • Output-files
          • Abstract-syntax-operations
          • Implementation-environments
          • Abstract-syntax
          • Concrete-syntax
          • Disambiguation
            • Disambiguator
            • Unambiguity
              • Abstract-syntax-unambp
                • Exprs/decls/stmts-unambp
                • Filepath-transunit-map-unambp
                • Transunit-ensemble-unambp
                • Declor/absdeclor-unambp
                • Type-spec-list-unambp
                • Fundef-option-unambp
                • Extdecl-list-unambp
                • Expr/tyname-unambp
                • Code-ensemble-unambp
                • Fundef-unambp
                • Decl/stmt-unambp
                • Transunit-unambp
                • Extdecl-unambp
                • Typequal/attribspec-list-unambp
                • Typequal/attribspec-list-list-unambp
                • Typequal/attribspec-unambp
                • Struni-spec-unambp
                • Struct-declor-unambp
                • Struct-declor-list-unambp
                • Struct-declon-unambp
                • Struct-declon-list-unambp
                • Statassert-unambp
                • Spec/qual-unambp
                • Spec/qual-list-unambp
                • Param-declor-unambp
                • Param-declon-unambp
                • Param-declon-list-unambp
                • Member-designor-unambp
                • Initer-option-unambp
                • Initdeclor-unambp
                • Initdeclor-list-unambp
                • Genassoc-list-unambp
                • Expr-option-unambp
                • Enumer-list-unambp
                • Dirabsdeclor-unambp
                • Dirabsdeclor-option-unambp
                • Desiniter-list-unambp
                • Designor-list-unambp
                • Declor-option-unambp
                • Decl-spec-list-unambp
                • Const-expr-unambp
                • Const-expr-option-unambp
                • Block-item-unambp
                • Block-item-list-unambp
                • Attrib-spec-unambp
                • Attrib-spec-list-unambp
                • Attrib-list-unambp
                • Asm-output-unambp
                • Asm-output-list-unambp
                • Asm-input-list-unambp
                • Amb-expr/tyname-unambp
                • Amb-decl/stmt-unambp
                • Amb-declor/absdeclor-unambp
                • Align-spec-unambp
                • Absdeclor-option-unambp
                • Type-spec-unambp
                • Tyname-unambp
                • Stmt-unambp
                • Label-unambp
                • Initer-unambp
                • Genassoc-unambp
                • Expr-unambp
                • Expr-list-unambp
                • Enumer-unambp
                • Enum-spec-unambp
                • Dirdeclor-unambp
                • Desiniter-unambp
                • Designor-unambp
                • Declor-unambp
                • Decl-unambp
                • Decl-spec-unambp
                • Decl-list-unambp
                • Comp-stmt-unambp
                • Attrib-unambp
                • Asm-stmt-unambp
                • Asm-input-unambp
                • Absdeclor-unambp
              • Abstract-syntax-unambp-additional-theorems
              • Type-spec-list-unambp-of-sublists
              • Expr-unambp-of-operation-on-expr-unambp
          • Validation
          • Gcc-builtins
          • Preprocessing
          • Parsing
        • Atc
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Abstract-syntax-unambp

Exprs/decls/stmts-unambp

Definitions and Theorems

Function: expr-unambp

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

Function: expr-list-unambp

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

Function: expr-option-unambp

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

Function: const-expr-unambp

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

Function: const-expr-option-unambp

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

Function: genassoc-unambp

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

Function: genassoc-list-unambp

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

Function: member-designor-unambp

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

Function: type-spec-unambp

(defun type-spec-unambp (type-spec)
 (declare (xargs :guard (type-specp type-spec)))
 (declare (ignorable type-spec))
 (let ((__function__ 'type-spec-unambp))
  (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-unambp (type-spec-atomic->type type-spec))
     :struct (struni-spec-unambp (type-spec-struct->spec type-spec))
     :union (struni-spec-unambp (type-spec-union->spec type-spec))
     :enum (enum-spec-unambp (type-spec-enum->spec type-spec))
     :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 (attrib-spec-list-unambp
                        (type-spec-struct-empty->attribs type-spec))
     :typeof-expr
     (expr-unambp (type-spec-typeof-expr->expr type-spec))
     :typeof-type
     (tyname-unambp (type-spec-typeof-type->type type-spec))
     :typeof-ambig nil
     :auto-type t)))

Function: spec/qual-unambp

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

Function: spec/qual-list-unambp

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

Function: align-spec-unambp

(defun align-spec-unambp (align-spec)
 (declare (xargs :guard (align-specp align-spec)))
 (declare (ignorable align-spec))
 (let ((__function__ 'align-spec-unambp))
  (declare (ignorable __function__))
  (align-spec-case
      align-spec
      :alignas-type
      (tyname-unambp (align-spec-alignas-type->type align-spec))
      :alignas-expr
      (const-expr-unambp (align-spec-alignas-expr->expr align-spec))
      :alignas-ambig nil)))

Function: decl-spec-unambp

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

Function: decl-spec-list-unambp

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

Function: typequal/attribspec-unambp

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

Function: typequal/attribspec-list-unambp

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

Function: typequal/attribspec-list-list-unambp

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

Function: initer-unambp

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

Function: initer-option-unambp

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

Function: desiniter-unambp

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

Function: desiniter-list-unambp

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

Function: designor-unambp

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

Function: designor-list-unambp

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

Function: declor-unambp

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

Function: declor-option-unambp

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

Function: dirdeclor-unambp

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

Function: absdeclor-unambp

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

Function: absdeclor-option-unambp

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

Function: dirabsdeclor-unambp

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

Function: dirabsdeclor-option-unambp

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

Function: param-declon-unambp

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

Function: param-declon-list-unambp

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

Function: param-declor-unambp

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

Function: tyname-unambp

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

Function: struni-spec-unambp

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

Function: struct-declon-unambp

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

Function: struct-declon-list-unambp

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

Function: struct-declor-unambp

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

Function: struct-declor-list-unambp

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

Function: enum-spec-unambp

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

Function: enumer-unambp

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

Function: enumer-list-unambp

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

Function: statassert-unambp

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

Function: attrib-unambp

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

Function: attrib-list-unambp

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

Function: attrib-spec-unambp

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

Function: attrib-spec-list-unambp

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

Function: initdeclor-unambp

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

Function: initdeclor-list-unambp

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

Function: decl-unambp

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

Function: decl-list-unambp

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

Function: label-unambp

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

Function: asm-output-unambp

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

Function: asm-output-list-unambp

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

Function: asm-input-unambp

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

Function: asm-input-list-unambp

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

Function: asm-stmt-unambp

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

Function: stmt-unambp

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

Function: comp-stmt-unambp

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

Function: block-item-unambp

(defun block-item-unambp (block-item)
  (declare (xargs :guard (block-itemp block-item)))
  (declare (ignorable block-item))
  (let ((__function__ 'block-item-unambp))
    (declare (ignorable __function__))
    (block-item-case
         block-item
         :decl (decl-unambp (block-item-decl->decl block-item))
         :stmt (stmt-unambp (block-item-stmt->stmt block-item))
         :ambig nil)))

Function: block-item-list-unambp

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

Function: amb-expr/tyname-unambp

(defun amb-expr/tyname-unambp (amb-expr/tyname)
  (declare (xargs :guard (amb-expr/tyname-p amb-expr/tyname)))
  (declare (ignorable amb-expr/tyname))
  (let ((__function__ 'amb-expr/tyname-unambp))
    (declare (ignorable __function__))
    nil))

Function: amb-declor/absdeclor-unambp

(defun amb-declor/absdeclor-unambp (amb-declor/absdeclor)
  (declare
       (xargs :guard (amb-declor/absdeclor-p amb-declor/absdeclor)))
  (declare (ignorable amb-declor/absdeclor))
  (let ((__function__ 'amb-declor/absdeclor-unambp))
    (declare (ignorable __function__))
    nil))

Function: amb-decl/stmt-unambp

(defun amb-decl/stmt-unambp (amb-decl/stmt)
  (declare (xargs :guard (amb-decl/stmt-p amb-decl/stmt)))
  (declare (ignorable amb-decl/stmt))
  (let ((__function__ 'amb-decl/stmt-unambp))
    (declare (ignorable __function__))
    nil))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: expr-unambp-of-expr-fix-expr

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

Theorem: expr-list-unambp-of-expr-list-fix-expr-list

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

Theorem: expr-option-unambp-of-expr-option-fix-expr-option

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

Theorem: const-expr-unambp-of-const-expr-fix-const-expr

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

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

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

Theorem: genassoc-unambp-of-genassoc-fix-genassoc

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

Theorem: genassoc-list-unambp-of-genassoc-list-fix-genassoc-list

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

Theorem: member-designor-unambp-of-member-designor-fix-member-designor

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

Theorem: type-spec-unambp-of-type-spec-fix-type-spec

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

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

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

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

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

Theorem: align-spec-unambp-of-align-spec-fix-align-spec

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

Theorem: decl-spec-unambp-of-decl-spec-fix-decl-spec

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

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

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

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

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

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

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

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

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

Theorem: initer-unambp-of-initer-fix-initer

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

Theorem: initer-option-unambp-of-initer-option-fix-initer-option

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

Theorem: desiniter-unambp-of-desiniter-fix-desiniter

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

Theorem: desiniter-list-unambp-of-desiniter-list-fix-desiniter-list

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

Theorem: designor-unambp-of-designor-fix-designor

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

Theorem: designor-list-unambp-of-designor-list-fix-designor-list

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

Theorem: declor-unambp-of-declor-fix-declor

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

Theorem: declor-option-unambp-of-declor-option-fix-declor-option

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

Theorem: dirdeclor-unambp-of-dirdeclor-fix-dirdeclor

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

Theorem: absdeclor-unambp-of-absdeclor-fix-absdeclor

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

Theorem: absdeclor-option-unambp-of-absdeclor-option-fix-absdeclor-option

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

Theorem: dirabsdeclor-unambp-of-dirabsdeclor-fix-dirabsdeclor

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

Theorem: dirabsdeclor-option-unambp-of-dirabsdeclor-option-fix-dirabsdeclor-option

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

Theorem: param-declon-unambp-of-param-declon-fix-param-declon

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

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

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

Theorem: param-declor-unambp-of-param-declor-fix-param-declor

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

Theorem: tyname-unambp-of-tyname-fix-tyname

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

Theorem: struni-spec-unambp-of-struni-spec-fix-struni-spec

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

Theorem: struct-declon-unambp-of-struct-declon-fix-struct-declon

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

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

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

Theorem: struct-declor-unambp-of-struct-declor-fix-struct-declor

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

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

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

Theorem: enum-spec-unambp-of-enum-spec-fix-enum-spec

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

Theorem: enumer-unambp-of-enumer-fix-enumer

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

Theorem: enumer-list-unambp-of-enumer-list-fix-enumer-list

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

Theorem: statassert-unambp-of-statassert-fix-statassert

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

Theorem: attrib-unambp-of-attrib-fix-attrib

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

Theorem: attrib-list-unambp-of-attrib-list-fix-attrib-list

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

Theorem: attrib-spec-unambp-of-attrib-spec-fix-attrib-spec

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

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

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

Theorem: initdeclor-unambp-of-initdeclor-fix-initdeclor

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

Theorem: initdeclor-list-unambp-of-initdeclor-list-fix-initdeclor-list

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

Theorem: decl-unambp-of-decl-fix-decl

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

Theorem: decl-list-unambp-of-decl-list-fix-decl-list

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

Theorem: label-unambp-of-label-fix-label

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

Theorem: asm-output-unambp-of-asm-output-fix-asm-output

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

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

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

Theorem: asm-input-unambp-of-asm-input-fix-asm-input

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

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

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

Theorem: asm-stmt-unambp-of-asm-stmt-fix-asm-stmt

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

Theorem: stmt-unambp-of-stmt-fix-stmt

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

Theorem: comp-stmt-unambp-of-comp-stmt-fix-comp-stmt

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

Theorem: block-item-unambp-of-block-item-fix-block-item

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

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

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

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

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

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

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

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

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

Theorem: expr-unambp-expr-equiv-congruence-on-expr

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

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

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

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

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

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

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

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

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

Theorem: genassoc-unambp-genassoc-equiv-congruence-on-genassoc

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: initer-unambp-initer-equiv-congruence-on-initer

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

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

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

Theorem: desiniter-unambp-desiniter-equiv-congruence-on-desiniter

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

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

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

Theorem: designor-unambp-designor-equiv-congruence-on-designor

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

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

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

Theorem: declor-unambp-declor-equiv-congruence-on-declor

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

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

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

Theorem: dirdeclor-unambp-dirdeclor-equiv-congruence-on-dirdeclor

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

Theorem: absdeclor-unambp-absdeclor-equiv-congruence-on-absdeclor

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

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

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

Theorem: dirabsdeclor-unambp-dirabsdeclor-equiv-congruence-on-dirabsdeclor

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

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

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

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

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

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

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

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

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

Theorem: tyname-unambp-tyname-equiv-congruence-on-tyname

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: enumer-unambp-enumer-equiv-congruence-on-enumer

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

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

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

Theorem: statassert-unambp-statassert-equiv-congruence-on-statassert

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

Theorem: attrib-unambp-attrib-equiv-congruence-on-attrib

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

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

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

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

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

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

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

Theorem: initdeclor-unambp-initdeclor-equiv-congruence-on-initdeclor

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

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

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

Theorem: decl-unambp-decl-equiv-congruence-on-decl

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

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

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

Theorem: label-unambp-label-equiv-congruence-on-label

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

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

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

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

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

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

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

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

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

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

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

Theorem: stmt-unambp-stmt-equiv-congruence-on-stmt

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

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

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

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

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

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

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

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

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

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

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

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

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