• 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
            • Abstract-syntax-trees
            • Abstract-syntax-irrelevants
            • Type-specifier-lists
            • Ascii-identifiers
            • Abstraction-mapping
            • Standard
              • Abstract-syntax-standardp
                • Exprs/decls/stmts-standardp
                • Filepath-transunit-map-standardp
                • Transunit-ensemble-standardp
                • Simple-escape-standardp
                • Stringlit-list-standardp
                • Type-qual-standardp
                • S-char-list-standardp
                • Fundef-standardp
                • Extdecl-list-standardp
                • C-char-list-standardp
                • Transunit-standardp
                • Stringlit-standardp
                • Fun-spec-standardp
                • Extdecl-standardp
                • S-char-standardp
                • Escape-standardp
                • Const-standardp
                • Cconst-standardp
                • C-char-standardp
                • Typequal/attribspec-list-standardp
                • Typequal/attribspec-list-list-standardp
                • Typequal/attribspec-standardp
                • Type-spec-standardp
                • Struni-spec-standardp
                • Struct-declor-standardp
                • Struct-declor-list-standardp
                • Struct-declon-standardp
                • Struct-declon-list-standardp
                • Statassert-standardp
                • Spec/qual-standardp
                • Spec/qual-list-standardp
                • Param-declor-standardp
                • Param-declon-standardp
                • Param-declon-list-standardp
                • Member-designor-standardp
                • Initer-option-standardp
                • Initdeclor-standardp
                • Initdeclor-list-standardp
                • Genassoc-list-standardp
                • Expr-option-standardp
                • Expr-list-standardp
                • Enumer-list-standardp
                • Enum-spec-standardp
                • Dirdeclor-standardp
                • Dirabsdeclor-standardp
                • Dirabsdeclor-option-standardp
                • Desiniter-standardp
                • Desiniter-list-standardp
                • Designor-list-standardp
                • Declor-option-standardp
                • Decl-spec-standardp
                • Decl-spec-list-standardp
                • Decl-list-standardp
                • Const-expr-standardp
                • Const-expr-option-standardp
                • Comp-stmt-standardp
                • Block-item-standardp
                • Block-item-list-standardp
                • Attrib-spec-standardp
                • Attrib-spec-list-standardp
                • Attrib-list-standardp
                • Asm-output-standardp
                • Asm-output-list-standardp
                • Asm-input-standardp
                • Asm-input-list-standardp
                • Amb-expr/tyname-standardp
                • Amb-decl/stmt-standardp
                • Amb-declor/absdeclor-standardp
                • Align-spec-standardp
                • Absdeclor-standardp
                • Absdeclor-option-standardp
                • Tyname-standardp
                • Stmt-standardp
                • Label-standardp
                • Initer-standardp
                • Genassoc-standardp
                • Expr-standardp
                • Enumer-standardp
                • Designor-standardp
                • Declor-standardp
                • Decl-standardp
                • Attrib-standardp
                • Asm-stmt-standardp
            • Storage-specifier-lists
            • Code-ensembles
            • Purity
            • Make-self-code-ensemble
          • Concrete-syntax
          • Disambiguation
          • 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-standardp

Exprs/decls/stmts-standardp

Definitions and Theorems

Function: expr-standardp

(defun expr-standardp (expr)
 (declare (xargs :guard (exprp expr)))
 (declare (ignorable expr))
 (let ((__function__ 'expr-standardp))
  (declare (ignorable __function__))
  (expr-case
   expr
   :ident t
   :const (const-standardp (expr-const->const expr))
   :string (stringlit-list-standardp (expr-string->strings expr))
   :paren (expr-standardp (expr-paren->inner expr))
   :gensel
   (and (expr-standardp (expr-gensel->control expr))
        (genassoc-list-standardp (expr-gensel->assocs expr)))
   :arrsub (and (expr-standardp (expr-arrsub->arg1 expr))
                (expr-standardp (expr-arrsub->arg2 expr)))
   :funcall (and (expr-standardp (expr-funcall->fun expr))
                 (expr-list-standardp (expr-funcall->args expr)))
   :member (expr-standardp (expr-member->arg expr))
   :memberp (expr-standardp (expr-memberp->arg expr))
   :complit
   (and (tyname-standardp (expr-complit->type expr))
        (desiniter-list-standardp (expr-complit->elems expr)))
   :unary (and (expr-standardp (expr-unary->arg expr))
               (not (member-eq (expr-unary->op expr)
                               '(:alignof :real :imag))))
   :label-addr nil
   :sizeof (tyname-standardp (expr-sizeof->type expr))
   :sizeof-ambig (raise "Internal error: ambiguous ~x0."
                        (expr-fix expr))
   :alignof (and (tyname-standardp (expr-alignof->type expr))
                 (keyword-uscores-case (expr-alignof->uscores expr)
                                       :none))
   :alignof-ambig (raise "Internal error: ambiguous ~x0."
                         (expr-fix expr))
   :cast (and (tyname-standardp (expr-cast->type expr))
              (expr-standardp (expr-cast->arg expr)))
   :binary (and (expr-standardp (expr-binary->arg1 expr))
                (expr-standardp (expr-binary->arg2 expr)))
   :cond
   (and
     (expr-standardp (expr-cond->test expr))
     (expr-option-case (expr-cond->then expr)
                       :some)
     (expr-standardp (expr-option-some->val (expr-cond->then expr)))
     (expr-standardp (expr-cond->else expr)))
   :comma (and (expr-standardp (expr-comma->first expr))
               (expr-standardp (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 nil
   :tycompat nil
   :offsetof nil
   :va-arg nil
   :extension nil)))

Function: expr-list-standardp

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

Function: expr-option-standardp

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

Function: const-expr-standardp

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

Function: const-expr-option-standardp

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

Function: genassoc-standardp

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

Function: genassoc-list-standardp

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

Function: member-designor-standardp

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

Function: type-spec-standardp

(defun type-spec-standardp (type-spec)
 (declare (xargs :guard (type-specp type-spec)))
 (declare (ignorable type-spec))
 (let ((__function__ 'type-spec-standardp))
  (declare (ignorable __function__))
  (type-spec-case
    type-spec
    :void t
    :char t
    :short t
    :int t
    :long t
    :float t
    :double t
    :signed
    (keyword-uscores-case (type-spec-signed->uscores type-spec)
                          :none)
    :unsigned t
    :bool t
    :complex t
    :atomic (tyname-standardp (type-spec-atomic->type type-spec))
    :struct
    (struni-spec-standardp (type-spec-struct->spec type-spec))
    :union (struni-spec-standardp (type-spec-union->spec type-spec))
    :enum (enum-spec-standardp (type-spec-enum->spec type-spec))
    :typedef t
    :int128 nil
    :locase-float80 t
    :locase-float128 t
    :float16 nil
    :float16x nil
    :float32 nil
    :float32x nil
    :float64 nil
    :float64x nil
    :float128 nil
    :float128x nil
    :builtin-va-list nil
    :struct-empty nil
    :typeof-expr nil
    :typeof-type nil
    :typeof-ambig (raise "Internal error: ambiguous ~x0."
                         (type-spec-fix type-spec))
    :auto-type nil)))

Function: spec/qual-standardp

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

Function: spec/qual-list-standardp

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

Function: align-spec-standardp

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

Function: decl-spec-standardp

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

Function: decl-spec-list-standardp

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

Function: typequal/attribspec-standardp

(defun typequal/attribspec-standardp (typequal/attribspec)
 (declare
      (xargs :guard (typequal/attribspec-p typequal/attribspec)))
 (declare (ignorable typequal/attribspec))
 (let ((__function__ 'typequal/attribspec-standardp))
   (declare (ignorable __function__))
   (typequal/attribspec-case
        typequal/attribspec
        :type
        (type-qual-standardp
             (typequal/attribspec-type->unwrap typequal/attribspec))
        :attrib nil)))

Function: typequal/attribspec-list-standardp

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

Function: typequal/attribspec-list-list-standardp

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

Function: initer-standardp

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

Function: initer-option-standardp

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

Function: desiniter-standardp

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

Function: desiniter-list-standardp

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

Function: designor-standardp

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

Function: designor-list-standardp

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

Function: declor-standardp

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

Function: declor-option-standardp

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

Function: dirdeclor-standardp

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

Function: absdeclor-standardp

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

Function: absdeclor-option-standardp

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

Function: dirabsdeclor-standardp

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

Function: dirabsdeclor-option-standardp

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

Function: param-declon-standardp

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

Function: param-declon-list-standardp

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

Function: param-declor-standardp

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

Function: tyname-standardp

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

Function: struni-spec-standardp

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

Function: struct-declon-standardp

(defun struct-declon-standardp (struct-declon)
  (declare (xargs :guard (struct-declonp struct-declon)))
  (declare (ignorable struct-declon))
  (let ((__function__ 'struct-declon-standardp))
    (declare (ignorable __function__))
    (struct-declon-case
         struct-declon
         :member
         (and (not (struct-declon-member->extension struct-declon))
              (spec/qual-list-standardp
                   (struct-declon-member->specquals struct-declon))
              (struct-declor-list-standardp
                   (struct-declon-member->declors struct-declon))
              (endp (struct-declon-member->attribs struct-declon)))
         :statassert
         (statassert-standardp
              (struct-declon-statassert->unwrap struct-declon))
         :empty nil)))

Function: struct-declon-list-standardp

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

Function: struct-declor-standardp

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

Function: struct-declor-list-standardp

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

Function: enum-spec-standardp

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

Function: enumer-standardp

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

Function: enumer-list-standardp

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

Function: statassert-standardp

(defun statassert-standardp (statassert)
 (declare (xargs :guard (statassertp statassert)))
 (declare (ignorable statassert))
 (let ((__function__ 'statassert-standardp))
  (declare (ignorable __function__))
  (and
      (const-expr-standardp (statassert->test statassert))
      (stringlit-list-standardp (statassert->message statassert)))))

Function: attrib-standardp

(defun attrib-standardp (attrib)
  (declare (xargs :guard (attribp attrib)))
  (declare (ignorable attrib))
  (let ((__function__ 'attrib-standardp))
    (declare (ignorable __function__))
    nil))

Function: attrib-list-standardp

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

Function: attrib-spec-standardp

(defun attrib-spec-standardp (attrib-spec)
  (declare (xargs :guard (attrib-specp attrib-spec)))
  (declare (ignorable attrib-spec))
  (let ((__function__ 'attrib-spec-standardp))
    (declare (ignorable __function__))
    nil))

Function: attrib-spec-list-standardp

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

Function: initdeclor-standardp

(defun initdeclor-standardp (initdeclor)
  (declare (xargs :guard (initdeclorp initdeclor)))
  (declare (ignorable initdeclor))
  (let ((__function__ 'initdeclor-standardp))
    (declare (ignorable __function__))
    (and (declor-standardp (initdeclor->declor initdeclor))
         (not (initdeclor->asm? initdeclor))
         (endp (initdeclor->attribs initdeclor))
         (initer-option-standardp (initdeclor->init? initdeclor)))))

Function: initdeclor-list-standardp

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

Function: decl-standardp

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

Function: decl-list-standardp

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

Function: label-standardp

(defun label-standardp (label)
  (declare (xargs :guard (labelp label)))
  (declare (ignorable label))
  (let ((__function__ 'label-standardp))
    (declare (ignorable __function__))
    (label-case
         label
         :name (endp (label-name->attribs label))
         :casexpr
         (and (const-expr-standardp (label-casexpr->expr label))
              (const-expr-option-case (label-casexpr->range? label)
                                      :none))
         :default t)))

Function: asm-output-standardp

(defun asm-output-standardp (asm-output)
  (declare (xargs :guard (asm-outputp asm-output)))
  (declare (ignorable asm-output))
  (let ((__function__ 'asm-output-standardp))
    (declare (ignorable __function__))
    nil))

Function: asm-output-list-standardp

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

Function: asm-input-standardp

(defun asm-input-standardp (asm-input)
  (declare (xargs :guard (asm-inputp asm-input)))
  (declare (ignorable asm-input))
  (let ((__function__ 'asm-input-standardp))
    (declare (ignorable __function__))
    nil))

Function: asm-input-list-standardp

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

Function: asm-stmt-standardp

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

Function: stmt-standardp

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

Function: comp-stmt-standardp

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

Function: block-item-standardp

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

Function: block-item-list-standardp

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

Function: amb-expr/tyname-standardp

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

Function: amb-declor/absdeclor-standardp

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

Function: amb-decl/stmt-standardp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: expr-standardp-of-expr-fix-expr

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

Theorem: expr-list-standardp-of-expr-list-fix-expr-list

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

Theorem: expr-option-standardp-of-expr-option-fix-expr-option

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

Theorem: const-expr-standardp-of-const-expr-fix-const-expr

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

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

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

Theorem: genassoc-standardp-of-genassoc-fix-genassoc

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

Theorem: genassoc-list-standardp-of-genassoc-list-fix-genassoc-list

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

Theorem: member-designor-standardp-of-member-designor-fix-member-designor

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

Theorem: type-spec-standardp-of-type-spec-fix-type-spec

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

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

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

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

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

Theorem: align-spec-standardp-of-align-spec-fix-align-spec

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

Theorem: decl-spec-standardp-of-decl-spec-fix-decl-spec

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

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

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

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

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

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

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

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

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

Theorem: initer-standardp-of-initer-fix-initer

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

Theorem: initer-option-standardp-of-initer-option-fix-initer-option

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

Theorem: desiniter-standardp-of-desiniter-fix-desiniter

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

Theorem: desiniter-list-standardp-of-desiniter-list-fix-desiniter-list

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

Theorem: designor-standardp-of-designor-fix-designor

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

Theorem: designor-list-standardp-of-designor-list-fix-designor-list

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

Theorem: declor-standardp-of-declor-fix-declor

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

Theorem: declor-option-standardp-of-declor-option-fix-declor-option

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

Theorem: dirdeclor-standardp-of-dirdeclor-fix-dirdeclor

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

Theorem: absdeclor-standardp-of-absdeclor-fix-absdeclor

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

Theorem: absdeclor-option-standardp-of-absdeclor-option-fix-absdeclor-option

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

Theorem: dirabsdeclor-standardp-of-dirabsdeclor-fix-dirabsdeclor

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

Theorem: dirabsdeclor-option-standardp-of-dirabsdeclor-option-fix-dirabsdeclor-option

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

Theorem: param-declon-standardp-of-param-declon-fix-param-declon

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

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

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

Theorem: param-declor-standardp-of-param-declor-fix-param-declor

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

Theorem: tyname-standardp-of-tyname-fix-tyname

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

Theorem: struni-spec-standardp-of-struni-spec-fix-struni-spec

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

Theorem: struct-declon-standardp-of-struct-declon-fix-struct-declon

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

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

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

Theorem: struct-declor-standardp-of-struct-declor-fix-struct-declor

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

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

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

Theorem: enum-spec-standardp-of-enum-spec-fix-enum-spec

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

Theorem: enumer-standardp-of-enumer-fix-enumer

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

Theorem: enumer-list-standardp-of-enumer-list-fix-enumer-list

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

Theorem: statassert-standardp-of-statassert-fix-statassert

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

Theorem: attrib-standardp-of-attrib-fix-attrib

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

Theorem: attrib-list-standardp-of-attrib-list-fix-attrib-list

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

Theorem: attrib-spec-standardp-of-attrib-spec-fix-attrib-spec

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

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

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

Theorem: initdeclor-standardp-of-initdeclor-fix-initdeclor

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

Theorem: initdeclor-list-standardp-of-initdeclor-list-fix-initdeclor-list

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

Theorem: decl-standardp-of-decl-fix-decl

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

Theorem: decl-list-standardp-of-decl-list-fix-decl-list

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

Theorem: label-standardp-of-label-fix-label

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

Theorem: asm-output-standardp-of-asm-output-fix-asm-output

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

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

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

Theorem: asm-input-standardp-of-asm-input-fix-asm-input

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

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

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

Theorem: asm-stmt-standardp-of-asm-stmt-fix-asm-stmt

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

Theorem: stmt-standardp-of-stmt-fix-stmt

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

Theorem: comp-stmt-standardp-of-comp-stmt-fix-comp-stmt

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

Theorem: block-item-standardp-of-block-item-fix-block-item

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

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

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

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

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

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

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

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

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

Theorem: expr-standardp-expr-equiv-congruence-on-expr

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

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

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

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

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

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

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

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

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

Theorem: genassoc-standardp-genassoc-equiv-congruence-on-genassoc

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: initer-standardp-initer-equiv-congruence-on-initer

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

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

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

Theorem: desiniter-standardp-desiniter-equiv-congruence-on-desiniter

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

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

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

Theorem: designor-standardp-designor-equiv-congruence-on-designor

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

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

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

Theorem: declor-standardp-declor-equiv-congruence-on-declor

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

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

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

Theorem: dirdeclor-standardp-dirdeclor-equiv-congruence-on-dirdeclor

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

Theorem: absdeclor-standardp-absdeclor-equiv-congruence-on-absdeclor

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

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

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

Theorem: dirabsdeclor-standardp-dirabsdeclor-equiv-congruence-on-dirabsdeclor

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

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

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

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

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

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

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

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

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

Theorem: tyname-standardp-tyname-equiv-congruence-on-tyname

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: enumer-standardp-enumer-equiv-congruence-on-enumer

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

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

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

Theorem: statassert-standardp-statassert-equiv-congruence-on-statassert

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

Theorem: attrib-standardp-attrib-equiv-congruence-on-attrib

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

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

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

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

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

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

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

Theorem: initdeclor-standardp-initdeclor-equiv-congruence-on-initdeclor

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

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

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

Theorem: decl-standardp-decl-equiv-congruence-on-decl

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

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

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

Theorem: label-standardp-label-equiv-congruence-on-label

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

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

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

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

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

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

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

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

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

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

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

Theorem: stmt-standardp-stmt-equiv-congruence-on-stmt

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

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

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

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

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

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

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

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

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

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

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

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

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