		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-exprs/decls/stmts

Disambiguate expressions, declarations, statements, and related artifacts.

In general, to disambiguate a construct, first we recursively disambiguate its sub-constructs, then we either join them into an updated construct, or perform a disambiguation of the construct itself if needed.

In general, the disambiguation of a construct may involve the extension of the disambiguation table. For instance, the mere occurrence of an enumeration specifier in the type name that is part of a cast expression extends the disambiguation table with enumeration constants.

Definitions and Theorems

Function: dimb-expr

(defun dimb-expr (expr table)
 (declare (xargs :guard (and (exprp expr) (dimb-tablep table))))
 (let ((__function__ 'dimb-expr))
  (declare (ignorable __function__))
  (b* (((reterr) (irr-expr) (irr-dimb-table)))
   (expr-case
    expr :ident
    (b*
     ((kind (dimb-lookup-ident expr.ident table))
      ((unless kind)
       (retmsg$
        "The identifier ~x0 is used as an expression ~
                       but is not in scope."
        (ident->unwrap expr.ident))))
     (dimb-kind-case
      kind
      :typedef
      (retmsg$
       "The identifier ~x0 denotes a typedef ~
                             but it is used as an expression."
       (ident->unwrap expr.ident))
      :objfun (retok (expr-fix expr)
                     (dimb-table-fix table))
      :enumconst
      (retok (make-expr-const :const (const-enum expr.ident))
             (dimb-table-fix table))))
    :const
    (retok (expr-fix expr)
           (dimb-table-fix table))
    :string
    (retok (expr-fix expr)
           (dimb-table-fix table))
    :paren
    (b* (((erp new-expr table)
          (dimb-expr expr.inner table)))
      (retok (expr-paren new-expr) table))
    :gensel
    (b* (((erp new-control table)
          (dimb-expr expr.control table))
         ((erp new-assocs table)
          (dimb-genassoc-list expr.assocs table)))
      (retok (make-expr-gensel :control new-control
                               :assocs new-assocs)
             table))
    :arrsub
    (b* (((erp new-arg1 table)
          (dimb-expr expr.arg1 table))
         ((erp new-arg2 table)
          (dimb-expr expr.arg2 table)))
      (retok (make-expr-arrsub :arg1 new-arg1
                               :arg2 new-arg2)
             table))
    :funcall
    (b* (((erp new-fun table)
          (dimb-expr expr.fun table))
         ((erp new-args table)
          (dimb-expr-list expr.args table)))
      (retok (make-expr-funcall :fun new-fun
                                :args new-args)
             table))
    :member
    (b* (((erp new-arg table)
          (dimb-expr expr.arg table)))
      (retok (make-expr-member :arg new-arg
                               :name expr.name)
             table))
    :memberp
    (b* (((erp new-arg table)
          (dimb-expr expr.arg table)))
      (retok (make-expr-memberp :arg new-arg
                                :name expr.name)
             (dimb-table-fix table)))
    :complit
    (b* (((erp new-type table)
          (dimb-tyname expr.type table))
         ((erp new-elems table)
          (dimb-desiniter-list expr.elems table)))
      (retok (make-expr-complit :type new-type
                                :elems new-elems
                                :final-comma expr.final-comma)
             table))
    :unary
    (b* (((erp new-arg table)
          (dimb-expr expr.arg table)))
      (retok (dimb-make/adjust-expr-unary expr.op new-arg)
             table))
    :label-addr
    (retok (expr-fix expr)
           (dimb-table-fix table))
    :sizeof
    (b* (((erp new-tyname table)
          (dimb-tyname expr.type table)))
      (retok (expr-sizeof new-tyname) table))
    :sizeof-ambig
    (b* (((erp expr-or-tyname table)
          (dimb-amb-expr/tyname expr.expr/tyname t table)))
     (expr/tyname-case
      expr-or-tyname
      :expr (retok (dimb-make/adjust-expr-unary (unop-sizeof)
                                                expr-or-tyname.expr)
                   table)
      :tyname (retok (expr-sizeof expr-or-tyname.tyname)
                     table)))
    :alignof
    (b* (((erp new-tyname table)
          (dimb-tyname expr.type table)))
      (retok (make-expr-alignof :type new-tyname
                                :uscores expr.uscores)
             table))
    :alignof-ambig
    (b* (((erp expr-or-tyname table)
          (dimb-amb-expr/tyname expr.expr/tyname t table)))
     (expr/tyname-case
       expr-or-tyname
       :expr
       (retok
            (dimb-make/adjust-expr-unary (unop-alignof expr.uscores)
                                         expr-or-tyname.expr)
            table)
       :tyname (retok (make-expr-alignof :type expr-or-tyname.tyname
                                         :uscores expr.uscores)
                      table)))
    :cast
    (b* (((erp new-type table)
          (dimb-tyname expr.type table))
         ((erp new-arg table)
          (dimb-expr expr.arg table)))
      (retok (dimb-make/adjust-expr-cast new-type nil new-arg)
             table))
    :binary
    (b* (((erp new-arg1 table)
          (dimb-expr expr.arg1 table))
         ((erp new-arg2 table)
          (dimb-expr expr.arg2 table)))
     (retok (dimb-make/adjust-expr-binary expr.op new-arg1 new-arg2)
            table))
    :cond
    (b* (((erp new-test table)
          (dimb-expr expr.test table))
         ((erp new-then table)
          (dimb-expr-option expr.then table))
         ((erp new-else table)
          (dimb-expr expr.else table)))
      (retok (make-expr-cond :test new-test
                             :then new-then
                             :else new-else)
             table))
    :comma
    (b* (((erp new-first table)
          (dimb-expr expr.first table))
         ((erp new-next table)
          (dimb-expr expr.next table)))
      (retok (make-expr-comma :first new-first
                              :next new-next)
             table))
    :cast/call-ambig
    (b* (((erp expr/tyname table)
          (dimb-amb-expr/tyname expr.type/fun t table))
         ((erp new-arg/rest table)
          (dimb-expr expr.arg/rest table)))
     (expr/tyname-case
      expr/tyname
      :tyname (retok (dimb-cast/call-to-cast
                          (expr/tyname-tyname->tyname expr/tyname)
                          expr.inc/dec new-arg/rest)
                     table)
      :expr
      (retok
        (dimb-cast/call-to-call (expr/tyname-expr->expr expr/tyname)
                                expr.inc/dec new-arg/rest)
        table)))
    :cast/mul-ambig
    (b* (((erp expr/tyname table)
          (dimb-amb-expr/tyname expr.type/arg1 t table))
         ((erp new-arg/arg2 table)
          (dimb-expr expr.arg/arg2 table)))
     (expr/tyname-case
      expr/tyname
      :tyname (retok (dimb-cast/mul-to-cast
                          (expr/tyname-tyname->tyname expr/tyname)
                          expr.inc/dec new-arg/arg2)
                     table)
      :expr
      (retok
          (dimb-cast/mul-to-mul (expr/tyname-expr->expr expr/tyname)
                                expr.inc/dec new-arg/arg2)
          table)))
    :cast/add-ambig
    (b* (((erp expr/tyname table)
          (dimb-amb-expr/tyname expr.type/arg1 t table))
         ((erp new-arg/arg2 table)
          (dimb-expr expr.arg/arg2 table)))
     (expr/tyname-case
        expr/tyname
        :tyname (retok (dimb-cast/addsub-to-cast
                            (expr/tyname-tyname->tyname expr/tyname)
                            expr.inc/dec new-arg/arg2 (unop-plus))
                       table)
        :expr (retok (dimb-cast/addsub-to-addsub
                          (expr/tyname-expr->expr expr/tyname)
                          expr.inc/dec new-arg/arg2 (binop-add))
                     table)))
    :cast/sub-ambig
    (b* (((erp expr/tyname table)
          (dimb-amb-expr/tyname expr.type/arg1 t table))
         ((erp new-arg/arg2 table)
          (dimb-expr expr.arg/arg2 table)))
     (expr/tyname-case
        expr/tyname
        :tyname (retok (dimb-cast/addsub-to-cast
                            (expr/tyname-tyname->tyname expr/tyname)
                            expr.inc/dec new-arg/arg2 (unop-minus))
                       table)
        :expr (retok (dimb-cast/addsub-to-addsub
                          (expr/tyname-expr->expr expr/tyname)
                          expr.inc/dec new-arg/arg2 (binop-sub))
                     table)))
    :cast/and-ambig
    (b* (((erp expr/tyname table)
          (dimb-amb-expr/tyname expr.type/arg1 t table))
         ((erp new-arg/arg2 table)
          (dimb-expr expr.arg/arg2 table)))
     (expr/tyname-case
      expr/tyname
      :tyname (retok (dimb-cast/and-to-cast
                          (expr/tyname-tyname->tyname expr/tyname)
                          expr.inc/dec new-arg/arg2)
                     table)
      :expr
      (retok
          (dimb-cast/and-to-and (expr/tyname-expr->expr expr/tyname)
                                expr.inc/dec new-arg/arg2)
          table)))
    :cast/logand-ambig
    (b* (((erp expr/tyname table)
          (dimb-amb-expr/tyname expr.type/arg1 t table))
         ((erp new-arg/arg2 table)
          (dimb-expr expr.arg/arg2 table)))
     (expr/tyname-case
        expr/tyname
        :tyname (retok (dimb-cast/logand-to-cast
                            (expr/tyname-tyname->tyname expr/tyname)
                            expr.inc/dec new-arg/arg2)
                       table)
        :expr (retok (dimb-cast/logand-to-logand
                          (expr/tyname-expr->expr expr/tyname)
                          expr.inc/dec new-arg/arg2)
                     table)))
    :stmt
    (b* (((erp cstmt table)
          (dimb-comp-stmt expr.stmt nil table)))
      (retok (expr-stmt cstmt) table))
    :tycompat
    (b* (((erp type1 table)
          (dimb-tyname expr.type1 table))
         ((erp type2 table)
          (dimb-tyname expr.type2 table)))
      (retok (make-expr-tycompat :type1 type1
                                 :type2 type2)
             table))
    :offsetof
    (b* (((erp type table)
          (dimb-tyname expr.type table))
         ((erp memdes table)
          (dimb-member-designor expr.member table)))
      (retok (make-expr-offsetof :type type
                                 :member memdes)
             table))
    :va-arg
    (b* (((erp list table)
          (dimb-expr expr.list table))
         ((erp type table)
          (dimb-tyname expr.type table)))
      (retok (make-expr-va-arg :list list :type type)
             table))
    :extension
    (b* (((erp expr table)
          (dimb-expr expr.expr table)))
      (retok (expr-extension expr) table))))))

Function: dimb-expr-list

(defun dimb-expr-list (exprs table)
  (declare (xargs :guard (and (expr-listp exprs)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-expr-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp exprs))
          (retok nil (dimb-table-fix table)))
         ((erp new-expr table)
          (dimb-expr (car exprs) table))
         ((erp new-exprs table)
          (dimb-expr-list (cdr exprs) table)))
      (retok (cons new-expr new-exprs)
             table))))

Function: dimb-expr-option

(defun dimb-expr-option (expr? table)
  (declare (xargs :guard (and (expr-optionp expr?)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-expr-option))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table)))
      (expr-option-case expr?
                        :some (dimb-expr expr?.val table)
                        :none (retok nil (dimb-table-fix table))))))

Function: dimb-const-expr

(defun dimb-const-expr (cexpr table)
  (declare (xargs :guard (and (const-exprp cexpr)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-const-expr))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-const-expr)
          (irr-dimb-table))
         ((erp new-expr table)
          (dimb-expr (const-expr->expr cexpr)
                     table)))
      (retok (const-expr new-expr) table))))

Function: dimb-const-expr-option

(defun dimb-const-expr-option (cexpr? table)
  (declare (xargs :guard (and (const-expr-optionp cexpr?)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-const-expr-option))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table)))
      (const-expr-option-case
           cexpr?
           :some (dimb-const-expr cexpr?.val table)
           :none (retok nil (dimb-table-fix table))))))

Function: dimb-genassoc

(defun dimb-genassoc (assoc table)
  (declare (xargs :guard (and (genassocp assoc)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-genassoc))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-genassoc)
          (irr-dimb-table)))
      (genassoc-case assoc :type
                     (b* (((erp new-tyname table)
                           (dimb-tyname assoc.type table))
                          ((erp new-expr table)
                           (dimb-expr assoc.expr table)))
                       (retok (make-genassoc-type :type new-tyname
                                                  :expr new-expr)
                              table))
                     :default
                     (b* (((erp new-expr table)
                           (dimb-expr assoc.expr table)))
                       (retok (genassoc-default new-expr)
                              table))))))

Function: dimb-genassoc-list

(defun dimb-genassoc-list (assocs table)
  (declare (xargs :guard (and (genassoc-listp assocs)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-genassoc-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp assocs))
          (retok nil (dimb-table-fix table)))
         ((erp new-assoc table)
          (dimb-genassoc (car assocs) table))
         ((erp new-assocs table)
          (dimb-genassoc-list (cdr assocs)
                              table)))
      (retok (cons new-assoc new-assocs)
             table))))

Function: dimb-member-designor

(defun dimb-member-designor (memdes table)
  (declare (xargs :guard (and (member-designorp memdes)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-member-designor))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-member-designor)
          (irr-dimb-table)))
      (member-designor-case
           memdes :ident
           (retok (member-designor-fix memdes)
                  (dimb-table-fix table))
           :dot
           (b* (((erp new-memdes table)
                 (dimb-member-designor memdes.member table)))
             (retok (make-member-designor-dot :member new-memdes
                                              :name memdes.name)
                    table))
           :sub
           (b* (((erp new-memdes table)
                 (dimb-member-designor memdes.member table))
                ((erp new-index table)
                 (dimb-expr memdes.index table)))
             (retok (make-member-designor-sub :member new-memdes
                                              :index new-index)
                    table))))))

Function: dimb-type-spec

(defun dimb-type-spec (tyspec table)
 (declare (xargs :guard (and (type-specp tyspec)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-type-spec))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-type-spec)
        (irr-dimb-table)))
   (type-spec-case
    tyspec :void
    (retok (type-spec-void)
           (dimb-table-fix table))
    :char
    (retok (type-spec-char)
           (dimb-table-fix table))
    :short
    (retok (type-spec-short)
           (dimb-table-fix table))
    :int
    (retok (type-spec-int)
           (dimb-table-fix table))
    :long
    (retok (type-spec-long)
           (dimb-table-fix table))
    :float
    (retok (type-spec-float)
           (dimb-table-fix table))
    :double
    (retok (type-spec-double)
           (dimb-table-fix table))
    :signed
    (retok (type-spec-signed tyspec.uscores)
           (dimb-table-fix table))
    :unsigned
    (retok (type-spec-unsigned)
           (dimb-table-fix table))
    :bool
    (retok (type-spec-bool)
           (dimb-table-fix table))
    :complex
    (retok (type-spec-complex)
           (dimb-table-fix table))
    :atomic
    (b* (((erp new-type table)
          (dimb-tyname tyspec.type table)))
      (retok (type-spec-atomic new-type)
             table))
    :struct
    (b* (((erp new-struni-spec table)
          (dimb-struni-spec tyspec.spec table)))
      (retok (type-spec-struct new-struni-spec)
             table))
    :union
    (b* (((erp new-struni-spec table)
          (dimb-struni-spec tyspec.spec table)))
      (retok (type-spec-union new-struni-spec)
             table))
    :enum
    (b* (((erp new-enumspec table)
          (dimb-enum-spec tyspec.spec table)))
      (retok (type-spec-enum new-enumspec)
             table))
    :typedef
    (b*
     ((kind (dimb-lookup-ident tyspec.name table))
      ((unless kind)
       (retmsg$
        "The identifier ~x0 is used as a type specifier ~
                                but it is not in scope."
        (ident->unwrap tyspec.name))))
     (dimb-kind-case
      kind
      :typedef (retok (type-spec-typedef tyspec.name)
                      (dimb-table-fix table))
      :objfun
      (retmsg$
       "The identifier ~x0 denotes ~
                                     an object or function ~
                                     but it is used as a typedef name."
       (ident->unwrap tyspec.name))
      :enumconst
      (retmsg$
       "The identifier ~x0 denotes ~
                                        an enumeration constant ~
                                        but it is used as a typedef name."
       (ident->unwrap tyspec.name))))
    :int128
    (retok (make-type-spec-int128 :uscoret tyspec.uscoret)
           (dimb-table-fix table))
    :locase-float80
    (retok (type-spec-locase-float80)
           (dimb-table-fix table))
    :locase-float128
    (retok (type-spec-locase-float128)
           (dimb-table-fix table))
    :float16
    (retok (type-spec-float16)
           (dimb-table-fix table))
    :float16x
    (retok (type-spec-float16x)
           (dimb-table-fix table))
    :float32
    (retok (type-spec-float32)
           (dimb-table-fix table))
    :float32x
    (retok (type-spec-float32x)
           (dimb-table-fix table))
    :float64
    (retok (type-spec-float64)
           (dimb-table-fix table))
    :float64x
    (retok (type-spec-float64x)
           (dimb-table-fix table))
    :float128
    (retok (type-spec-float128)
           (dimb-table-fix table))
    :float128x
    (retok (type-spec-float128x)
           (dimb-table-fix table))
    :builtin-va-list
    (retok (type-spec-builtin-va-list)
           (dimb-table-fix table))
    :struct-empty
    (retok (type-spec-fix tyspec)
           (dimb-table-fix table))
    :typeof-expr
    (b* (((erp new-expr table)
          (dimb-expr tyspec.expr table)))
      (retok (make-type-spec-typeof-expr :expr new-expr
                                         :uscores tyspec.uscores)
             table))
    :typeof-type
    (b* (((erp new-tyname table)
          (dimb-tyname tyspec.type table)))
      (retok (make-type-spec-typeof-type :type new-tyname
                                         :uscores tyspec.uscores)
             table))
    :typeof-ambig
    (b* (((erp expr/tyname table)
          (dimb-amb-expr/tyname tyspec.expr/type nil table)))
     (expr/tyname-case
         expr/tyname
         :expr
         (retok (make-type-spec-typeof-expr :expr expr/tyname.expr
                                            :uscores tyspec.uscores)
                table)
         :tyname
         (retok (make-type-spec-typeof-type :type expr/tyname.tyname
                                            :uscores tyspec.uscores)
                table)))
    :auto-type (retok (type-spec-auto-type)
                      (dimb-table-fix table))))))

Function: dimb-spec/qual

(defun dimb-spec/qual (specqual table)
 (declare (xargs :guard (and (spec/qual-p specqual)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-spec/qual))
   (declare (ignorable __function__))
   (b* (((reterr)
         (irr-spec/qual)
         (irr-dimb-table)))
     (spec/qual-case specqual :typespec
                     (b* (((erp new-tyspec table)
                           (dimb-type-spec specqual.spec table)))
                       (retok (spec/qual-typespec new-tyspec)
                              table))
                     :typequal
                     (retok (spec/qual-typequal specqual.qual)
                            (dimb-table-fix table))
                     :align
                     (b* (((erp new-alignspec table)
                           (dimb-align-spec specqual.spec table)))
                       (retok (spec/qual-align new-alignspec)
                              table))
                     :attrib (retok (spec/qual-attrib specqual.spec)
                                    (dimb-table-fix table))))))

Function: dimb-spec/qual-list

(defun dimb-spec/qual-list (specquals table)
  (declare (xargs :guard (and (spec/qual-listp specquals)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-spec/qual-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp specquals))
          (retok nil (dimb-table-fix table)))
         ((erp new-specqual table)
          (dimb-spec/qual (car specquals) table))
         ((erp new-specquals table)
          (dimb-spec/qual-list (cdr specquals)
                               table)))
      (retok (cons new-specqual new-specquals)
             table))))

Function: dimb-align-spec

(defun dimb-align-spec (alignspec table)
 (declare (xargs :guard (and (align-specp alignspec)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-align-spec))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-align-spec)
        (irr-dimb-table)))
   (align-spec-case
    alignspec :alignas-type
    (b* (((erp new-type table)
          (dimb-tyname alignspec.type table)))
      (retok (align-spec-alignas-type new-type)
             table))
    :alignas-expr
    (b* (((erp new-expr table)
          (dimb-const-expr alignspec.expr table)))
      (retok (align-spec-alignas-expr new-expr)
             table))
    :alignas-ambig
    (b* (((erp expr/tyname table)
          (dimb-amb-expr/tyname alignspec.expr/type nil table)))
     (expr/tyname-case
      expr/tyname
      :expr
      (retok (align-spec-alignas-expr (const-expr expr/tyname.expr))
             table)
      :tyname (retok (align-spec-alignas-type expr/tyname.tyname)
                     table)))))))

Function: dimb-decl-spec

(defun dimb-decl-spec (declspec kind table)
  (declare (xargs :guard (and (decl-specp declspec)
                              (dimb-kindp kind)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-decl-spec))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-decl-spec)
          (irr-dimb-kind)
          (irr-dimb-table)))
      (decl-spec-case declspec :stoclass
                      (if (stor-spec-case declspec.spec :typedef)
                          (retok (decl-spec-fix declspec)
                                 (dimb-kind-typedef)
                                 (dimb-table-fix table))
                        (retok (decl-spec-fix declspec)
                               (dimb-kind-fix kind)
                               (dimb-table-fix table)))
                      :typespec
                      (b* (((erp new-tyspec table)
                            (dimb-type-spec declspec.spec table)))
                        (retok (decl-spec-typespec new-tyspec)
                               (dimb-kind-fix kind)
                               (dimb-table-fix table)))
                      :typequal
                      (retok (decl-spec-fix declspec)
                             (dimb-kind-fix kind)
                             (dimb-table-fix table))
                      :function
                      (retok (decl-spec-fix declspec)
                             (dimb-kind-fix kind)
                             (dimb-table-fix table))
                      :align
                      (b* (((erp new-alignspec table)
                            (dimb-align-spec declspec.spec table)))
                        (retok (decl-spec-align new-alignspec)
                               (dimb-kind-fix kind)
                               table))
                      :attrib (retok (decl-spec-fix declspec)
                                     (dimb-kind-fix kind)
                                     (dimb-table-fix table))
                      :stdcall (retok (decl-spec-fix declspec)
                                      (dimb-kind-fix kind)
                                      (dimb-table-fix table))
                      :declspec (retok (decl-spec-fix declspec)
                                       (dimb-kind-fix kind)
                                       (dimb-table-fix table))))))

Function: dimb-decl-spec-list

(defun dimb-decl-spec-list (declspecs kind table)
  (declare (xargs :guard (and (decl-spec-listp declspecs)
                              (dimb-kindp kind)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-decl-spec-list))
    (declare (ignorable __function__))
    (b* (((reterr)
          nil (irr-dimb-kind)
          (irr-dimb-table))
         ((when (endp declspecs))
          (retok nil (dimb-kind-fix kind)
                 (dimb-table-fix table)))
         ((erp new-declspec kind table)
          (dimb-decl-spec (car declspecs)
                          kind table))
         ((erp new-declspecs kind table)
          (dimb-decl-spec-list (cdr declspecs)
                               kind table)))
      (retok (cons new-declspec new-declspecs)
             kind table))))

Function: dimb-initer

(defun dimb-initer (initer table)
 (declare (xargs :guard (and (initerp initer)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-initer))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-initer)
        (irr-dimb-table)))
    (initer-case
         initer :single
         (b* (((erp new-expr table)
               (dimb-expr initer.expr table)))
           (retok (initer-single new-expr) table))
         :list
         (b* (((erp new-elems table)
               (dimb-desiniter-list initer.elems table)))
           (retok (make-initer-list :elems new-elems
                                    :final-comma initer.final-comma)
                  table))))))

Function: dimb-initer-option

(defun dimb-initer-option (initer? table)
 (declare (xargs :guard (and (initer-optionp initer?)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-initer-option))
  (declare (ignorable __function__))
  (b* (((reterr) nil (irr-dimb-table)))
    (initer-option-case initer?
                        :some (dimb-initer initer?.val table)
                        :none (retok nil (dimb-table-fix table))))))

Function: dimb-desiniter

(defun dimb-desiniter (desiniter table)
  (declare (xargs :guard (and (desiniterp desiniter)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-desiniter))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-desiniter)
          (irr-dimb-table))
         ((desiniter desiniter) desiniter)
         ((erp new-designors table)
          (dimb-designor-list desiniter.designors table))
         ((erp new-initer table)
          (dimb-initer desiniter.initer table)))
      (retok (make-desiniter :designors new-designors
                             :initer new-initer)
             table))))

Function: dimb-desiniter-list

(defun dimb-desiniter-list (desiniters table)
  (declare (xargs :guard (and (desiniter-listp desiniters)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-desiniter-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp desiniters))
          (retok nil (dimb-table-fix table)))
         ((erp new-desiniter table)
          (dimb-desiniter (car desiniters) table))
         ((erp new-desiniters table)
          (dimb-desiniter-list (cdr desiniters)
                               table)))
      (retok (cons new-desiniter new-desiniters)
             table))))

Function: dimb-designor

(defun dimb-designor (design table)
  (declare (xargs :guard (and (designorp design)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-designor))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-designor)
          (irr-dimb-table)))
      (designor-case
           design :sub
           (b* (((erp new-index table)
                 (dimb-const-expr design.index table))
                ((erp new-range? table)
                 (dimb-const-expr-option design.range? table)))
             (retok (make-designor-sub :index new-index
                                       :range? new-range?)
                    table))
           :dot (retok (designor-dot design.name)
                       (dimb-table-fix table))))))

Function: dimb-designor-list

(defun dimb-designor-list (designs table)
  (declare (xargs :guard (and (designor-listp designs)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-designor-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp designs))
          (retok nil (dimb-table-fix table)))
         ((erp new-design table)
          (dimb-designor (car designs) table))
         ((erp new-designs table)
          (dimb-designor-list (cdr designs)
                              table)))
      (retok (cons new-design new-designs)
             table))))

Function: dimb-declor

(defun dimb-declor (declor fundefp table)
  (declare (xargs :guard (and (declorp declor)
                              (booleanp fundefp)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-declor))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-declor)
          (irr-ident)
          (irr-dimb-table))
         ((declor declor) declor)
         ((erp new-dirdeclor ident table)
          (dimb-dirdeclor declor.direct fundefp table)))
      (retok (make-declor :pointers declor.pointers
                          :direct new-dirdeclor)
             ident table))))

Function: dimb-declor-option

(defun dimb-declor-option (declor? table)
  (declare (xargs :guard (and (declor-optionp declor?)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-declor-option))
    (declare (ignorable __function__))
    (b* (((reterr) nil nil (irr-dimb-table)))
      (declor-option-case
           declor? :some
           (b* (((erp new-declor? ident table)
                 (dimb-declor declor?.val nil table)))
             (retok new-declor? ident table))
           :none (retok nil nil (dimb-table-fix table))))))

Function: dimb-dirdeclor

(defun dimb-dirdeclor (dirdeclor fundefp table)
 (declare (xargs :guard (and (dirdeclorp dirdeclor)
                             (booleanp fundefp)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-dirdeclor))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-dirdeclor)
        (irr-ident)
        (irr-dimb-table)))
   (dirdeclor-case
    dirdeclor :ident
    (retok (dirdeclor-fix dirdeclor)
           dirdeclor.ident (dimb-table-fix table))
    :paren
    (b* (((erp new-declor ident table)
          (dimb-declor dirdeclor.inner fundefp table)))
      (retok (dirdeclor-paren new-declor)
             ident table))
    :array
    (b* (((erp new-dirdeclor ident table)
          (dimb-dirdeclor dirdeclor.declor fundefp table))
         ((erp new-expr? table)
          (dimb-expr-option dirdeclor.size? table)))
      (retok (make-dirdeclor-array :declor new-dirdeclor
                                   :qualspecs dirdeclor.qualspecs
                                   :size? new-expr?)
             ident table))
    :array-static1
    (b* (((erp new-dirdeclor ident table)
          (dimb-dirdeclor dirdeclor.declor fundefp table))
         ((erp new-expr table)
          (dimb-expr dirdeclor.size table)))
     (retok
        (make-dirdeclor-array-static1 :declor new-dirdeclor
                                      :qualspecs dirdeclor.qualspecs
                                      :size new-expr)
        ident table))
    :array-static2
    (b* (((erp new-dirdeclor ident table)
          (dimb-dirdeclor dirdeclor.declor fundefp table))
         ((erp new-expr table)
          (dimb-expr dirdeclor.size table)))
     (retok
        (make-dirdeclor-array-static2 :declor new-dirdeclor
                                      :qualspecs dirdeclor.qualspecs
                                      :size new-expr)
        ident table))
    :array-star
    (b* (((erp new-dirdeclor ident table)
          (dimb-dirdeclor dirdeclor.declor fundefp table)))
     (retok
          (make-dirdeclor-array-star :declor new-dirdeclor
                                     :qualspecs dirdeclor.qualspecs)
          ident table))
    :function-params
    (b*
     (((erp new-dirdeclor ident table)
       (dimb-dirdeclor dirdeclor.declor fundefp table))
      ((mv yes/no names)
       (dimb-params-to-names dirdeclor.params fundefp table))
      ((when yes/no)
       (retok
           (make-dirdeclor-function-names :declor new-dirdeclor
                                          :names names)
           ident
           (if (and fundefp
                    (not (dirdeclor-has-params-p dirdeclor.declor)))
               (dimb-push-scope table)
             table)))
      (table (dimb-push-scope table))
      ((erp new-params table)
       (dimb-param-declon-list dirdeclor.params table))
      (table
          (if (and fundefp
                   (not (dirdeclor-has-params-p dirdeclor.declor)))
              table
            (dimb-pop-scope table))
))
     (retok
       (make-dirdeclor-function-params :declor new-dirdeclor
                                       :params new-params
                                       :ellipsis dirdeclor.ellipsis)
       ident table))
    :function-names
    (b* (((erp new-dirdeclor ident table)
          (dimb-dirdeclor dirdeclor.declor fundefp table)))
      (retok (make-dirdeclor-function-names :declor new-dirdeclor
                                            :names dirdeclor.names)
             ident
             (if fundefp (dimb-push-scope table)
               table)))))))

Function: dimb-absdeclor

(defun dimb-absdeclor (absdeclor table)
  (declare (xargs :guard (and (absdeclorp absdeclor)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-absdeclor))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-absdeclor)
          (irr-dimb-table))
         ((absdeclor absdeclor) absdeclor)
         ((erp new-direct? table)
          (dimb-dirabsdeclor-option absdeclor.direct? table)))
      (retok (make-absdeclor :pointers absdeclor.pointers
                             :direct? new-direct?)
             table))))

Function: dimb-absdeclor-option

(defun dimb-absdeclor-option (absdeclor? table)
  (declare (xargs :guard (and (absdeclor-optionp absdeclor?)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-absdeclor-option))
    (declare (ignorable __function__))
    (b* (((reterr) nil nil (irr-dimb-table)))
      (absdeclor-option-case
           absdeclor?
           :some (dimb-absdeclor absdeclor?.val table)
           :none (retok nil (dimb-table-fix table))))))

Function: dimb-dirabsdeclor

(defun dimb-dirabsdeclor (dirabsdeclor table)
 (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-dirabsdeclor))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-dirabsdeclor)
        (irr-dimb-table)))
   (dirabsdeclor-case
    dirabsdeclor :dummy-base
    (prog2$
     (raise
      "Internal error: dummy base case of direct abstract declarator.")
     (retmsg$ ""))
    :paren
    (b* (((erp new-absdeclor table)
          (dimb-absdeclor dirabsdeclor.inner table)))
      (retok (dirabsdeclor-paren new-absdeclor)
             table))
    :array
    (b* (((erp new-declor? table)
          (dimb-dirabsdeclor-option dirabsdeclor.declor? table))
         ((erp new-size? table)
          (dimb-expr-option dirabsdeclor.size? table)))
     (retok
          (make-dirabsdeclor-array :declor? new-declor?
                                   :qualspecs dirabsdeclor.qualspecs
                                   :size? new-size?)
          table))
    :array-static1
    (b* (((erp new-declor? table)
          (dimb-dirabsdeclor-option dirabsdeclor.declor? table))
         ((erp new-size table)
          (dimb-expr dirabsdeclor.size table)))
      (retok (make-dirabsdeclor-array-static1
                  :declor? new-declor?
                  :qualspecs dirabsdeclor.qualspecs
                  :size new-size)
             table))
    :array-static2
    (b* (((erp new-declor? table)
          (dimb-dirabsdeclor-option dirabsdeclor.declor? table))
         ((erp new-size table)
          (dimb-expr dirabsdeclor.size table)))
      (retok (make-dirabsdeclor-array-static2
                  :declor? new-declor?
                  :qualspecs dirabsdeclor.qualspecs
                  :size new-size)
             table))
    :array-star
    (b* (((erp new-declor? table)
          (dimb-dirabsdeclor-option dirabsdeclor.declor? table)))
      (retok (dirabsdeclor-array-star new-declor?)
             table))
    :function
    (b* (((erp new-declor? table)
          (dimb-dirabsdeclor-option dirabsdeclor.declor? table))
         (table (dimb-push-scope table))
         ((erp new-params table)
          (dimb-param-declon-list dirabsdeclor.params table))
         (table (dimb-pop-scope table)))
     (retok
        (make-dirabsdeclor-function :declor? new-declor?
                                    :params new-params
                                    :ellipsis dirabsdeclor.ellipsis)
        table))))))

Function: dimb-dirabsdeclor-option

(defun dimb-dirabsdeclor-option (dirabsdeclor? table)
  (declare (xargs :guard (and (dirabsdeclor-optionp dirabsdeclor?)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-dirabsdeclor-option))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table)))
      (dirabsdeclor-option-case
           dirabsdeclor?
           :some (dimb-dirabsdeclor dirabsdeclor?.val table)
           :none (retok nil (dimb-table-fix table))))))

Function: dimb-param-declon

(defun dimb-param-declon (param table)
  (declare (xargs :guard (and (param-declonp param)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-param-declon))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-param-declon)
          (irr-dimb-table))
         ((param-declon param) param)
         ((erp new-specs & table)
          (dimb-decl-spec-list param.specs (dimb-kind-objfun)
                               table))
         ((erp new-decl table)
          (dimb-param-declor param.declor table)))
      (retok (make-param-declon :specs new-specs
                                :declor new-decl
                                :attribs param.attribs)
             table))))

Function: dimb-param-declon-list

(defun dimb-param-declon-list (params table)
  (declare (xargs :guard (and (param-declon-listp params)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-param-declon-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp params))
          (retok nil (dimb-table-fix table)))
         ((erp new-param table)
          (dimb-param-declon (car params) table))
         ((erp new-params table)
          (dimb-param-declon-list (cdr params)
                                  table)))
      (retok (cons new-param new-params)
             table))))

Function: dimb-param-declor

(defun dimb-param-declor (paramdeclor table)
 (declare (xargs :guard (and (param-declorp paramdeclor)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-param-declor))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-param-declor)
        (irr-dimb-table)))
   (param-declor-case
    paramdeclor :nonabstract
    (b* (((erp new-declor ident table)
          (dimb-declor paramdeclor.declor nil table))
         (table (dimb-add-ident ident (dimb-kind-objfun)
                                table)
))
      (retok (make-param-declor-nonabstract :declor new-declor
                                            :info nil)
             table))
    :abstract
    (b* (((erp new-absdeclor table)
          (dimb-absdeclor paramdeclor.declor table)))
      (retok (param-declor-abstract new-absdeclor)
             (dimb-table-fix table)))
    :none
    (retok (param-declor-none)
           (dimb-table-fix table))
    :ambig
    (b* (((erp declor/absdeclor ident? table)
          (dimb-amb-declor/absdeclor paramdeclor.declor table)))
     (declor/absdeclor-case
      declor/absdeclor :declor
      (b* (((unless ident?)
            (raise "Internal error: declarator without identifier.")
            (retmsg$ ""))
           (table (dimb-add-ident ident? (dimb-kind-objfun)
                                  table)
))
        (retok (make-param-declor-nonabstract
                    :declor declor/absdeclor.declor
                    :info nil)
               table))
      :absdeclor
      (retok (param-declor-abstract declor/absdeclor.absdeclor)
             (dimb-table-fix table))))))))

Function: dimb-tyname

(defun dimb-tyname (tyname table)
  (declare (xargs :guard (and (tynamep tyname)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-tyname))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-tyname) (irr-dimb-table))
         ((tyname tyname) tyname)
         ((erp new-specquals table)
          (dimb-spec/qual-list tyname.specquals table))
         ((erp new-declor? table)
          (dimb-absdeclor-option tyname.declor? table)))
      (retok (make-tyname :specquals new-specquals
                          :declor? new-declor?
                          :info nil)
             table))))

Function: dimb-struni-spec

(defun dimb-struni-spec (struni-spec table)
  (declare (xargs :guard (and (struni-specp struni-spec)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-struni-spec))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-struni-spec)
          (irr-dimb-table))
         ((struni-spec struni-spec) struni-spec)
         ((erp new-members table)
          (dimb-struct-declon-list struni-spec.members table)))
      (retok (make-struni-spec :attribs struni-spec.attribs
                               :name? struni-spec.name?
                               :members new-members)
             table))))

Function: dimb-struct-declon

(defun dimb-struct-declon (structdeclon table)
 (declare (xargs :guard (and (struct-declonp structdeclon)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-struct-declon))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-struct-declon)
        (irr-dimb-table)))
   (struct-declon-case
    structdeclon :member
    (b* (((erp new-specquals table)
          (dimb-spec/qual-list structdeclon.specquals table))
         ((erp new-declors table)
          (dimb-struct-declor-list structdeclon.declors table)))
     (retok
        (make-struct-declon-member :extension structdeclon.extension
                                   :specquals new-specquals
                                   :declors new-declors
                                   :attribs structdeclon.attribs)
        table))
    :statassert
    (b* (((erp new-statassert table)
          (dimb-statassert structdeclon.statassert table)))
      (retok (struct-declon-statassert new-statassert)
             table))
    :empty (retok (struct-declon-empty)
                  (dimb-table-fix table))))))

Function: dimb-struct-declon-list

(defun dimb-struct-declon-list (structdeclons table)
  (declare (xargs :guard (and (struct-declon-listp structdeclons)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-struct-declon-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp structdeclons))
          (retok nil (dimb-table-fix table)))
         ((erp new-structdeclon table)
          (dimb-struct-declon (car structdeclons)
                              table))
         ((erp new-structdeclons table)
          (dimb-struct-declon-list (cdr structdeclons)
                                   table)))
      (retok (cons new-structdeclon new-structdeclons)
             table))))

Function: dimb-struct-declor

(defun dimb-struct-declor (structdeclor table)
  (declare (xargs :guard (and (struct-declorp structdeclor)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-struct-declor))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-struct-declor)
          (irr-dimb-table))
         ((struct-declor structdeclor)
          structdeclor)
         ((erp new-declor? & table)
          (dimb-declor-option structdeclor.declor? table))
         ((erp new-expr? table)
          (dimb-const-expr-option structdeclor.expr? table)))
      (retok (make-struct-declor :declor? new-declor?
                                 :expr? new-expr?)
             table))))

Function: dimb-struct-declor-list

(defun dimb-struct-declor-list (structdeclors table)
  (declare (xargs :guard (and (struct-declor-listp structdeclors)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-struct-declor-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp structdeclors))
          (retok nil (dimb-table-fix table)))
         ((erp new-structdeclor table)
          (dimb-struct-declor (car structdeclors)
                              table))
         ((erp new-structdeclors table)
          (dimb-struct-declor-list (cdr structdeclors)
                                   table)))
      (retok (cons new-structdeclor new-structdeclors)
             table))))

Function: dimb-enum-spec

(defun dimb-enum-spec (enumspec table)
  (declare (xargs :guard (and (enum-specp enumspec)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-enum-spec))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-enum-spec)
          (irr-dimb-table))
         ((enum-spec enumspec) enumspec)
         ((erp new-list table)
          (dimb-enumer-list enumspec.list table)))
      (retok (make-enum-spec :name enumspec.name
                             :list new-list
                             :final-comma enumspec.final-comma)
             table))))

Function: dimb-enumer

(defun dimb-enumer (enumer table)
  (declare (xargs :guard (and (enumerp enumer)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-enumer))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-enumer) (irr-dimb-table))
         ((enumer enumer) enumer)
         ((erp new-value table)
          (dimb-const-expr-option enumer.value table))
         (table (dimb-add-ident enumer.name (dimb-kind-enumconst)
                                table)
))
      (retok (make-enumer :name enumer.name
                          :value new-value)
             table))))

Function: dimb-enumer-list

(defun dimb-enumer-list (enumers table)
  (declare (xargs :guard (and (enumer-listp enumers)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-enumer-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp enumers))
          (retok nil (dimb-table-fix table)))
         ((erp new-enumer table)
          (dimb-enumer (car enumers) table))
         ((erp new-enumers table)
          (dimb-enumer-list (cdr enumers) table)))
      (retok (cons new-enumer new-enumers)
             table))))

Function: dimb-statassert

(defun dimb-statassert (statassert table)
  (declare (xargs :guard (and (statassertp statassert)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-statassert))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-statassert)
          (irr-dimb-table))
         ((statassert statassert) statassert)
         ((erp new-test table)
          (dimb-const-expr statassert.test table)))
      (retok (make-statassert :test new-test
                              :message statassert.message)
             table))))

Function: dimb-initdeclor

(defun dimb-initdeclor (ideclor kind table)
  (declare (xargs :guard (and (initdeclorp ideclor)
                              (dimb-kindp kind)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-initdeclor))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-initdeclor)
          (irr-dimb-table))
         ((initdeclor ideclor) ideclor)
         ((erp new-declor ident table)
          (dimb-declor ideclor.declor nil table))
         (table (dimb-add-ident ident kind table)
)
         ((erp new-init? table)
          (dimb-initer-option ideclor.init? table)))
      (retok (make-initdeclor :declor new-declor
                              :asm? ideclor.asm?
                              :attribs ideclor.attribs
                              :init? new-init?)
             table))))

Function: dimb-initdeclor-list

(defun dimb-initdeclor-list (ideclors kind table)
  (declare (xargs :guard (and (initdeclor-listp ideclors)
                              (dimb-kindp kind)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-initdeclor-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp ideclors))
          (retok nil (dimb-table-fix table)))
         ((erp new-ideclor table)
          (dimb-initdeclor (car ideclors)
                           kind table))
         ((erp new-ideclors table)
          (dimb-initdeclor-list (cdr ideclors)
                                kind table)))
      (retok (cons new-ideclor new-ideclors)
             table))))

Function: dimb-decl

(defun dimb-decl (decl table)
  (declare (xargs :guard (and (declp decl) (dimb-tablep table))))
  (let ((__function__ 'dimb-decl))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-decl) (irr-dimb-table)))
      (decl-case
           decl :decl
           (b* (((erp new-specs kind table)
                 (dimb-decl-spec-list decl.specs (dimb-kind-objfun)
                                      table))
                ((erp new-init table)
                 (dimb-initdeclor-list decl.init kind table)))
             (retok (make-decl-decl :extension decl.extension
                                    :specs new-specs
                                    :init new-init)
                    table))
           :statassert
           (b* (((erp new-statassert table)
                 (dimb-statassert decl.statassert table)))
             (retok (decl-statassert new-statassert)
                    table))))))

Function: dimb-decl-list

(defun dimb-decl-list (decls table)
  (declare (xargs :guard (and (decl-listp decls)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-decl-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (dimb-table-fix table))
         ((when (endp decls))
          (retok nil (dimb-table-fix table)))
         ((erp new-decl table)
          (dimb-decl (car decls) table))
         ((erp new-decls table)
          (dimb-decl-list (cdr decls) table)))
      (retok (cons new-decl new-decls)
             table))))

Function: dimb-label

(defun dimb-label (label table)
 (declare (xargs :guard (and (labelp label)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-label))
   (declare (ignorable __function__))
   (b* (((reterr) (irr-label) (irr-dimb-table)))
     (label-case label :name
                 (retok (label-fix label)
                        (dimb-table-fix table))
                 :casexpr
                 (b* (((erp new-expr table)
                       (dimb-const-expr label.expr table))
                      ((erp new-range? table)
                       (dimb-const-expr-option label.range? table)))
                   (retok (make-label-casexpr :expr new-expr
                                              :range? new-range?)
                          table))
                 :default (retok (label-fix label)
                                 (dimb-table-fix table))))))

Function: dimb-stmt

(defun dimb-stmt (stmt table)
 (declare (xargs :guard (and (stmtp stmt) (dimb-tablep table))))
 (let ((__function__ 'dimb-stmt))
  (declare (ignorable __function__))
  (b* (((reterr) (irr-stmt) (irr-dimb-table)))
   (stmt-case
    stmt :labeled
    (b* (((erp new-label table)
          (dimb-label stmt.label table))
         ((erp new-stmt table)
          (dimb-stmt stmt.stmt table)))
      (retok (make-stmt-labeled :label new-label
                                :stmt new-stmt)
             table))
    :compound
    (b* (((erp cstmt table)
          (dimb-comp-stmt stmt.stmt nil table)))
      (retok (stmt-compound cstmt) table))
    :expr
    (b* (((erp new-expr? table)
          (dimb-expr-option stmt.expr? table)))
      (retok (make-stmt-expr :expr? new-expr?
                             :info nil)
             table))
    :if
    (b* ((table (dimb-push-scope table))
         ((erp new-test table)
          (dimb-expr stmt.test table))
         (table (dimb-push-scope table))
         ((erp new-then table)
          (dimb-stmt stmt.then table))
         (table (dimb-pop-scope table))
         (table (dimb-pop-scope table)))
      (retok (make-stmt-if :test new-test
                           :then new-then)
             table))
    :ifelse
    (b* ((table (dimb-push-scope table))
         ((erp new-test table)
          (dimb-expr stmt.test table))
         (table (dimb-push-scope table))
         ((erp new-then table)
          (dimb-stmt stmt.then table))
         (table (dimb-pop-scope table))
         (table (dimb-push-scope table))
         ((erp new-else table)
          (dimb-stmt stmt.else table))
         (table (dimb-pop-scope table))
         (table (dimb-pop-scope table)))
      (retok (make-stmt-ifelse :test new-test
                               :then new-then
                               :else new-else)
             table))
    :switch
    (b* ((table (dimb-push-scope table))
         ((erp new-target table)
          (dimb-expr stmt.target table))
         (table (dimb-push-scope table))
         ((erp new-body table)
          (dimb-stmt stmt.body table))
         (table (dimb-pop-scope table))
         (table (dimb-pop-scope table)))
      (retok (make-stmt-switch :target new-target
                               :body new-body)
             table))
    :while
    (b* ((table (dimb-push-scope table))
         ((erp new-test table)
          (dimb-expr stmt.test table))
         (table (dimb-push-scope table))
         ((erp new-body table)
          (dimb-stmt stmt.body table))
         (table (dimb-pop-scope table))
         (table (dimb-pop-scope table)))
      (retok (make-stmt-while :test new-test
                              :body new-body)
             table))
    :dowhile
    (b* ((table (dimb-push-scope table))
         (table (dimb-push-scope table))
         ((erp new-body table)
          (dimb-stmt stmt.body table))
         (table (dimb-pop-scope table))
         ((erp new-test table)
          (dimb-expr stmt.test table))
         (table (dimb-pop-scope table)))
      (retok (make-stmt-dowhile :body new-body
                                :test new-test)
             table))
    :for-expr
    (b* ((table (dimb-push-scope table))
         ((erp new-init table)
          (dimb-expr-option stmt.init table))
         ((erp new-test table)
          (dimb-expr-option stmt.test table))
         ((erp new-next table)
          (dimb-expr-option stmt.next table))
         (table (dimb-push-scope table))
         ((erp new-body table)
          (dimb-stmt stmt.body table))
         (table (dimb-pop-scope table)))
      (retok (make-stmt-for-expr :init new-init
                                 :test new-test
                                 :next new-next
                                 :body new-body)
             table))
    :for-decl
    (b* ((table (dimb-push-scope table))
         ((erp new-init table)
          (dimb-decl stmt.init table))
         ((erp new-test table)
          (dimb-expr-option stmt.test table))
         ((erp new-next table)
          (dimb-expr-option stmt.next table))
         (table (dimb-push-scope table))
         ((erp new-body table)
          (dimb-stmt stmt.body table))
         (table (dimb-pop-scope table)))
      (retok (make-stmt-for-decl :init new-init
                                 :test new-test
                                 :next new-next
                                 :body new-body)
             table))
    :for-ambig
    (b* ((table (dimb-push-scope table))
         ((erp decl/expr table)
          (dimb-amb-decl/stmt stmt.init table))
         ((erp new-test table)
          (dimb-expr-option stmt.test table))
         ((erp new-next table)
          (dimb-expr-option stmt.next table))
         (table (dimb-push-scope table))
         ((erp new-body table)
          (dimb-stmt stmt.body table))
         (table (dimb-pop-scope table)))
      (decl/stmt-case
           decl/expr
           :decl (retok (make-stmt-for-decl :init decl/expr.decl
                                            :test new-test
                                            :next new-next
                                            :body new-body)
                        table)
           :stmt (retok (make-stmt-for-expr :init decl/expr.expr
                                            :test new-test
                                            :next new-next
                                            :body new-body)
                        table)))
    :goto
    (retok (stmt-fix stmt)
           (dimb-table-fix table))
    :gotoe
    (b*
     (((when
         (and (expr-case stmt.label :ident)
              (not (dimb-lookup-ident (expr-ident->ident stmt.label)
                                      table))))
       (retok (stmt-goto (expr-ident->ident stmt.label))
              (dimb-table-fix table)))
      ((erp new-label table)
       (dimb-expr stmt.label table)))
     (retok (stmt-gotoe new-label) table))
    :continue
    (retok (stmt-fix stmt)
           (dimb-table-fix table))
    :break
    (retok (stmt-fix stmt)
           (dimb-table-fix table))
    :return
    (b* (((erp new-expr? table)
          (dimb-expr-option stmt.expr? table)))
      (retok (make-stmt-return :expr? new-expr?
                               :info stmt.info)
             table))
    :asm (retok (stmt-fix stmt)
                (dimb-table-fix table))))))

Function: dimb-comp-stmt

(defun dimb-comp-stmt (cstmt fundefp table)
  (declare (xargs :guard (and (comp-stmtp cstmt)
                              (booleanp fundefp)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-comp-stmt))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-comp-stmt)
          (irr-dimb-table))
         ((comp-stmt cstmt) cstmt)
         (table (if fundefp table
                  (dimb-push-scope table))
)
         ((erp new-items table)
          (dimb-block-item-list cstmt.items table))
         (table (if fundefp table
                  (dimb-pop-scope table))
))
      (retok (make-comp-stmt :labels cstmt.labels
                             :items new-items)
             table))))

Function: dimb-block-item

(defun dimb-block-item (item table)
 (declare (xargs :guard (and (block-itemp item)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-block-item))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-block-item)
        (irr-dimb-table)))
   (block-item-case
    item :decl
    (b* (((erp new-decl table)
          (dimb-decl item.decl table)))
      (retok (make-block-item-decl :decl new-decl
                                   :info item.info)
             table))
    :stmt
    (b* (((erp new-stmt table)
          (dimb-stmt item.stmt table)))
      (retok (make-block-item-stmt :stmt new-stmt
                                   :info item.info)
             table))
    :ambig
    (b* (((erp decl/stmt table)
          (dimb-amb-decl/stmt item.decl/stmt table)))
     (decl/stmt-case
       decl/stmt
       :decl (retok (make-block-item-decl :decl decl/stmt.decl
                                          :info nil)
                    table)
       :stmt (retok (make-block-item-stmt
                         :stmt (make-stmt-expr :expr? decl/stmt.expr
                                               :info nil)
                         :info nil)
                    table)))))))

Function: dimb-block-item-list

(defun dimb-block-item-list (items table)
  (declare (xargs :guard (and (block-item-listp items)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-block-item-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp items))
          (retok nil (dimb-table-fix table)))
         ((erp new-item table)
          (dimb-block-item (car items) table))
         ((erp new-items table)
          (dimb-block-item-list (cdr items)
                                table)))
      (retok (cons new-item new-items)
             table))))

Function: dimb-amb-expr/tyname

(defun dimb-amb-expr/tyname (expr/tyname add-parens-p table)
 (declare (xargs :guard (and (amb-expr/tyname-p expr/tyname)
                             (booleanp add-parens-p)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-amb-expr/tyname))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-expr/tyname)
        (irr-dimb-table))
       ((amb-expr/tyname expr/tyname)
        expr/tyname)
       ((mv erp-expr new-expr table-expr)
        (dimb-expr expr/tyname.expr table))
       ((mv erp-tyname new-tyname table-tyname)
        (dimb-tyname expr/tyname.tyname table)))
   (if erp-expr
    (if erp-tyname
     (retmsg$
      "In the ambiguous expression or type name ~x0, ~
                        neither the expression nor the type name can be ~
                        successfully disambiguated. The code must be invalid, ~
                        because at least one must succeed.~%~%~
                        These are the failures for each:~%~%~
                        ~@1~%~%~@2"
      (amb-expr/tyname-fix expr/tyname)
      erp-expr erp-tyname)
     (retok (expr/tyname-tyname new-tyname)
            table-tyname))
    (if erp-tyname
        (b* ((new-expr (if add-parens-p (expr-paren new-expr)
                         new-expr)))
          (retok (expr/tyname-expr new-expr)
                 table-expr))
     (retmsg$
      "In the ambiguous expression or type name ~x0, ~
                    both the expression and the type name
                    are successfully disambiguated. ~
                    The code must be invalid, ~
                    because at most one must succeed."
      (amb-expr/tyname-fix expr/tyname)))))))

Function: dimb-amb-declor/absdeclor

(defun dimb-amb-declor/absdeclor (declor/absdeclor table)
 (declare
      (xargs :guard (and (amb-declor/absdeclor-p declor/absdeclor)
                         (dimb-tablep table))))
 (let ((__function__ 'dimb-amb-declor/absdeclor))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-declor/absdeclor)
        nil (irr-dimb-table))
       ((amb-declor/absdeclor declor/absdeclor)
        declor/absdeclor)
       ((mv erp-declor
            new-declor ident table-declor)
        (dimb-declor declor/absdeclor.declor nil table))
       ((mv erp-absdeclor
            new-absdeclor table-absdeclor)
        (dimb-absdeclor declor/absdeclor.absdeclor table)))
   (if erp-declor
    (if erp-absdeclor
     (retmsg$
      "In the ambiguous ~
                        declarator or abstract declarator ~x0, ~
                        neither the declarator nor the abstract declarator ~
                        can be successfully disambiguated. ~
                        The code must be invalid, ~
                        because at least one must succeed.~%~%~
                        These are the failures for each:~%~%~
                        ~@1~%~%~@2"
      (amb-declor/absdeclor-fix declor/absdeclor)
      erp-declor erp-absdeclor)
     (retok (declor/absdeclor-absdeclor new-absdeclor)
            nil table-absdeclor))
    (if erp-absdeclor (retok (declor/absdeclor-declor new-declor)
                             ident table-declor)
     (b* ((kind (dimb-lookup-ident ident table)))
      (if (equal kind (dimb-kind-typedef))
          (retok (declor/absdeclor-absdeclor new-absdeclor)
                 nil table-absdeclor)
       (retmsg$
        "In the ambiguous ~
                        declarator or abstract declarator ~x0, ~
                        both the declarator and the abstract declarator ~
                        are successfully disambiguated, ~
                        and the identifier ~x1 in the declarator ~
                        is not a typedef name. ~
                        The code must be invalid, ~
                        because at most one must succeed."
        (amb-declor/absdeclor-fix declor/absdeclor)
        ident))))))))

Function: dimb-amb-decl/stmt

(defun dimb-amb-decl/stmt (decl/stmt table)
 (declare (xargs :guard (and (amb-decl/stmt-p decl/stmt)
                             (dimb-tablep table))))
 (let ((__function__ 'dimb-amb-decl/stmt))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-decl/stmt)
        (irr-dimb-table))
       ((amb-decl/stmt decl/stmt) decl/stmt)
       ((mv erp-decl new-decl table-decl)
        (dimb-decl decl/stmt.decl table))
       ((mv erp-expr new-expr table-expr)
        (dimb-expr decl/stmt.stmt table)))
   (if erp-decl
    (if erp-expr
     (retmsg$
      "In the ambiguous declaration or statement ~x0, ~
                        neither the declaration nor the expression ~
                        can be successfully disambiguated. ~
                        The code must be invalid, ~
                        because at least one must succeed.~%~%~
                        These are the failures for each:~%~%~
                        ~@1~%~%~@2"
      (amb-decl/stmt-fix decl/stmt)
      erp-decl erp-expr)
     (retok (decl/stmt-stmt new-expr)
            table-expr))
    (if erp-expr (retok (decl/stmt-decl new-decl)
                        table-decl)
     (retmsg$
      "In the ambiguous declaration or statement ~x0, ~
                    both the declaration and the statement ~
                    are successfully disambiguated. ~
                    The code must be invalid, ~
                    because at most one must succeed."
      (amb-decl/stmt-fix decl/stmt)))))))

Theorem: return-type-of-dimb-expr.erp

(defthm return-type-of-dimb-expr.erp
  (b* (((mv acl2::?erp ?new-expr ?new-table)
        (dimb-expr expr table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-expr.new-expr

(defthm return-type-of-dimb-expr.new-expr
  (b* (((mv acl2::?erp ?new-expr ?new-table)
        (dimb-expr expr table)))
    (exprp new-expr))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-expr.new-table

(defthm return-type-of-dimb-expr.new-table
  (b* (((mv acl2::?erp ?new-expr ?new-table)
        (dimb-expr expr table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-expr-list.erp

(defthm return-type-of-dimb-expr-list.erp
  (b* (((mv acl2::?erp ?new-exprs ?new-table)
        (dimb-expr-list exprs table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-expr-list.new-exprs

(defthm return-type-of-dimb-expr-list.new-exprs
  (b* (((mv acl2::?erp ?new-exprs ?new-table)
        (dimb-expr-list exprs table)))
    (expr-listp new-exprs))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-expr-list.new-table

(defthm return-type-of-dimb-expr-list.new-table
  (b* (((mv acl2::?erp ?new-exprs ?new-table)
        (dimb-expr-list exprs table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-expr-option.erp

(defthm return-type-of-dimb-expr-option.erp
  (b* (((mv acl2::?erp ?new-expr? ?new-table)
        (dimb-expr-option expr? table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-expr-option.new-expr?

(defthm return-type-of-dimb-expr-option.new-expr?
  (b* (((mv acl2::?erp ?new-expr? ?new-table)
        (dimb-expr-option expr? table)))
    (expr-optionp new-expr?))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-expr-option.new-table

(defthm return-type-of-dimb-expr-option.new-table
  (b* (((mv acl2::?erp ?new-expr? ?new-table)
        (dimb-expr-option expr? table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-const-expr.erp

(defthm return-type-of-dimb-const-expr.erp
  (b* (((mv acl2::?erp ?new-cexpr ?new-table)
        (dimb-const-expr cexpr table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-const-expr.new-cexpr

(defthm return-type-of-dimb-const-expr.new-cexpr
  (b* (((mv acl2::?erp ?new-cexpr ?new-table)
        (dimb-const-expr cexpr table)))
    (const-exprp new-cexpr))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-const-expr.new-table

(defthm return-type-of-dimb-const-expr.new-table
  (b* (((mv acl2::?erp ?new-cexpr ?new-table)
        (dimb-const-expr cexpr table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-const-expr-option.erp

(defthm return-type-of-dimb-const-expr-option.erp
  (b* (((mv acl2::?erp ?new-cexpr? ?new-table)
        (dimb-const-expr-option cexpr? table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-const-expr-option.new-cexpr?

(defthm return-type-of-dimb-const-expr-option.new-cexpr?
  (b* (((mv acl2::?erp ?new-cexpr? ?new-table)
        (dimb-const-expr-option cexpr? table)))
    (const-expr-optionp new-cexpr?))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-const-expr-option.new-table

(defthm return-type-of-dimb-const-expr-option.new-table
  (b* (((mv acl2::?erp ?new-cexpr? ?new-table)
        (dimb-const-expr-option cexpr? table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-genassoc.erp

(defthm return-type-of-dimb-genassoc.erp
  (b* (((mv acl2::?erp ?new-assoc ?new-table)
        (dimb-genassoc assoc table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-genassoc.new-assoc

(defthm return-type-of-dimb-genassoc.new-assoc
  (b* (((mv acl2::?erp ?new-assoc ?new-table)
        (dimb-genassoc assoc table)))
    (genassocp new-assoc))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-genassoc.new-table

(defthm return-type-of-dimb-genassoc.new-table
  (b* (((mv acl2::?erp ?new-assoc ?new-table)
        (dimb-genassoc assoc table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-genassoc-list.erp

(defthm return-type-of-dimb-genassoc-list.erp
  (b* (((mv acl2::?erp ?new-assocs ?new-table)
        (dimb-genassoc-list assocs table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-genassoc-list.new-assocs

(defthm return-type-of-dimb-genassoc-list.new-assocs
  (b* (((mv acl2::?erp ?new-assocs ?new-table)
        (dimb-genassoc-list assocs table)))
    (genassoc-listp new-assocs))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-genassoc-list.new-table

(defthm return-type-of-dimb-genassoc-list.new-table
  (b* (((mv acl2::?erp ?new-assocs ?new-table)
        (dimb-genassoc-list assocs table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-member-designor.erp

(defthm return-type-of-dimb-member-designor.erp
  (b* (((mv acl2::?erp ?new-memdes ?new-table)
        (dimb-member-designor memdes table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-member-designor.new-memdes

(defthm return-type-of-dimb-member-designor.new-memdes
  (b* (((mv acl2::?erp ?new-memdes ?new-table)
        (dimb-member-designor memdes table)))
    (member-designorp new-memdes))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-member-designor.new-table

(defthm return-type-of-dimb-member-designor.new-table
  (b* (((mv acl2::?erp ?new-memdes ?new-table)
        (dimb-member-designor memdes table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-type-spec.erp

(defthm return-type-of-dimb-type-spec.erp
  (b* (((mv acl2::?erp ?new-tyspec ?new-table)
        (dimb-type-spec tyspec table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-type-spec.new-tyspec

(defthm return-type-of-dimb-type-spec.new-tyspec
  (b* (((mv acl2::?erp ?new-tyspec ?new-table)
        (dimb-type-spec tyspec table)))
    (type-specp new-tyspec))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-type-spec.new-table

(defthm return-type-of-dimb-type-spec.new-table
  (b* (((mv acl2::?erp ?new-tyspec ?new-table)
        (dimb-type-spec tyspec table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-spec/qual.erp

(defthm return-type-of-dimb-spec/qual.erp
  (b* (((mv acl2::?erp ?new-specqual ?new-table)
        (dimb-spec/qual specqual table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-spec/qual.new-specqual

(defthm return-type-of-dimb-spec/qual.new-specqual
  (b* (((mv acl2::?erp ?new-specqual ?new-table)
        (dimb-spec/qual specqual table)))
    (spec/qual-p new-specqual))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-spec/qual.new-table

(defthm return-type-of-dimb-spec/qual.new-table
  (b* (((mv acl2::?erp ?new-specqual ?new-table)
        (dimb-spec/qual specqual table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-spec/qual-list.erp

(defthm return-type-of-dimb-spec/qual-list.erp
  (b* (((mv acl2::?erp ?new-specquals ?new-table)
        (dimb-spec/qual-list specquals table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-spec/qual-list.new-specquals

(defthm return-type-of-dimb-spec/qual-list.new-specquals
  (b* (((mv acl2::?erp ?new-specquals ?new-table)
        (dimb-spec/qual-list specquals table)))
    (spec/qual-listp new-specquals))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-spec/qual-list.new-table

(defthm return-type-of-dimb-spec/qual-list.new-table
  (b* (((mv acl2::?erp ?new-specquals ?new-table)
        (dimb-spec/qual-list specquals table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-align-spec.erp

(defthm return-type-of-dimb-align-spec.erp
  (b* (((mv acl2::?erp ?new-alignspec ?new-table)
        (dimb-align-spec alignspec table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-align-spec.new-alignspec

(defthm return-type-of-dimb-align-spec.new-alignspec
  (b* (((mv acl2::?erp ?new-alignspec ?new-table)
        (dimb-align-spec alignspec table)))
    (align-specp new-alignspec))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-align-spec.new-table

(defthm return-type-of-dimb-align-spec.new-table
  (b* (((mv acl2::?erp ?new-alignspec ?new-table)
        (dimb-align-spec alignspec table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-spec.erp

(defthm return-type-of-dimb-decl-spec.erp
  (b* (((mv acl2::?erp
            ?new-declspec ?new-kind ?new-table)
        (dimb-decl-spec declspec kind table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-spec.new-declspec

(defthm return-type-of-dimb-decl-spec.new-declspec
  (b* (((mv acl2::?erp
            ?new-declspec ?new-kind ?new-table)
        (dimb-decl-spec declspec kind table)))
    (decl-specp new-declspec))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-spec.new-kind

(defthm return-type-of-dimb-decl-spec.new-kind
  (b* (((mv acl2::?erp
            ?new-declspec ?new-kind ?new-table)
        (dimb-decl-spec declspec kind table)))
    (dimb-kindp new-kind))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-spec.new-table

(defthm return-type-of-dimb-decl-spec.new-table
  (b* (((mv acl2::?erp
            ?new-declspec ?new-kind ?new-table)
        (dimb-decl-spec declspec kind table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-spec-list.erp

(defthm return-type-of-dimb-decl-spec-list.erp
  (b* (((mv acl2::?erp
            ?new-declspecs ?new-kind ?new-table)
        (dimb-decl-spec-list declspecs kind table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-spec-list.new-declspecs

(defthm return-type-of-dimb-decl-spec-list.new-declspecs
  (b* (((mv acl2::?erp
            ?new-declspecs ?new-kind ?new-table)
        (dimb-decl-spec-list declspecs kind table)))
    (decl-spec-listp new-declspecs))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-spec-list.new-kind

(defthm return-type-of-dimb-decl-spec-list.new-kind
  (b* (((mv acl2::?erp
            ?new-declspecs ?new-kind ?new-table)
        (dimb-decl-spec-list declspecs kind table)))
    (dimb-kindp new-kind))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-spec-list.new-table

(defthm return-type-of-dimb-decl-spec-list.new-table
  (b* (((mv acl2::?erp
            ?new-declspecs ?new-kind ?new-table)
        (dimb-decl-spec-list declspecs kind table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initer.erp

(defthm return-type-of-dimb-initer.erp
  (b* (((mv acl2::?erp ?new-initer ?new-table)
        (dimb-initer initer table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initer.new-initer

(defthm return-type-of-dimb-initer.new-initer
  (b* (((mv acl2::?erp ?new-initer ?new-table)
        (dimb-initer initer table)))
    (initerp new-initer))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initer.new-table

(defthm return-type-of-dimb-initer.new-table
  (b* (((mv acl2::?erp ?new-initer ?new-table)
        (dimb-initer initer table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initer-option.erp

(defthm return-type-of-dimb-initer-option.erp
  (b* (((mv acl2::?erp ?new-initer? ?new-table)
        (dimb-initer-option initer? table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initer-option.new-initer?

(defthm return-type-of-dimb-initer-option.new-initer?
  (b* (((mv acl2::?erp ?new-initer? ?new-table)
        (dimb-initer-option initer? table)))
    (initer-optionp new-initer?))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initer-option.new-table

(defthm return-type-of-dimb-initer-option.new-table
  (b* (((mv acl2::?erp ?new-initer? ?new-table)
        (dimb-initer-option initer? table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-desiniter.erp

(defthm return-type-of-dimb-desiniter.erp
  (b* (((mv acl2::?erp ?new-desiniter ?new-table)
        (dimb-desiniter desiniter table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-desiniter.new-desiniter

(defthm return-type-of-dimb-desiniter.new-desiniter
  (b* (((mv acl2::?erp ?new-desiniter ?new-table)
        (dimb-desiniter desiniter table)))
    (desiniterp new-desiniter))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-desiniter.new-table

(defthm return-type-of-dimb-desiniter.new-table
  (b* (((mv acl2::?erp ?new-desiniter ?new-table)
        (dimb-desiniter desiniter table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-desiniter-list.erp

(defthm return-type-of-dimb-desiniter-list.erp
  (b* (((mv acl2::?erp ?new-desiniters ?new-table)
        (dimb-desiniter-list desiniters table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-desiniter-list.new-desiniters

(defthm return-type-of-dimb-desiniter-list.new-desiniters
  (b* (((mv acl2::?erp ?new-desiniters ?new-table)
        (dimb-desiniter-list desiniters table)))
    (desiniter-listp new-desiniters))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-desiniter-list.new-table

(defthm return-type-of-dimb-desiniter-list.new-table
  (b* (((mv acl2::?erp ?new-desiniters ?new-table)
        (dimb-desiniter-list desiniters table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-designor.erp

(defthm return-type-of-dimb-designor.erp
  (b* (((mv acl2::?erp ?new-design ?new-table)
        (dimb-designor design table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-designor.new-design

(defthm return-type-of-dimb-designor.new-design
  (b* (((mv acl2::?erp ?new-design ?new-table)
        (dimb-designor design table)))
    (designorp new-design))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-designor.new-table

(defthm return-type-of-dimb-designor.new-table
  (b* (((mv acl2::?erp ?new-design ?new-table)
        (dimb-designor design table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-designor-list.erp

(defthm return-type-of-dimb-designor-list.erp
  (b* (((mv acl2::?erp ?new-designs ?new-table)
        (dimb-designor-list designs table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-designor-list.new-designs

(defthm return-type-of-dimb-designor-list.new-designs
  (b* (((mv acl2::?erp ?new-designs ?new-table)
        (dimb-designor-list designs table)))
    (designor-listp new-designs))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-designor-list.new-table

(defthm return-type-of-dimb-designor-list.new-table
  (b* (((mv acl2::?erp ?new-designs ?new-table)
        (dimb-designor-list designs table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-declor.erp

(defthm return-type-of-dimb-declor.erp
  (b* (((mv acl2::?erp
            ?new-declor ?ident acl2::?table)
        (dimb-declor declor fundefp table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-declor.new-declor

(defthm return-type-of-dimb-declor.new-declor
  (b* (((mv acl2::?erp
            ?new-declor ?ident acl2::?table)
        (dimb-declor declor fundefp table)))
    (declorp new-declor))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-declor.ident

(defthm return-type-of-dimb-declor.ident
  (b* (((mv acl2::?erp
            ?new-declor ?ident acl2::?table)
        (dimb-declor declor fundefp table)))
    (identp ident))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-declor.table

(defthm return-type-of-dimb-declor.table
  (b* (((mv acl2::?erp
            ?new-declor ?ident acl2::?table)
        (dimb-declor declor fundefp table)))
    (dimb-tablep table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-declor-option.erp

(defthm return-type-of-dimb-declor-option.erp
  (b* (((mv acl2::?erp
            ?new-declor? ?ident? ?new-table)
        (dimb-declor-option declor? table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-declor-option.new-declor?

(defthm return-type-of-dimb-declor-option.new-declor?
  (b* (((mv acl2::?erp
            ?new-declor? ?ident? ?new-table)
        (dimb-declor-option declor? table)))
    (declor-optionp new-declor?))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-declor-option.ident?

(defthm return-type-of-dimb-declor-option.ident?
  (b* (((mv acl2::?erp
            ?new-declor? ?ident? ?new-table)
        (dimb-declor-option declor? table)))
    (ident-optionp ident?))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-declor-option.new-table

(defthm return-type-of-dimb-declor-option.new-table
  (b* (((mv acl2::?erp
            ?new-declor? ?ident? ?new-table)
        (dimb-declor-option declor? table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirdeclor.erp

(defthm return-type-of-dimb-dirdeclor.erp
  (b* (((mv acl2::?erp
            ?new-dirdeclor ?ident ?new-table)
        (dimb-dirdeclor dirdeclor fundefp table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirdeclor.new-dirdeclor

(defthm return-type-of-dimb-dirdeclor.new-dirdeclor
  (b* (((mv acl2::?erp
            ?new-dirdeclor ?ident ?new-table)
        (dimb-dirdeclor dirdeclor fundefp table)))
    (dirdeclorp new-dirdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirdeclor.ident

(defthm return-type-of-dimb-dirdeclor.ident
  (b* (((mv acl2::?erp
            ?new-dirdeclor ?ident ?new-table)
        (dimb-dirdeclor dirdeclor fundefp table)))
    (identp ident))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirdeclor.new-table

(defthm return-type-of-dimb-dirdeclor.new-table
  (b* (((mv acl2::?erp
            ?new-dirdeclor ?ident ?new-table)
        (dimb-dirdeclor dirdeclor fundefp table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-absdeclor.erp

(defthm return-type-of-dimb-absdeclor.erp
  (b* (((mv acl2::?erp ?new-absdeclor ?new-table)
        (dimb-absdeclor absdeclor table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-absdeclor.new-absdeclor

(defthm return-type-of-dimb-absdeclor.new-absdeclor
  (b* (((mv acl2::?erp ?new-absdeclor ?new-table)
        (dimb-absdeclor absdeclor table)))
    (absdeclorp new-absdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-absdeclor.new-table

(defthm return-type-of-dimb-absdeclor.new-table
  (b* (((mv acl2::?erp ?new-absdeclor ?new-table)
        (dimb-absdeclor absdeclor table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-absdeclor-option.erp

(defthm return-type-of-dimb-absdeclor-option.erp
  (b* (((mv acl2::?erp ?new-absdeclor? ?new-table)
        (dimb-absdeclor-option absdeclor? table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-absdeclor-option.new-absdeclor?

(defthm return-type-of-dimb-absdeclor-option.new-absdeclor?
  (b* (((mv acl2::?erp ?new-absdeclor? ?new-table)
        (dimb-absdeclor-option absdeclor? table)))
    (absdeclor-optionp new-absdeclor?))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-absdeclor-option.new-table

(defthm return-type-of-dimb-absdeclor-option.new-table
  (b* (((mv acl2::?erp ?new-absdeclor? ?new-table)
        (dimb-absdeclor-option absdeclor? table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirabsdeclor.erp

(defthm return-type-of-dimb-dirabsdeclor.erp
  (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-table)
        (dimb-dirabsdeclor dirabsdeclor table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirabsdeclor.new-dirabsdeclor

(defthm return-type-of-dimb-dirabsdeclor.new-dirabsdeclor
  (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-table)
        (dimb-dirabsdeclor dirabsdeclor table)))
    (dirabsdeclorp new-dirabsdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirabsdeclor.new-table

(defthm return-type-of-dimb-dirabsdeclor.new-table
  (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-table)
        (dimb-dirabsdeclor dirabsdeclor table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirabsdeclor-option.erp

(defthm return-type-of-dimb-dirabsdeclor-option.erp
  (b* (((mv acl2::?erp
            ?new-dirabsdeclor? ?new-table)
        (dimb-dirabsdeclor-option dirabsdeclor? table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirabsdeclor-option.new-dirabsdeclor?

(defthm return-type-of-dimb-dirabsdeclor-option.new-dirabsdeclor?
  (b* (((mv acl2::?erp
            ?new-dirabsdeclor? ?new-table)
        (dimb-dirabsdeclor-option dirabsdeclor? table)))
    (dirabsdeclor-optionp new-dirabsdeclor?))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-dirabsdeclor-option.new-table

(defthm return-type-of-dimb-dirabsdeclor-option.new-table
  (b* (((mv acl2::?erp
            ?new-dirabsdeclor? ?new-table)
        (dimb-dirabsdeclor-option dirabsdeclor? table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declon.erp

(defthm return-type-of-dimb-param-declon.erp
  (b* (((mv acl2::?erp ?new-param ?new-table)
        (dimb-param-declon param table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declon.new-param

(defthm return-type-of-dimb-param-declon.new-param
  (b* (((mv acl2::?erp ?new-param ?new-table)
        (dimb-param-declon param table)))
    (param-declonp new-param))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declon.new-table

(defthm return-type-of-dimb-param-declon.new-table
  (b* (((mv acl2::?erp ?new-param ?new-table)
        (dimb-param-declon param table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declon-list.erp

(defthm return-type-of-dimb-param-declon-list.erp
  (b* (((mv acl2::?erp ?new-params ?new-table)
        (dimb-param-declon-list params table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declon-list.new-params

(defthm return-type-of-dimb-param-declon-list.new-params
  (b* (((mv acl2::?erp ?new-params ?new-table)
        (dimb-param-declon-list params table)))
    (param-declon-listp new-params))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declon-list.new-table

(defthm return-type-of-dimb-param-declon-list.new-table
  (b* (((mv acl2::?erp ?new-params ?new-table)
        (dimb-param-declon-list params table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declor.erp

(defthm return-type-of-dimb-param-declor.erp
  (b* (((mv acl2::?erp ?new-paramdeclor ?new-table)
        (dimb-param-declor paramdeclor table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declor.new-paramdeclor

(defthm return-type-of-dimb-param-declor.new-paramdeclor
  (b* (((mv acl2::?erp ?new-paramdeclor ?new-table)
        (dimb-param-declor paramdeclor table)))
    (param-declorp new-paramdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-param-declor.new-table

(defthm return-type-of-dimb-param-declor.new-table
  (b* (((mv acl2::?erp ?new-paramdeclor ?new-table)
        (dimb-param-declor paramdeclor table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-tyname.erp

(defthm return-type-of-dimb-tyname.erp
  (b* (((mv acl2::?erp ?new-tyname ?new-table)
        (dimb-tyname tyname table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-tyname.new-tyname

(defthm return-type-of-dimb-tyname.new-tyname
  (b* (((mv acl2::?erp ?new-tyname ?new-table)
        (dimb-tyname tyname table)))
    (tynamep new-tyname))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-tyname.new-table

(defthm return-type-of-dimb-tyname.new-table
  (b* (((mv acl2::?erp ?new-tyname ?new-table)
        (dimb-tyname tyname table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struni-spec.erp

(defthm return-type-of-dimb-struni-spec.erp
  (b* (((mv acl2::?erp ?new-struni-spec ?new-table)
        (dimb-struni-spec struni-spec table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struni-spec.new-struni-spec

(defthm return-type-of-dimb-struni-spec.new-struni-spec
  (b* (((mv acl2::?erp ?new-struni-spec ?new-table)
        (dimb-struni-spec struni-spec table)))
    (struni-specp new-struni-spec))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struni-spec.new-table

(defthm return-type-of-dimb-struni-spec.new-table
  (b* (((mv acl2::?erp ?new-struni-spec ?new-table)
        (dimb-struni-spec struni-spec table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declon.erp

(defthm return-type-of-dimb-struct-declon.erp
  (b* (((mv acl2::?erp ?new-structdeclon ?new-table)
        (dimb-struct-declon structdeclon table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declon.new-structdeclon

(defthm return-type-of-dimb-struct-declon.new-structdeclon
  (b* (((mv acl2::?erp ?new-structdeclon ?new-table)
        (dimb-struct-declon structdeclon table)))
    (struct-declonp new-structdeclon))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declon.new-table

(defthm return-type-of-dimb-struct-declon.new-table
  (b* (((mv acl2::?erp ?new-structdeclon ?new-table)
        (dimb-struct-declon structdeclon table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declon-list.erp

(defthm return-type-of-dimb-struct-declon-list.erp
  (b* (((mv acl2::?erp
            ?new-structdeclons ?new-table)
        (dimb-struct-declon-list structdeclons table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declon-list.new-structdeclons

(defthm return-type-of-dimb-struct-declon-list.new-structdeclons
  (b* (((mv acl2::?erp
            ?new-structdeclons ?new-table)
        (dimb-struct-declon-list structdeclons table)))
    (struct-declon-listp new-structdeclons))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declon-list.new-table

(defthm return-type-of-dimb-struct-declon-list.new-table
  (b* (((mv acl2::?erp
            ?new-structdeclons ?new-table)
        (dimb-struct-declon-list structdeclons table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declor.erp

(defthm return-type-of-dimb-struct-declor.erp
  (b* (((mv acl2::?erp ?new-structdeclor ?new-table)
        (dimb-struct-declor structdeclor table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declor.new-structdeclor

(defthm return-type-of-dimb-struct-declor.new-structdeclor
  (b* (((mv acl2::?erp ?new-structdeclor ?new-table)
        (dimb-struct-declor structdeclor table)))
    (struct-declorp new-structdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declor.new-table

(defthm return-type-of-dimb-struct-declor.new-table
  (b* (((mv acl2::?erp ?new-structdeclor ?new-table)
        (dimb-struct-declor structdeclor table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declor-list.erp

(defthm return-type-of-dimb-struct-declor-list.erp
  (b* (((mv acl2::?erp
            ?new-structdeclors ?new-table)
        (dimb-struct-declor-list structdeclors table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declor-list.new-structdeclors

(defthm return-type-of-dimb-struct-declor-list.new-structdeclors
  (b* (((mv acl2::?erp
            ?new-structdeclors ?new-table)
        (dimb-struct-declor-list structdeclors table)))
    (struct-declor-listp new-structdeclors))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-struct-declor-list.new-table

(defthm return-type-of-dimb-struct-declor-list.new-table
  (b* (((mv acl2::?erp
            ?new-structdeclors ?new-table)
        (dimb-struct-declor-list structdeclors table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enum-spec.erp

(defthm return-type-of-dimb-enum-spec.erp
  (b* (((mv acl2::?erp ?new-enumspec ?new-table)
        (dimb-enum-spec enumspec table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enum-spec.new-enumspec

(defthm return-type-of-dimb-enum-spec.new-enumspec
  (b* (((mv acl2::?erp ?new-enumspec ?new-table)
        (dimb-enum-spec enumspec table)))
    (enum-specp new-enumspec))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enum-spec.new-table

(defthm return-type-of-dimb-enum-spec.new-table
  (b* (((mv acl2::?erp ?new-enumspec ?new-table)
        (dimb-enum-spec enumspec table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enumer.erp

(defthm return-type-of-dimb-enumer.erp
  (b* (((mv acl2::?erp ?new-enumer ?new-table)
        (dimb-enumer enumer table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enumer.new-enumer

(defthm return-type-of-dimb-enumer.new-enumer
  (b* (((mv acl2::?erp ?new-enumer ?new-table)
        (dimb-enumer enumer table)))
    (enumerp new-enumer))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enumer.new-table

(defthm return-type-of-dimb-enumer.new-table
  (b* (((mv acl2::?erp ?new-enumer ?new-table)
        (dimb-enumer enumer table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enumer-list.erp

(defthm return-type-of-dimb-enumer-list.erp
  (b* (((mv acl2::?erp ?new-enumers ?new-table)
        (dimb-enumer-list enumers table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enumer-list.new-enumers

(defthm return-type-of-dimb-enumer-list.new-enumers
  (b* (((mv acl2::?erp ?new-enumers ?new-table)
        (dimb-enumer-list enumers table)))
    (enumer-listp new-enumers))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-enumer-list.new-table

(defthm return-type-of-dimb-enumer-list.new-table
  (b* (((mv acl2::?erp ?new-enumers ?new-table)
        (dimb-enumer-list enumers table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-statassert.erp

(defthm return-type-of-dimb-statassert.erp
  (b* (((mv acl2::?erp ?new-statassert ?new-table)
        (dimb-statassert statassert table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-statassert.new-statassert

(defthm return-type-of-dimb-statassert.new-statassert
  (b* (((mv acl2::?erp ?new-statassert ?new-table)
        (dimb-statassert statassert table)))
    (statassertp new-statassert))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-statassert.new-table

(defthm return-type-of-dimb-statassert.new-table
  (b* (((mv acl2::?erp ?new-statassert ?new-table)
        (dimb-statassert statassert table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initdeclor.erp

(defthm return-type-of-dimb-initdeclor.erp
  (b* (((mv acl2::?erp ?new-ideclor ?new-table)
        (dimb-initdeclor ideclor kind table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initdeclor.new-ideclor

(defthm return-type-of-dimb-initdeclor.new-ideclor
  (b* (((mv acl2::?erp ?new-ideclor ?new-table)
        (dimb-initdeclor ideclor kind table)))
    (initdeclorp new-ideclor))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initdeclor.new-table

(defthm return-type-of-dimb-initdeclor.new-table
  (b* (((mv acl2::?erp ?new-ideclor ?new-table)
        (dimb-initdeclor ideclor kind table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initdeclor-list.erp

(defthm return-type-of-dimb-initdeclor-list.erp
  (b* (((mv acl2::?erp ?new-ideclors ?new-table)
        (dimb-initdeclor-list ideclors kind table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initdeclor-list.new-ideclors

(defthm return-type-of-dimb-initdeclor-list.new-ideclors
  (b* (((mv acl2::?erp ?new-ideclors ?new-table)
        (dimb-initdeclor-list ideclors kind table)))
    (initdeclor-listp new-ideclors))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-initdeclor-list.new-table

(defthm return-type-of-dimb-initdeclor-list.new-table
  (b* (((mv acl2::?erp ?new-ideclors ?new-table)
        (dimb-initdeclor-list ideclors kind table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl.erp

(defthm return-type-of-dimb-decl.erp
  (b* (((mv acl2::?erp ?new-decl ?new-table)
        (dimb-decl decl table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl.new-decl

(defthm return-type-of-dimb-decl.new-decl
  (b* (((mv acl2::?erp ?new-decl ?new-table)
        (dimb-decl decl table)))
    (declp new-decl))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl.new-table

(defthm return-type-of-dimb-decl.new-table
  (b* (((mv acl2::?erp ?new-decl ?new-table)
        (dimb-decl decl table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-list.erp

(defthm return-type-of-dimb-decl-list.erp
  (b* (((mv acl2::?erp ?new-decls ?new-table)
        (dimb-decl-list decls table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-list.new-decls

(defthm return-type-of-dimb-decl-list.new-decls
  (b* (((mv acl2::?erp ?new-decls ?new-table)
        (dimb-decl-list decls table)))
    (decl-listp new-decls))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-decl-list.new-table

(defthm return-type-of-dimb-decl-list.new-table
  (b* (((mv acl2::?erp ?new-decls ?new-table)
        (dimb-decl-list decls table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-label.erp

(defthm return-type-of-dimb-label.erp
  (b* (((mv acl2::?erp ?new-label ?new-table)
        (dimb-label label table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-label.new-label

(defthm return-type-of-dimb-label.new-label
  (b* (((mv acl2::?erp ?new-label ?new-table)
        (dimb-label label table)))
    (labelp new-label))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-label.new-table

(defthm return-type-of-dimb-label.new-table
  (b* (((mv acl2::?erp ?new-label ?new-table)
        (dimb-label label table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-stmt.erp

(defthm return-type-of-dimb-stmt.erp
  (b* (((mv acl2::?erp ?new-stmt ?new-table)
        (dimb-stmt stmt table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-stmt.new-stmt

(defthm return-type-of-dimb-stmt.new-stmt
  (b* (((mv acl2::?erp ?new-stmt ?new-table)
        (dimb-stmt stmt table)))
    (stmtp new-stmt))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-stmt.new-table

(defthm return-type-of-dimb-stmt.new-table
  (b* (((mv acl2::?erp ?new-stmt ?new-table)
        (dimb-stmt stmt table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-comp-stmt.erp

(defthm return-type-of-dimb-comp-stmt.erp
  (b* (((mv acl2::?erp ?new-cstmt ?new-table)
        (dimb-comp-stmt cstmt fundefp table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-comp-stmt.new-cstmt

(defthm return-type-of-dimb-comp-stmt.new-cstmt
  (b* (((mv acl2::?erp ?new-cstmt ?new-table)
        (dimb-comp-stmt cstmt fundefp table)))
    (comp-stmtp new-cstmt))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-comp-stmt.new-table

(defthm return-type-of-dimb-comp-stmt.new-table
  (b* (((mv acl2::?erp ?new-cstmt ?new-table)
        (dimb-comp-stmt cstmt fundefp table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-block-item.erp

(defthm return-type-of-dimb-block-item.erp
  (b* (((mv acl2::?erp ?new-item ?new-table)
        (dimb-block-item item table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-block-item.new-item

(defthm return-type-of-dimb-block-item.new-item
  (b* (((mv acl2::?erp ?new-item ?new-table)
        (dimb-block-item item table)))
    (block-itemp new-item))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-block-item.new-table

(defthm return-type-of-dimb-block-item.new-table
  (b* (((mv acl2::?erp ?new-item ?new-table)
        (dimb-block-item item table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-block-item-list.erp

(defthm return-type-of-dimb-block-item-list.erp
  (b* (((mv acl2::?erp ?new-items ?new-table)
        (dimb-block-item-list items table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-block-item-list.new-items

(defthm return-type-of-dimb-block-item-list.new-items
  (b* (((mv acl2::?erp ?new-items ?new-table)
        (dimb-block-item-list items table)))
    (block-item-listp new-items))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-block-item-list.new-table

(defthm return-type-of-dimb-block-item-list.new-table
  (b* (((mv acl2::?erp ?new-items ?new-table)
        (dimb-block-item-list items table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-expr/tyname.erp

(defthm return-type-of-dimb-amb-expr/tyname.erp
  (b* (((mv acl2::?erp ?expr-or-tyname ?new-table)
        (dimb-amb-expr/tyname expr/tyname add-parens-p table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-expr/tyname.expr-or-tyname

(defthm return-type-of-dimb-amb-expr/tyname.expr-or-tyname
  (b* (((mv acl2::?erp ?expr-or-tyname ?new-table)
        (dimb-amb-expr/tyname expr/tyname add-parens-p table)))
    (expr/tyname-p expr-or-tyname))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-expr/tyname.new-table

(defthm return-type-of-dimb-amb-expr/tyname.new-table
  (b* (((mv acl2::?erp ?expr-or-tyname ?new-table)
        (dimb-amb-expr/tyname expr/tyname add-parens-p table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-declor/absdeclor.erp

(defthm return-type-of-dimb-amb-declor/absdeclor.erp
  (b* (((mv acl2::?erp
            ?declor-or-absdeclor ?ident? ?new-table)
        (dimb-amb-declor/absdeclor declor/absdeclor table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-declor/absdeclor.declor-or-absdeclor

(defthm return-type-of-dimb-amb-declor/absdeclor.declor-or-absdeclor
  (b* (((mv acl2::?erp
            ?declor-or-absdeclor ?ident? ?new-table)
        (dimb-amb-declor/absdeclor declor/absdeclor table)))
    (declor/absdeclor-p declor-or-absdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-declor/absdeclor.ident?

(defthm return-type-of-dimb-amb-declor/absdeclor.ident?
  (b* (((mv acl2::?erp
            ?declor-or-absdeclor ?ident? ?new-table)
        (dimb-amb-declor/absdeclor declor/absdeclor table)))
    (ident-optionp ident?))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-declor/absdeclor.new-table

(defthm return-type-of-dimb-amb-declor/absdeclor.new-table
  (b* (((mv acl2::?erp
            ?declor-or-absdeclor ?ident? ?new-table)
        (dimb-amb-declor/absdeclor declor/absdeclor table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-decl/stmt.erp

(defthm return-type-of-dimb-amb-decl/stmt.erp
  (b* (((mv acl2::?erp ?decl-or-stmt ?new-table)
        (dimb-amb-decl/stmt decl/stmt table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-decl/stmt.decl-or-stmt

(defthm return-type-of-dimb-amb-decl/stmt.decl-or-stmt
  (b* (((mv acl2::?erp ?decl-or-stmt ?new-table)
        (dimb-amb-decl/stmt decl/stmt table)))
    (decl/stmt-p decl-or-stmt))
  :rule-classes :rewrite)

Theorem: return-type-of-dimb-amb-decl/stmt.new-table

(defthm return-type-of-dimb-amb-decl/stmt.new-table
  (b* (((mv acl2::?erp ?decl-or-stmt ?new-table)
        (dimb-amb-decl/stmt decl/stmt table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: dimb-expr-of-expr-fix-expr

(defthm dimb-expr-of-expr-fix-expr
  (equal (dimb-expr (expr-fix expr) table)
         (dimb-expr expr table)))

Theorem: dimb-expr-of-dimb-table-fix-table

(defthm dimb-expr-of-dimb-table-fix-table
  (equal (dimb-expr expr (dimb-table-fix table))
         (dimb-expr expr table)))

Theorem: dimb-expr-list-of-expr-list-fix-exprs

(defthm dimb-expr-list-of-expr-list-fix-exprs
  (equal (dimb-expr-list (expr-list-fix exprs)
                         table)
         (dimb-expr-list exprs table)))

Theorem: dimb-expr-list-of-dimb-table-fix-table

(defthm dimb-expr-list-of-dimb-table-fix-table
  (equal (dimb-expr-list exprs (dimb-table-fix table))
         (dimb-expr-list exprs table)))

Theorem: dimb-expr-option-of-expr-option-fix-expr?

(defthm dimb-expr-option-of-expr-option-fix-expr?
  (equal (dimb-expr-option (expr-option-fix expr?)
                           table)
         (dimb-expr-option expr? table)))

Theorem: dimb-expr-option-of-dimb-table-fix-table

(defthm dimb-expr-option-of-dimb-table-fix-table
  (equal (dimb-expr-option expr? (dimb-table-fix table))
         (dimb-expr-option expr? table)))

Theorem: dimb-const-expr-of-const-expr-fix-cexpr

(defthm dimb-const-expr-of-const-expr-fix-cexpr
  (equal (dimb-const-expr (const-expr-fix cexpr)
                          table)
         (dimb-const-expr cexpr table)))

Theorem: dimb-const-expr-of-dimb-table-fix-table

(defthm dimb-const-expr-of-dimb-table-fix-table
  (equal (dimb-const-expr cexpr (dimb-table-fix table))
         (dimb-const-expr cexpr table)))

Theorem: dimb-const-expr-option-of-const-expr-option-fix-cexpr?

(defthm dimb-const-expr-option-of-const-expr-option-fix-cexpr?
  (equal (dimb-const-expr-option (const-expr-option-fix cexpr?)
                                 table)
         (dimb-const-expr-option cexpr? table)))

Theorem: dimb-const-expr-option-of-dimb-table-fix-table

(defthm dimb-const-expr-option-of-dimb-table-fix-table
  (equal (dimb-const-expr-option cexpr? (dimb-table-fix table))
         (dimb-const-expr-option cexpr? table)))

Theorem: dimb-genassoc-of-genassoc-fix-assoc

(defthm dimb-genassoc-of-genassoc-fix-assoc
  (equal (dimb-genassoc (genassoc-fix assoc)
                        table)
         (dimb-genassoc assoc table)))

Theorem: dimb-genassoc-of-dimb-table-fix-table

(defthm dimb-genassoc-of-dimb-table-fix-table
  (equal (dimb-genassoc assoc (dimb-table-fix table))
         (dimb-genassoc assoc table)))

Theorem: dimb-genassoc-list-of-genassoc-list-fix-assocs

(defthm dimb-genassoc-list-of-genassoc-list-fix-assocs
  (equal (dimb-genassoc-list (genassoc-list-fix assocs)
                             table)
         (dimb-genassoc-list assocs table)))

Theorem: dimb-genassoc-list-of-dimb-table-fix-table

(defthm dimb-genassoc-list-of-dimb-table-fix-table
  (equal (dimb-genassoc-list assocs (dimb-table-fix table))
         (dimb-genassoc-list assocs table)))

Theorem: dimb-member-designor-of-member-designor-fix-memdes

(defthm dimb-member-designor-of-member-designor-fix-memdes
  (equal (dimb-member-designor (member-designor-fix memdes)
                               table)
         (dimb-member-designor memdes table)))

Theorem: dimb-member-designor-of-dimb-table-fix-table

(defthm dimb-member-designor-of-dimb-table-fix-table
  (equal (dimb-member-designor memdes (dimb-table-fix table))
         (dimb-member-designor memdes table)))

Theorem: dimb-type-spec-of-type-spec-fix-tyspec

(defthm dimb-type-spec-of-type-spec-fix-tyspec
  (equal (dimb-type-spec (type-spec-fix tyspec)
                         table)
         (dimb-type-spec tyspec table)))

Theorem: dimb-type-spec-of-dimb-table-fix-table

(defthm dimb-type-spec-of-dimb-table-fix-table
  (equal (dimb-type-spec tyspec (dimb-table-fix table))
         (dimb-type-spec tyspec table)))

Theorem: dimb-spec/qual-of-spec/qual-fix-specqual

(defthm dimb-spec/qual-of-spec/qual-fix-specqual
  (equal (dimb-spec/qual (spec/qual-fix specqual)
                         table)
         (dimb-spec/qual specqual table)))

Theorem: dimb-spec/qual-of-dimb-table-fix-table

(defthm dimb-spec/qual-of-dimb-table-fix-table
  (equal (dimb-spec/qual specqual (dimb-table-fix table))
         (dimb-spec/qual specqual table)))

Theorem: dimb-spec/qual-list-of-spec/qual-list-fix-specquals

(defthm dimb-spec/qual-list-of-spec/qual-list-fix-specquals
  (equal (dimb-spec/qual-list (spec/qual-list-fix specquals)
                              table)
         (dimb-spec/qual-list specquals table)))

Theorem: dimb-spec/qual-list-of-dimb-table-fix-table

(defthm dimb-spec/qual-list-of-dimb-table-fix-table
  (equal (dimb-spec/qual-list specquals (dimb-table-fix table))
         (dimb-spec/qual-list specquals table)))

Theorem: dimb-align-spec-of-align-spec-fix-alignspec

(defthm dimb-align-spec-of-align-spec-fix-alignspec
  (equal (dimb-align-spec (align-spec-fix alignspec)
                          table)
         (dimb-align-spec alignspec table)))

Theorem: dimb-align-spec-of-dimb-table-fix-table

(defthm dimb-align-spec-of-dimb-table-fix-table
  (equal (dimb-align-spec alignspec (dimb-table-fix table))
         (dimb-align-spec alignspec table)))

Theorem: dimb-decl-spec-of-decl-spec-fix-declspec

(defthm dimb-decl-spec-of-decl-spec-fix-declspec
  (equal (dimb-decl-spec (decl-spec-fix declspec)
                         kind table)
         (dimb-decl-spec declspec kind table)))

Theorem: dimb-decl-spec-of-dimb-kind-fix-kind

(defthm dimb-decl-spec-of-dimb-kind-fix-kind
  (equal (dimb-decl-spec declspec (dimb-kind-fix kind)
                         table)
         (dimb-decl-spec declspec kind table)))

Theorem: dimb-decl-spec-of-dimb-table-fix-table

(defthm dimb-decl-spec-of-dimb-table-fix-table
  (equal (dimb-decl-spec declspec kind (dimb-table-fix table))
         (dimb-decl-spec declspec kind table)))

Theorem: dimb-decl-spec-list-of-decl-spec-list-fix-declspecs

(defthm dimb-decl-spec-list-of-decl-spec-list-fix-declspecs
  (equal (dimb-decl-spec-list (decl-spec-list-fix declspecs)
                              kind table)
         (dimb-decl-spec-list declspecs kind table)))

Theorem: dimb-decl-spec-list-of-dimb-kind-fix-kind

(defthm dimb-decl-spec-list-of-dimb-kind-fix-kind
  (equal (dimb-decl-spec-list declspecs (dimb-kind-fix kind)
                              table)
         (dimb-decl-spec-list declspecs kind table)))

Theorem: dimb-decl-spec-list-of-dimb-table-fix-table

(defthm dimb-decl-spec-list-of-dimb-table-fix-table
  (equal (dimb-decl-spec-list declspecs kind (dimb-table-fix table))
         (dimb-decl-spec-list declspecs kind table)))

Theorem: dimb-initer-of-initer-fix-initer

(defthm dimb-initer-of-initer-fix-initer
  (equal (dimb-initer (initer-fix initer) table)
         (dimb-initer initer table)))

Theorem: dimb-initer-of-dimb-table-fix-table

(defthm dimb-initer-of-dimb-table-fix-table
  (equal (dimb-initer initer (dimb-table-fix table))
         (dimb-initer initer table)))

Theorem: dimb-initer-option-of-initer-option-fix-initer?

(defthm dimb-initer-option-of-initer-option-fix-initer?
  (equal (dimb-initer-option (initer-option-fix initer?)
                             table)
         (dimb-initer-option initer? table)))

Theorem: dimb-initer-option-of-dimb-table-fix-table

(defthm dimb-initer-option-of-dimb-table-fix-table
  (equal (dimb-initer-option initer? (dimb-table-fix table))
         (dimb-initer-option initer? table)))

Theorem: dimb-desiniter-of-desiniter-fix-desiniter

(defthm dimb-desiniter-of-desiniter-fix-desiniter
  (equal (dimb-desiniter (desiniter-fix desiniter)
                         table)
         (dimb-desiniter desiniter table)))

Theorem: dimb-desiniter-of-dimb-table-fix-table

(defthm dimb-desiniter-of-dimb-table-fix-table
  (equal (dimb-desiniter desiniter (dimb-table-fix table))
         (dimb-desiniter desiniter table)))

Theorem: dimb-desiniter-list-of-desiniter-list-fix-desiniters

(defthm dimb-desiniter-list-of-desiniter-list-fix-desiniters
  (equal (dimb-desiniter-list (desiniter-list-fix desiniters)
                              table)
         (dimb-desiniter-list desiniters table)))

Theorem: dimb-desiniter-list-of-dimb-table-fix-table

(defthm dimb-desiniter-list-of-dimb-table-fix-table
  (equal (dimb-desiniter-list desiniters (dimb-table-fix table))
         (dimb-desiniter-list desiniters table)))

Theorem: dimb-designor-of-designor-fix-design

(defthm dimb-designor-of-designor-fix-design
  (equal (dimb-designor (designor-fix design)
                        table)
         (dimb-designor design table)))

Theorem: dimb-designor-of-dimb-table-fix-table

(defthm dimb-designor-of-dimb-table-fix-table
  (equal (dimb-designor design (dimb-table-fix table))
         (dimb-designor design table)))

Theorem: dimb-designor-list-of-designor-list-fix-designs

(defthm dimb-designor-list-of-designor-list-fix-designs
  (equal (dimb-designor-list (designor-list-fix designs)
                             table)
         (dimb-designor-list designs table)))

Theorem: dimb-designor-list-of-dimb-table-fix-table

(defthm dimb-designor-list-of-dimb-table-fix-table
  (equal (dimb-designor-list designs (dimb-table-fix table))
         (dimb-designor-list designs table)))

Theorem: dimb-declor-of-declor-fix-declor

(defthm dimb-declor-of-declor-fix-declor
  (equal (dimb-declor (declor-fix declor)
                      fundefp table)
         (dimb-declor declor fundefp table)))

Theorem: dimb-declor-of-bool-fix-fundefp

(defthm dimb-declor-of-bool-fix-fundefp
  (equal (dimb-declor declor (bool-fix fundefp)
                      table)
         (dimb-declor declor fundefp table)))

Theorem: dimb-declor-of-dimb-table-fix-table

(defthm dimb-declor-of-dimb-table-fix-table
  (equal (dimb-declor declor fundefp (dimb-table-fix table))
         (dimb-declor declor fundefp table)))

Theorem: dimb-declor-option-of-declor-option-fix-declor?

(defthm dimb-declor-option-of-declor-option-fix-declor?
  (equal (dimb-declor-option (declor-option-fix declor?)
                             table)
         (dimb-declor-option declor? table)))

Theorem: dimb-declor-option-of-dimb-table-fix-table

(defthm dimb-declor-option-of-dimb-table-fix-table
  (equal (dimb-declor-option declor? (dimb-table-fix table))
         (dimb-declor-option declor? table)))

Theorem: dimb-dirdeclor-of-dirdeclor-fix-dirdeclor

(defthm dimb-dirdeclor-of-dirdeclor-fix-dirdeclor
  (equal (dimb-dirdeclor (dirdeclor-fix dirdeclor)
                         fundefp table)
         (dimb-dirdeclor dirdeclor fundefp table)))

Theorem: dimb-dirdeclor-of-bool-fix-fundefp

(defthm dimb-dirdeclor-of-bool-fix-fundefp
  (equal (dimb-dirdeclor dirdeclor (bool-fix fundefp)
                         table)
         (dimb-dirdeclor dirdeclor fundefp table)))

Theorem: dimb-dirdeclor-of-dimb-table-fix-table

(defthm dimb-dirdeclor-of-dimb-table-fix-table
  (equal (dimb-dirdeclor dirdeclor
                         fundefp (dimb-table-fix table))
         (dimb-dirdeclor dirdeclor fundefp table)))

Theorem: dimb-absdeclor-of-absdeclor-fix-absdeclor

(defthm dimb-absdeclor-of-absdeclor-fix-absdeclor
  (equal (dimb-absdeclor (absdeclor-fix absdeclor)
                         table)
         (dimb-absdeclor absdeclor table)))

Theorem: dimb-absdeclor-of-dimb-table-fix-table

(defthm dimb-absdeclor-of-dimb-table-fix-table
  (equal (dimb-absdeclor absdeclor (dimb-table-fix table))
         (dimb-absdeclor absdeclor table)))

Theorem: dimb-absdeclor-option-of-absdeclor-option-fix-absdeclor?

(defthm dimb-absdeclor-option-of-absdeclor-option-fix-absdeclor?
  (equal (dimb-absdeclor-option (absdeclor-option-fix absdeclor?)
                                table)
         (dimb-absdeclor-option absdeclor? table)))

Theorem: dimb-absdeclor-option-of-dimb-table-fix-table

(defthm dimb-absdeclor-option-of-dimb-table-fix-table
  (equal (dimb-absdeclor-option absdeclor? (dimb-table-fix table))
         (dimb-absdeclor-option absdeclor? table)))

Theorem: dimb-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor

(defthm dimb-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor
  (equal (dimb-dirabsdeclor (dirabsdeclor-fix dirabsdeclor)
                            table)
         (dimb-dirabsdeclor dirabsdeclor table)))

Theorem: dimb-dirabsdeclor-of-dimb-table-fix-table

(defthm dimb-dirabsdeclor-of-dimb-table-fix-table
  (equal (dimb-dirabsdeclor dirabsdeclor (dimb-table-fix table))
         (dimb-dirabsdeclor dirabsdeclor table)))

Theorem: dimb-dirabsdeclor-option-of-dirabsdeclor-option-fix-dirabsdeclor?

(defthm
  dimb-dirabsdeclor-option-of-dirabsdeclor-option-fix-dirabsdeclor?
 (equal
   (dimb-dirabsdeclor-option (dirabsdeclor-option-fix dirabsdeclor?)
                             table)
   (dimb-dirabsdeclor-option dirabsdeclor? table)))

Theorem: dimb-dirabsdeclor-option-of-dimb-table-fix-table

(defthm dimb-dirabsdeclor-option-of-dimb-table-fix-table
 (equal
     (dimb-dirabsdeclor-option dirabsdeclor? (dimb-table-fix table))
     (dimb-dirabsdeclor-option dirabsdeclor? table)))

Theorem: dimb-param-declon-of-param-declon-fix-param

(defthm dimb-param-declon-of-param-declon-fix-param
  (equal (dimb-param-declon (param-declon-fix param)
                            table)
         (dimb-param-declon param table)))

Theorem: dimb-param-declon-of-dimb-table-fix-table

(defthm dimb-param-declon-of-dimb-table-fix-table
  (equal (dimb-param-declon param (dimb-table-fix table))
         (dimb-param-declon param table)))

Theorem: dimb-param-declon-list-of-param-declon-list-fix-params

(defthm dimb-param-declon-list-of-param-declon-list-fix-params
  (equal (dimb-param-declon-list (param-declon-list-fix params)
                                 table)
         (dimb-param-declon-list params table)))

Theorem: dimb-param-declon-list-of-dimb-table-fix-table

(defthm dimb-param-declon-list-of-dimb-table-fix-table
  (equal (dimb-param-declon-list params (dimb-table-fix table))
         (dimb-param-declon-list params table)))

Theorem: dimb-param-declor-of-param-declor-fix-paramdeclor

(defthm dimb-param-declor-of-param-declor-fix-paramdeclor
  (equal (dimb-param-declor (param-declor-fix paramdeclor)
                            table)
         (dimb-param-declor paramdeclor table)))

Theorem: dimb-param-declor-of-dimb-table-fix-table

(defthm dimb-param-declor-of-dimb-table-fix-table
  (equal (dimb-param-declor paramdeclor (dimb-table-fix table))
         (dimb-param-declor paramdeclor table)))

Theorem: dimb-tyname-of-tyname-fix-tyname

(defthm dimb-tyname-of-tyname-fix-tyname
  (equal (dimb-tyname (tyname-fix tyname) table)
         (dimb-tyname tyname table)))

Theorem: dimb-tyname-of-dimb-table-fix-table

(defthm dimb-tyname-of-dimb-table-fix-table
  (equal (dimb-tyname tyname (dimb-table-fix table))
         (dimb-tyname tyname table)))

Theorem: dimb-struni-spec-of-struni-spec-fix-struni-spec

(defthm dimb-struni-spec-of-struni-spec-fix-struni-spec
  (equal (dimb-struni-spec (struni-spec-fix struni-spec)
                           table)
         (dimb-struni-spec struni-spec table)))

Theorem: dimb-struni-spec-of-dimb-table-fix-table

(defthm dimb-struni-spec-of-dimb-table-fix-table
  (equal (dimb-struni-spec struni-spec (dimb-table-fix table))
         (dimb-struni-spec struni-spec table)))

Theorem: dimb-struct-declon-of-struct-declon-fix-structdeclon

(defthm dimb-struct-declon-of-struct-declon-fix-structdeclon
  (equal (dimb-struct-declon (struct-declon-fix structdeclon)
                             table)
         (dimb-struct-declon structdeclon table)))

Theorem: dimb-struct-declon-of-dimb-table-fix-table

(defthm dimb-struct-declon-of-dimb-table-fix-table
  (equal (dimb-struct-declon structdeclon (dimb-table-fix table))
         (dimb-struct-declon structdeclon table)))

Theorem: dimb-struct-declon-list-of-struct-declon-list-fix-structdeclons

(defthm
    dimb-struct-declon-list-of-struct-declon-list-fix-structdeclons
 (equal
     (dimb-struct-declon-list (struct-declon-list-fix structdeclons)
                              table)
     (dimb-struct-declon-list structdeclons table)))

Theorem: dimb-struct-declon-list-of-dimb-table-fix-table

(defthm dimb-struct-declon-list-of-dimb-table-fix-table
 (equal
      (dimb-struct-declon-list structdeclons (dimb-table-fix table))
      (dimb-struct-declon-list structdeclons table)))

Theorem: dimb-struct-declor-of-struct-declor-fix-structdeclor

(defthm dimb-struct-declor-of-struct-declor-fix-structdeclor
  (equal (dimb-struct-declor (struct-declor-fix structdeclor)
                             table)
         (dimb-struct-declor structdeclor table)))

Theorem: dimb-struct-declor-of-dimb-table-fix-table

(defthm dimb-struct-declor-of-dimb-table-fix-table
  (equal (dimb-struct-declor structdeclor (dimb-table-fix table))
         (dimb-struct-declor structdeclor table)))

Theorem: dimb-struct-declor-list-of-struct-declor-list-fix-structdeclors

(defthm
    dimb-struct-declor-list-of-struct-declor-list-fix-structdeclors
 (equal
     (dimb-struct-declor-list (struct-declor-list-fix structdeclors)
                              table)
     (dimb-struct-declor-list structdeclors table)))

Theorem: dimb-struct-declor-list-of-dimb-table-fix-table

(defthm dimb-struct-declor-list-of-dimb-table-fix-table
 (equal
      (dimb-struct-declor-list structdeclors (dimb-table-fix table))
      (dimb-struct-declor-list structdeclors table)))

Theorem: dimb-enum-spec-of-enum-spec-fix-enumspec

(defthm dimb-enum-spec-of-enum-spec-fix-enumspec
  (equal (dimb-enum-spec (enum-spec-fix enumspec)
                         table)
         (dimb-enum-spec enumspec table)))

Theorem: dimb-enum-spec-of-dimb-table-fix-table

(defthm dimb-enum-spec-of-dimb-table-fix-table
  (equal (dimb-enum-spec enumspec (dimb-table-fix table))
         (dimb-enum-spec enumspec table)))

Theorem: dimb-enumer-of-enumer-fix-enumer

(defthm dimb-enumer-of-enumer-fix-enumer
  (equal (dimb-enumer (enumer-fix enumer) table)
         (dimb-enumer enumer table)))

Theorem: dimb-enumer-of-dimb-table-fix-table

(defthm dimb-enumer-of-dimb-table-fix-table
  (equal (dimb-enumer enumer (dimb-table-fix table))
         (dimb-enumer enumer table)))

Theorem: dimb-enumer-list-of-enumer-list-fix-enumers

(defthm dimb-enumer-list-of-enumer-list-fix-enumers
  (equal (dimb-enumer-list (enumer-list-fix enumers)
                           table)
         (dimb-enumer-list enumers table)))

Theorem: dimb-enumer-list-of-dimb-table-fix-table

(defthm dimb-enumer-list-of-dimb-table-fix-table
  (equal (dimb-enumer-list enumers (dimb-table-fix table))
         (dimb-enumer-list enumers table)))

Theorem: dimb-statassert-of-statassert-fix-statassert

(defthm dimb-statassert-of-statassert-fix-statassert
  (equal (dimb-statassert (statassert-fix statassert)
                          table)
         (dimb-statassert statassert table)))

Theorem: dimb-statassert-of-dimb-table-fix-table

(defthm dimb-statassert-of-dimb-table-fix-table
  (equal (dimb-statassert statassert (dimb-table-fix table))
         (dimb-statassert statassert table)))

Theorem: dimb-initdeclor-of-initdeclor-fix-ideclor

(defthm dimb-initdeclor-of-initdeclor-fix-ideclor
  (equal (dimb-initdeclor (initdeclor-fix ideclor)
                          kind table)
         (dimb-initdeclor ideclor kind table)))

Theorem: dimb-initdeclor-of-dimb-kind-fix-kind

(defthm dimb-initdeclor-of-dimb-kind-fix-kind
  (equal (dimb-initdeclor ideclor (dimb-kind-fix kind)
                          table)
         (dimb-initdeclor ideclor kind table)))

Theorem: dimb-initdeclor-of-dimb-table-fix-table

(defthm dimb-initdeclor-of-dimb-table-fix-table
  (equal (dimb-initdeclor ideclor kind (dimb-table-fix table))
         (dimb-initdeclor ideclor kind table)))

Theorem: dimb-initdeclor-list-of-initdeclor-list-fix-ideclors

(defthm dimb-initdeclor-list-of-initdeclor-list-fix-ideclors
  (equal (dimb-initdeclor-list (initdeclor-list-fix ideclors)
                               kind table)
         (dimb-initdeclor-list ideclors kind table)))

Theorem: dimb-initdeclor-list-of-dimb-kind-fix-kind

(defthm dimb-initdeclor-list-of-dimb-kind-fix-kind
  (equal (dimb-initdeclor-list ideclors (dimb-kind-fix kind)
                               table)
         (dimb-initdeclor-list ideclors kind table)))

Theorem: dimb-initdeclor-list-of-dimb-table-fix-table

(defthm dimb-initdeclor-list-of-dimb-table-fix-table
  (equal (dimb-initdeclor-list ideclors kind (dimb-table-fix table))
         (dimb-initdeclor-list ideclors kind table)))

Theorem: dimb-decl-of-decl-fix-decl

(defthm dimb-decl-of-decl-fix-decl
  (equal (dimb-decl (decl-fix decl) table)
         (dimb-decl decl table)))

Theorem: dimb-decl-of-dimb-table-fix-table

(defthm dimb-decl-of-dimb-table-fix-table
  (equal (dimb-decl decl (dimb-table-fix table))
         (dimb-decl decl table)))

Theorem: dimb-decl-list-of-decl-list-fix-decls

(defthm dimb-decl-list-of-decl-list-fix-decls
  (equal (dimb-decl-list (decl-list-fix decls)
                         table)
         (dimb-decl-list decls table)))

Theorem: dimb-decl-list-of-dimb-table-fix-table

(defthm dimb-decl-list-of-dimb-table-fix-table
  (equal (dimb-decl-list decls (dimb-table-fix table))
         (dimb-decl-list decls table)))

Theorem: dimb-label-of-label-fix-label

(defthm dimb-label-of-label-fix-label
  (equal (dimb-label (label-fix label) table)
         (dimb-label label table)))

Theorem: dimb-label-of-dimb-table-fix-table

(defthm dimb-label-of-dimb-table-fix-table
  (equal (dimb-label label (dimb-table-fix table))
         (dimb-label label table)))

Theorem: dimb-stmt-of-stmt-fix-stmt

(defthm dimb-stmt-of-stmt-fix-stmt
  (equal (dimb-stmt (stmt-fix stmt) table)
         (dimb-stmt stmt table)))

Theorem: dimb-stmt-of-dimb-table-fix-table

(defthm dimb-stmt-of-dimb-table-fix-table
  (equal (dimb-stmt stmt (dimb-table-fix table))
         (dimb-stmt stmt table)))

Theorem: dimb-comp-stmt-of-comp-stmt-fix-cstmt

(defthm dimb-comp-stmt-of-comp-stmt-fix-cstmt
  (equal (dimb-comp-stmt (comp-stmt-fix cstmt)
                         fundefp table)
         (dimb-comp-stmt cstmt fundefp table)))

Theorem: dimb-comp-stmt-of-bool-fix-fundefp

(defthm dimb-comp-stmt-of-bool-fix-fundefp
  (equal (dimb-comp-stmt cstmt (bool-fix fundefp)
                         table)
         (dimb-comp-stmt cstmt fundefp table)))

Theorem: dimb-comp-stmt-of-dimb-table-fix-table

(defthm dimb-comp-stmt-of-dimb-table-fix-table
  (equal (dimb-comp-stmt cstmt fundefp (dimb-table-fix table))
         (dimb-comp-stmt cstmt fundefp table)))

Theorem: dimb-block-item-of-block-item-fix-item

(defthm dimb-block-item-of-block-item-fix-item
  (equal (dimb-block-item (block-item-fix item)
                          table)
         (dimb-block-item item table)))

Theorem: dimb-block-item-of-dimb-table-fix-table

(defthm dimb-block-item-of-dimb-table-fix-table
  (equal (dimb-block-item item (dimb-table-fix table))
         (dimb-block-item item table)))

Theorem: dimb-block-item-list-of-block-item-list-fix-items

(defthm dimb-block-item-list-of-block-item-list-fix-items
  (equal (dimb-block-item-list (block-item-list-fix items)
                               table)
         (dimb-block-item-list items table)))

Theorem: dimb-block-item-list-of-dimb-table-fix-table

(defthm dimb-block-item-list-of-dimb-table-fix-table
  (equal (dimb-block-item-list items (dimb-table-fix table))
         (dimb-block-item-list items table)))

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

(defthm dimb-amb-expr/tyname-of-amb-expr/tyname-fix-expr/tyname
  (equal (dimb-amb-expr/tyname (amb-expr/tyname-fix expr/tyname)
                               add-parens-p table)
         (dimb-amb-expr/tyname expr/tyname add-parens-p table)))

Theorem: dimb-amb-expr/tyname-of-bool-fix-add-parens-p

(defthm dimb-amb-expr/tyname-of-bool-fix-add-parens-p
  (equal (dimb-amb-expr/tyname expr/tyname (bool-fix add-parens-p)
                               table)
         (dimb-amb-expr/tyname expr/tyname add-parens-p table)))

Theorem: dimb-amb-expr/tyname-of-dimb-table-fix-table

(defthm dimb-amb-expr/tyname-of-dimb-table-fix-table
  (equal (dimb-amb-expr/tyname expr/tyname
                               add-parens-p (dimb-table-fix table))
         (dimb-amb-expr/tyname expr/tyname add-parens-p table)))

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

(defthm
 dimb-amb-declor/absdeclor-of-amb-declor/absdeclor-fix-declor/absdeclor
 (equal (dimb-amb-declor/absdeclor
             (amb-declor/absdeclor-fix declor/absdeclor)
             table)
        (dimb-amb-declor/absdeclor declor/absdeclor table)))

Theorem: dimb-amb-declor/absdeclor-of-dimb-table-fix-table

(defthm dimb-amb-declor/absdeclor-of-dimb-table-fix-table
  (equal (dimb-amb-declor/absdeclor
              declor/absdeclor (dimb-table-fix table))
         (dimb-amb-declor/absdeclor declor/absdeclor table)))

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

(defthm dimb-amb-decl/stmt-of-amb-decl/stmt-fix-decl/stmt
  (equal (dimb-amb-decl/stmt (amb-decl/stmt-fix decl/stmt)
                             table)
         (dimb-amb-decl/stmt decl/stmt table)))

Theorem: dimb-amb-decl/stmt-of-dimb-table-fix-table

(defthm dimb-amb-decl/stmt-of-dimb-table-fix-table
  (equal (dimb-amb-decl/stmt decl/stmt (dimb-table-fix table))
         (dimb-amb-decl/stmt decl/stmt table)))

Theorem: dimb-expr-expr-equiv-congruence-on-expr

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

Theorem: dimb-expr-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-expr-list-expr-list-equiv-congruence-on-exprs

(defthm dimb-expr-list-expr-list-equiv-congruence-on-exprs
  (implies (expr-list-equiv exprs exprs-equiv)
           (equal (dimb-expr-list exprs table)
                  (dimb-expr-list exprs-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-expr-list-dimb-table-equiv-congruence-on-table

(defthm dimb-expr-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-expr-list exprs table)
                  (dimb-expr-list exprs table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-expr-option-expr-option-equiv-congruence-on-expr?

(defthm dimb-expr-option-expr-option-equiv-congruence-on-expr?
  (implies (expr-option-equiv expr? expr?-equiv)
           (equal (dimb-expr-option expr? table)
                  (dimb-expr-option expr?-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-expr-option-dimb-table-equiv-congruence-on-table

(defthm dimb-expr-option-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-expr-option expr? table)
                  (dimb-expr-option expr? table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-const-expr-const-expr-equiv-congruence-on-cexpr

(defthm dimb-const-expr-const-expr-equiv-congruence-on-cexpr
  (implies (const-expr-equiv cexpr cexpr-equiv)
           (equal (dimb-const-expr cexpr table)
                  (dimb-const-expr cexpr-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-const-expr-dimb-table-equiv-congruence-on-table

(defthm dimb-const-expr-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-const-expr cexpr table)
                  (dimb-const-expr cexpr table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-const-expr-option-const-expr-option-equiv-congruence-on-cexpr?

(defthm
 dimb-const-expr-option-const-expr-option-equiv-congruence-on-cexpr?
 (implies (const-expr-option-equiv cexpr? cexpr?-equiv)
          (equal (dimb-const-expr-option cexpr? table)
                 (dimb-const-expr-option cexpr?-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-const-expr-option-dimb-table-equiv-congruence-on-table

(defthm dimb-const-expr-option-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-const-expr-option cexpr? table)
                  (dimb-const-expr-option cexpr? table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-genassoc-genassoc-equiv-congruence-on-assoc

(defthm dimb-genassoc-genassoc-equiv-congruence-on-assoc
  (implies (genassoc-equiv assoc assoc-equiv)
           (equal (dimb-genassoc assoc table)
                  (dimb-genassoc assoc-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-genassoc-dimb-table-equiv-congruence-on-table

(defthm dimb-genassoc-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-genassoc assoc table)
                  (dimb-genassoc assoc table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-genassoc-list-genassoc-list-equiv-congruence-on-assocs

(defthm dimb-genassoc-list-genassoc-list-equiv-congruence-on-assocs
  (implies (genassoc-list-equiv assocs assocs-equiv)
           (equal (dimb-genassoc-list assocs table)
                  (dimb-genassoc-list assocs-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-genassoc-list-dimb-table-equiv-congruence-on-table

(defthm dimb-genassoc-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-genassoc-list assocs table)
                  (dimb-genassoc-list assocs table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-member-designor-member-designor-equiv-congruence-on-memdes

(defthm
    dimb-member-designor-member-designor-equiv-congruence-on-memdes
  (implies (member-designor-equiv memdes memdes-equiv)
           (equal (dimb-member-designor memdes table)
                  (dimb-member-designor memdes-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-member-designor-dimb-table-equiv-congruence-on-table

(defthm dimb-member-designor-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-member-designor memdes table)
                  (dimb-member-designor memdes table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-type-spec-type-spec-equiv-congruence-on-tyspec

(defthm dimb-type-spec-type-spec-equiv-congruence-on-tyspec
  (implies (type-spec-equiv tyspec tyspec-equiv)
           (equal (dimb-type-spec tyspec table)
                  (dimb-type-spec tyspec-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-type-spec-dimb-table-equiv-congruence-on-table

(defthm dimb-type-spec-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-type-spec tyspec table)
                  (dimb-type-spec tyspec table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-spec/qual-spec/qual-equiv-congruence-on-specqual

(defthm dimb-spec/qual-spec/qual-equiv-congruence-on-specqual
  (implies (spec/qual-equiv specqual specqual-equiv)
           (equal (dimb-spec/qual specqual table)
                  (dimb-spec/qual specqual-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-spec/qual-dimb-table-equiv-congruence-on-table

(defthm dimb-spec/qual-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-spec/qual specqual table)
                  (dimb-spec/qual specqual table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-spec/qual-list-spec/qual-list-equiv-congruence-on-specquals

(defthm
   dimb-spec/qual-list-spec/qual-list-equiv-congruence-on-specquals
  (implies (spec/qual-list-equiv specquals specquals-equiv)
           (equal (dimb-spec/qual-list specquals table)
                  (dimb-spec/qual-list specquals-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-spec/qual-list-dimb-table-equiv-congruence-on-table

(defthm dimb-spec/qual-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-spec/qual-list specquals table)
                  (dimb-spec/qual-list specquals table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-align-spec-align-spec-equiv-congruence-on-alignspec

(defthm dimb-align-spec-align-spec-equiv-congruence-on-alignspec
  (implies (align-spec-equiv alignspec alignspec-equiv)
           (equal (dimb-align-spec alignspec table)
                  (dimb-align-spec alignspec-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-align-spec-dimb-table-equiv-congruence-on-table

(defthm dimb-align-spec-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-align-spec alignspec table)
                  (dimb-align-spec alignspec table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-decl-spec-decl-spec-equiv-congruence-on-declspec

(defthm dimb-decl-spec-decl-spec-equiv-congruence-on-declspec
  (implies (decl-spec-equiv declspec declspec-equiv)
           (equal (dimb-decl-spec declspec kind table)
                  (dimb-decl-spec declspec-equiv kind table)))
  :rule-classes :congruence)

Theorem: dimb-decl-spec-dimb-kind-equiv-congruence-on-kind

(defthm dimb-decl-spec-dimb-kind-equiv-congruence-on-kind
  (implies (dimb-kind-equiv kind kind-equiv)
           (equal (dimb-decl-spec declspec kind table)
                  (dimb-decl-spec declspec kind-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-decl-spec-dimb-table-equiv-congruence-on-table

(defthm dimb-decl-spec-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-decl-spec declspec kind table)
                  (dimb-decl-spec declspec kind table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-decl-spec-list-decl-spec-list-equiv-congruence-on-declspecs

(defthm
   dimb-decl-spec-list-decl-spec-list-equiv-congruence-on-declspecs
  (implies (decl-spec-list-equiv declspecs declspecs-equiv)
           (equal (dimb-decl-spec-list declspecs kind table)
                  (dimb-decl-spec-list declspecs-equiv kind table)))
  :rule-classes :congruence)

Theorem: dimb-decl-spec-list-dimb-kind-equiv-congruence-on-kind

(defthm dimb-decl-spec-list-dimb-kind-equiv-congruence-on-kind
  (implies (dimb-kind-equiv kind kind-equiv)
           (equal (dimb-decl-spec-list declspecs kind table)
                  (dimb-decl-spec-list declspecs kind-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-decl-spec-list-dimb-table-equiv-congruence-on-table

(defthm dimb-decl-spec-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-decl-spec-list declspecs kind table)
                  (dimb-decl-spec-list declspecs kind table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-initer-initer-equiv-congruence-on-initer

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

Theorem: dimb-initer-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-initer-option-initer-option-equiv-congruence-on-initer?

(defthm dimb-initer-option-initer-option-equiv-congruence-on-initer?
  (implies (initer-option-equiv initer? initer?-equiv)
           (equal (dimb-initer-option initer? table)
                  (dimb-initer-option initer?-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-initer-option-dimb-table-equiv-congruence-on-table

(defthm dimb-initer-option-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-initer-option initer? table)
                  (dimb-initer-option initer? table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-desiniter-desiniter-equiv-congruence-on-desiniter

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

Theorem: dimb-desiniter-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-desiniter-list-desiniter-list-equiv-congruence-on-desiniters

(defthm
  dimb-desiniter-list-desiniter-list-equiv-congruence-on-desiniters
  (implies (desiniter-list-equiv desiniters desiniters-equiv)
           (equal (dimb-desiniter-list desiniters table)
                  (dimb-desiniter-list desiniters-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-desiniter-list-dimb-table-equiv-congruence-on-table

(defthm dimb-desiniter-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-desiniter-list desiniters table)
                  (dimb-desiniter-list desiniters table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-designor-designor-equiv-congruence-on-design

(defthm dimb-designor-designor-equiv-congruence-on-design
  (implies (designor-equiv design design-equiv)
           (equal (dimb-designor design table)
                  (dimb-designor design-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-designor-dimb-table-equiv-congruence-on-table

(defthm dimb-designor-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-designor design table)
                  (dimb-designor design table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-designor-list-designor-list-equiv-congruence-on-designs

(defthm dimb-designor-list-designor-list-equiv-congruence-on-designs
  (implies (designor-list-equiv designs designs-equiv)
           (equal (dimb-designor-list designs table)
                  (dimb-designor-list designs-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-designor-list-dimb-table-equiv-congruence-on-table

(defthm dimb-designor-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-designor-list designs table)
                  (dimb-designor-list designs table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-declor-declor-equiv-congruence-on-declor

(defthm dimb-declor-declor-equiv-congruence-on-declor
  (implies (declor-equiv declor declor-equiv)
           (equal (dimb-declor declor fundefp table)
                  (dimb-declor declor-equiv fundefp table)))
  :rule-classes :congruence)

Theorem: dimb-declor-iff-congruence-on-fundefp

(defthm dimb-declor-iff-congruence-on-fundefp
  (implies (iff fundefp fundefp-equiv)
           (equal (dimb-declor declor fundefp table)
                  (dimb-declor declor fundefp-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-declor-dimb-table-equiv-congruence-on-table

(defthm dimb-declor-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-declor declor fundefp table)
                  (dimb-declor declor fundefp table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-declor-option-declor-option-equiv-congruence-on-declor?

(defthm dimb-declor-option-declor-option-equiv-congruence-on-declor?
  (implies (declor-option-equiv declor? declor?-equiv)
           (equal (dimb-declor-option declor? table)
                  (dimb-declor-option declor?-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-declor-option-dimb-table-equiv-congruence-on-table

(defthm dimb-declor-option-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-declor-option declor? table)
                  (dimb-declor-option declor? table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor

(defthm dimb-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor
  (implies (dirdeclor-equiv dirdeclor dirdeclor-equiv)
           (equal (dimb-dirdeclor dirdeclor fundefp table)
                  (dimb-dirdeclor dirdeclor-equiv fundefp table)))
  :rule-classes :congruence)

Theorem: dimb-dirdeclor-iff-congruence-on-fundefp

(defthm dimb-dirdeclor-iff-congruence-on-fundefp
  (implies (iff fundefp fundefp-equiv)
           (equal (dimb-dirdeclor dirdeclor fundefp table)
                  (dimb-dirdeclor dirdeclor fundefp-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-dirdeclor-dimb-table-equiv-congruence-on-table

(defthm dimb-dirdeclor-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-dirdeclor dirdeclor fundefp table)
                  (dimb-dirdeclor dirdeclor fundefp table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-absdeclor-absdeclor-equiv-congruence-on-absdeclor

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

Theorem: dimb-absdeclor-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-absdeclor-option-absdeclor-option-equiv-congruence-on-absdeclor?

(defthm
 dimb-absdeclor-option-absdeclor-option-equiv-congruence-on-absdeclor?
 (implies (absdeclor-option-equiv absdeclor? absdeclor?-equiv)
          (equal (dimb-absdeclor-option absdeclor? table)
                 (dimb-absdeclor-option absdeclor?-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-absdeclor-option-dimb-table-equiv-congruence-on-table

(defthm dimb-absdeclor-option-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-absdeclor-option absdeclor? table)
                  (dimb-absdeclor-option absdeclor? table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor

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

Theorem: dimb-dirabsdeclor-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-dirabsdeclor-option-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor?

(defthm
 dimb-dirabsdeclor-option-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor?
 (implies
      (dirabsdeclor-option-equiv dirabsdeclor? dirabsdeclor?-equiv)
      (equal (dimb-dirabsdeclor-option dirabsdeclor? table)
             (dimb-dirabsdeclor-option dirabsdeclor?-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-dirabsdeclor-option-dimb-table-equiv-congruence-on-table

(defthm
      dimb-dirabsdeclor-option-dimb-table-equiv-congruence-on-table
  (implies
       (dimb-table-equiv table table-equiv)
       (equal (dimb-dirabsdeclor-option dirabsdeclor? table)
              (dimb-dirabsdeclor-option dirabsdeclor? table-equiv)))
  :rule-classes :congruence)

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

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

Theorem: dimb-param-declon-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-param-declon-list-param-declon-list-equiv-congruence-on-params

(defthm
 dimb-param-declon-list-param-declon-list-equiv-congruence-on-params
 (implies (param-declon-list-equiv params params-equiv)
          (equal (dimb-param-declon-list params table)
                 (dimb-param-declon-list params-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-param-declon-list-dimb-table-equiv-congruence-on-table

(defthm dimb-param-declon-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-param-declon-list params table)
                  (dimb-param-declon-list params table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-param-declor-param-declor-equiv-congruence-on-paramdeclor

(defthm
     dimb-param-declor-param-declor-equiv-congruence-on-paramdeclor
  (implies (param-declor-equiv paramdeclor paramdeclor-equiv)
           (equal (dimb-param-declor paramdeclor table)
                  (dimb-param-declor paramdeclor-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-param-declor-dimb-table-equiv-congruence-on-table

(defthm dimb-param-declor-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-param-declor paramdeclor table)
                  (dimb-param-declor paramdeclor table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-tyname-tyname-equiv-congruence-on-tyname

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

Theorem: dimb-tyname-dimb-table-equiv-congruence-on-table

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

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

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

Theorem: dimb-struni-spec-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-struct-declon-struct-declon-equiv-congruence-on-structdeclon

(defthm
  dimb-struct-declon-struct-declon-equiv-congruence-on-structdeclon
  (implies (struct-declon-equiv structdeclon structdeclon-equiv)
           (equal (dimb-struct-declon structdeclon table)
                  (dimb-struct-declon structdeclon-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-struct-declon-dimb-table-equiv-congruence-on-table

(defthm dimb-struct-declon-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-struct-declon structdeclon table)
                  (dimb-struct-declon structdeclon table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-struct-declon-list-struct-declon-list-equiv-congruence-on-structdeclons

(defthm
 dimb-struct-declon-list-struct-declon-list-equiv-congruence-on-structdeclons
 (implies
      (struct-declon-list-equiv structdeclons structdeclons-equiv)
      (equal (dimb-struct-declon-list structdeclons table)
             (dimb-struct-declon-list structdeclons-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-struct-declon-list-dimb-table-equiv-congruence-on-table

(defthm dimb-struct-declon-list-dimb-table-equiv-congruence-on-table
  (implies
       (dimb-table-equiv table table-equiv)
       (equal (dimb-struct-declon-list structdeclons table)
              (dimb-struct-declon-list structdeclons table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-struct-declor-struct-declor-equiv-congruence-on-structdeclor

(defthm
  dimb-struct-declor-struct-declor-equiv-congruence-on-structdeclor
  (implies (struct-declor-equiv structdeclor structdeclor-equiv)
           (equal (dimb-struct-declor structdeclor table)
                  (dimb-struct-declor structdeclor-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-struct-declor-dimb-table-equiv-congruence-on-table

(defthm dimb-struct-declor-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-struct-declor structdeclor table)
                  (dimb-struct-declor structdeclor table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-struct-declor-list-struct-declor-list-equiv-congruence-on-structdeclors

(defthm
 dimb-struct-declor-list-struct-declor-list-equiv-congruence-on-structdeclors
 (implies
      (struct-declor-list-equiv structdeclors structdeclors-equiv)
      (equal (dimb-struct-declor-list structdeclors table)
             (dimb-struct-declor-list structdeclors-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-struct-declor-list-dimb-table-equiv-congruence-on-table

(defthm dimb-struct-declor-list-dimb-table-equiv-congruence-on-table
  (implies
       (dimb-table-equiv table table-equiv)
       (equal (dimb-struct-declor-list structdeclors table)
              (dimb-struct-declor-list structdeclors table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-enum-spec-enum-spec-equiv-congruence-on-enumspec

(defthm dimb-enum-spec-enum-spec-equiv-congruence-on-enumspec
  (implies (enum-spec-equiv enumspec enumspec-equiv)
           (equal (dimb-enum-spec enumspec table)
                  (dimb-enum-spec enumspec-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-enum-spec-dimb-table-equiv-congruence-on-table

(defthm dimb-enum-spec-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-enum-spec enumspec table)
                  (dimb-enum-spec enumspec table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-enumer-enumer-equiv-congruence-on-enumer

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

Theorem: dimb-enumer-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-enumer-list-enumer-list-equiv-congruence-on-enumers

(defthm dimb-enumer-list-enumer-list-equiv-congruence-on-enumers
  (implies (enumer-list-equiv enumers enumers-equiv)
           (equal (dimb-enumer-list enumers table)
                  (dimb-enumer-list enumers-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-enumer-list-dimb-table-equiv-congruence-on-table

(defthm dimb-enumer-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-enumer-list enumers table)
                  (dimb-enumer-list enumers table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-statassert-statassert-equiv-congruence-on-statassert

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

Theorem: dimb-statassert-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-initdeclor-initdeclor-equiv-congruence-on-ideclor

(defthm dimb-initdeclor-initdeclor-equiv-congruence-on-ideclor
  (implies (initdeclor-equiv ideclor ideclor-equiv)
           (equal (dimb-initdeclor ideclor kind table)
                  (dimb-initdeclor ideclor-equiv kind table)))
  :rule-classes :congruence)

Theorem: dimb-initdeclor-dimb-kind-equiv-congruence-on-kind

(defthm dimb-initdeclor-dimb-kind-equiv-congruence-on-kind
  (implies (dimb-kind-equiv kind kind-equiv)
           (equal (dimb-initdeclor ideclor kind table)
                  (dimb-initdeclor ideclor kind-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-initdeclor-dimb-table-equiv-congruence-on-table

(defthm dimb-initdeclor-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-initdeclor ideclor kind table)
                  (dimb-initdeclor ideclor kind table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-initdeclor-list-initdeclor-list-equiv-congruence-on-ideclors

(defthm
  dimb-initdeclor-list-initdeclor-list-equiv-congruence-on-ideclors
  (implies (initdeclor-list-equiv ideclors ideclors-equiv)
           (equal (dimb-initdeclor-list ideclors kind table)
                  (dimb-initdeclor-list ideclors-equiv kind table)))
  :rule-classes :congruence)

Theorem: dimb-initdeclor-list-dimb-kind-equiv-congruence-on-kind

(defthm dimb-initdeclor-list-dimb-kind-equiv-congruence-on-kind
  (implies (dimb-kind-equiv kind kind-equiv)
           (equal (dimb-initdeclor-list ideclors kind table)
                  (dimb-initdeclor-list ideclors kind-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-initdeclor-list-dimb-table-equiv-congruence-on-table

(defthm dimb-initdeclor-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-initdeclor-list ideclors kind table)
                  (dimb-initdeclor-list ideclors kind table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-decl-decl-equiv-congruence-on-decl

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

Theorem: dimb-decl-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-decl-list-decl-list-equiv-congruence-on-decls

(defthm dimb-decl-list-decl-list-equiv-congruence-on-decls
  (implies (decl-list-equiv decls decls-equiv)
           (equal (dimb-decl-list decls table)
                  (dimb-decl-list decls-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-decl-list-dimb-table-equiv-congruence-on-table

(defthm dimb-decl-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-decl-list decls table)
                  (dimb-decl-list decls table-equiv)))
  :rule-classes :congruence)

Theorem: dimb-label-label-equiv-congruence-on-label

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

Theorem: dimb-label-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-stmt-stmt-equiv-congruence-on-stmt

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

Theorem: dimb-stmt-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-comp-stmt-comp-stmt-equiv-congruence-on-cstmt

(defthm dimb-comp-stmt-comp-stmt-equiv-congruence-on-cstmt
  (implies (comp-stmt-equiv cstmt cstmt-equiv)
           (equal (dimb-comp-stmt cstmt fundefp table)
                  (dimb-comp-stmt cstmt-equiv fundefp table)))
  :rule-classes :congruence)

Theorem: dimb-comp-stmt-iff-congruence-on-fundefp

(defthm dimb-comp-stmt-iff-congruence-on-fundefp
  (implies (iff fundefp fundefp-equiv)
           (equal (dimb-comp-stmt cstmt fundefp table)
                  (dimb-comp-stmt cstmt fundefp-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-comp-stmt-dimb-table-equiv-congruence-on-table

(defthm dimb-comp-stmt-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-comp-stmt cstmt fundefp table)
                  (dimb-comp-stmt cstmt fundefp table-equiv)))
  :rule-classes :congruence)

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

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

Theorem: dimb-block-item-dimb-table-equiv-congruence-on-table

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

Theorem: dimb-block-item-list-block-item-list-equiv-congruence-on-items

(defthm
     dimb-block-item-list-block-item-list-equiv-congruence-on-items
  (implies (block-item-list-equiv items items-equiv)
           (equal (dimb-block-item-list items table)
                  (dimb-block-item-list items-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-block-item-list-dimb-table-equiv-congruence-on-table

(defthm dimb-block-item-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-block-item-list items table)
                  (dimb-block-item-list items table-equiv)))
  :rule-classes :congruence)

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

(defthm
 dimb-amb-expr/tyname-amb-expr/tyname-equiv-congruence-on-expr/tyname
 (implies
  (amb-expr/tyname-equiv expr/tyname expr/tyname-equiv)
  (equal
       (dimb-amb-expr/tyname expr/tyname add-parens-p table)
       (dimb-amb-expr/tyname expr/tyname-equiv add-parens-p table)))
 :rule-classes :congruence)

Theorem: dimb-amb-expr/tyname-iff-congruence-on-add-parens-p

(defthm dimb-amb-expr/tyname-iff-congruence-on-add-parens-p
 (implies
  (iff add-parens-p add-parens-p-equiv)
  (equal
       (dimb-amb-expr/tyname expr/tyname add-parens-p table)
       (dimb-amb-expr/tyname expr/tyname add-parens-p-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-amb-expr/tyname-dimb-table-equiv-congruence-on-table

(defthm dimb-amb-expr/tyname-dimb-table-equiv-congruence-on-table
 (implies
  (dimb-table-equiv table table-equiv)
  (equal
       (dimb-amb-expr/tyname expr/tyname add-parens-p table)
       (dimb-amb-expr/tyname expr/tyname add-parens-p table-equiv)))
 :rule-classes :congruence)

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

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

Theorem: dimb-amb-declor/absdeclor-dimb-table-equiv-congruence-on-table

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

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

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

Theorem: dimb-amb-decl/stmt-dimb-table-equiv-congruence-on-table

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

Theorem: expr-unambp-of-dimb-expr

(defthm expr-unambp-of-dimb-expr
  (b* (((mv acl2::?erp ?new-expr ?new-table)
        (dimb-expr expr table)))
    (implies (not erp)
             (expr-unambp new-expr))))

Theorem: expr-list-unambp-of-dimb-expr-list

(defthm expr-list-unambp-of-dimb-expr-list
  (b* (((mv acl2::?erp ?new-exprs ?new-table)
        (dimb-expr-list exprs table)))
    (implies (not erp)
             (expr-list-unambp new-exprs))))

Theorem: expr-option-unambp-of-dimb-expr-option

(defthm expr-option-unambp-of-dimb-expr-option
  (b* (((mv acl2::?erp ?new-expr? ?new-table)
        (dimb-expr-option expr? table)))
    (implies (not erp)
             (expr-option-unambp new-expr?))))

Theorem: const-expr-unambp-of-dimb-const-expr

(defthm const-expr-unambp-of-dimb-const-expr
  (b* (((mv acl2::?erp ?new-cexpr ?new-table)
        (dimb-const-expr cexpr table)))
    (implies (not erp)
             (const-expr-unambp new-cexpr))))

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

(defthm const-expr-option-unambp-of-dimb-const-expr-option
  (b* (((mv acl2::?erp ?new-cexpr? ?new-table)
        (dimb-const-expr-option cexpr? table)))
    (implies (not erp)
             (const-expr-option-unambp new-cexpr?))))

Theorem: genassoc-unambp-of-dimb-genassoc

(defthm genassoc-unambp-of-dimb-genassoc
  (b* (((mv acl2::?erp ?new-assoc ?new-table)
        (dimb-genassoc assoc table)))
    (implies (not erp)
             (genassoc-unambp new-assoc))))

Theorem: genassoc-list-unambp-of-dimb-genassoc-list

(defthm genassoc-list-unambp-of-dimb-genassoc-list
  (b* (((mv acl2::?erp ?new-assocs ?new-table)
        (dimb-genassoc-list assocs table)))
    (implies (not erp)
             (genassoc-list-unambp new-assocs))))

Theorem: member-designor-unambp-of-dimb-member-designor

(defthm member-designor-unambp-of-dimb-member-designor
  (b* (((mv acl2::?erp ?new-memdes ?new-table)
        (dimb-member-designor memdes table)))
    (implies (not erp)
             (member-designor-unambp new-memdes))))

Theorem: type-spec-unambp-of-dimb-type-spec

(defthm type-spec-unambp-of-dimb-type-spec
  (b* (((mv acl2::?erp ?new-tyspec ?new-table)
        (dimb-type-spec tyspec table)))
    (implies (not erp)
             (type-spec-unambp new-tyspec))))

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

(defthm spec/qual-unambp-of-dimb-spec/qual
  (b* (((mv acl2::?erp ?new-specqual ?new-table)
        (dimb-spec/qual specqual table)))
    (implies (not erp)
             (spec/qual-unambp new-specqual))))

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

(defthm spec/qual-list-unambp-of-dimb-spec/qual-list
  (b* (((mv acl2::?erp ?new-specquals ?new-table)
        (dimb-spec/qual-list specquals table)))
    (implies (not erp)
             (spec/qual-list-unambp new-specquals))))

Theorem: align-spec-unambp-of-dimb-align-spec

(defthm align-spec-unambp-of-dimb-align-spec
  (b* (((mv acl2::?erp ?new-alignspec ?new-table)
        (dimb-align-spec alignspec table)))
    (implies (not erp)
             (align-spec-unambp new-alignspec))))

Theorem: decl-spec-unambp-of-dimb-decl-spec

(defthm decl-spec-unambp-of-dimb-decl-spec
  (b* (((mv acl2::?erp
            ?new-declspec ?new-kind ?new-table)
        (dimb-decl-spec declspec kind table)))
    (implies (not erp)
             (decl-spec-unambp new-declspec))))

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

(defthm decl-spec-list-unambp-of-dimb-decl-spec-list
  (b* (((mv acl2::?erp
            ?new-declspecs ?new-kind ?new-table)
        (dimb-decl-spec-list declspecs kind table)))
    (implies (not erp)
             (decl-spec-list-unambp new-declspecs))))

Theorem: initer-unambp-of-dimb-initer

(defthm initer-unambp-of-dimb-initer
  (b* (((mv acl2::?erp ?new-initer ?new-table)
        (dimb-initer initer table)))
    (implies (not erp)
             (initer-unambp new-initer))))

Theorem: initer-option-unambp-of-dimb-initer-option

(defthm initer-option-unambp-of-dimb-initer-option
  (b* (((mv acl2::?erp ?new-initer? ?new-table)
        (dimb-initer-option initer? table)))
    (implies (not erp)
             (initer-option-unambp new-initer?))))

Theorem: desiniter-unambp-of-dimb-desiniter

(defthm desiniter-unambp-of-dimb-desiniter
  (b* (((mv acl2::?erp ?new-desiniter ?new-table)
        (dimb-desiniter desiniter table)))
    (implies (not erp)
             (desiniter-unambp new-desiniter))))

Theorem: desiniter-list-unambp-of-dimb-desiniter-list

(defthm desiniter-list-unambp-of-dimb-desiniter-list
  (b* (((mv acl2::?erp ?new-desiniters ?new-table)
        (dimb-desiniter-list desiniters table)))
    (implies (not erp)
             (desiniter-list-unambp new-desiniters))))

Theorem: designor-unambp-of-dimb-designor

(defthm designor-unambp-of-dimb-designor
  (b* (((mv acl2::?erp ?new-design ?new-table)
        (dimb-designor design table)))
    (implies (not erp)
             (designor-unambp new-design))))

Theorem: designor-list-unambp-of-dimb-designor-list

(defthm designor-list-unambp-of-dimb-designor-list
  (b* (((mv acl2::?erp ?new-designs ?new-table)
        (dimb-designor-list designs table)))
    (implies (not erp)
             (designor-list-unambp new-designs))))

Theorem: declor-unambp-of-dimb-declor

(defthm declor-unambp-of-dimb-declor
  (b* (((mv acl2::?erp
            ?new-declor ?ident acl2::?table)
        (dimb-declor declor fundefp table)))
    (implies (not erp)
             (declor-unambp new-declor))))

Theorem: declor-option-unambp-of-dimb-declor-option

(defthm declor-option-unambp-of-dimb-declor-option
  (b* (((mv acl2::?erp
            ?new-declor? ?ident? ?new-table)
        (dimb-declor-option declor? table)))
    (implies (not erp)
             (declor-option-unambp new-declor?))))

Theorem: dirdeclor-unambp-of-dimb-dirdeclor

(defthm dirdeclor-unambp-of-dimb-dirdeclor
  (b* (((mv acl2::?erp
            ?new-dirdeclor ?ident ?new-table)
        (dimb-dirdeclor dirdeclor fundefp table)))
    (implies (not erp)
             (dirdeclor-unambp new-dirdeclor))))

Theorem: absdeclor-unambp-of-dimb-absdeclor

(defthm absdeclor-unambp-of-dimb-absdeclor
  (b* (((mv acl2::?erp ?new-absdeclor ?new-table)
        (dimb-absdeclor absdeclor table)))
    (implies (not erp)
             (absdeclor-unambp new-absdeclor))))

Theorem: absdeclor-option-unambp-of-dimb-absdeclor-option

(defthm absdeclor-option-unambp-of-dimb-absdeclor-option
  (b* (((mv acl2::?erp ?new-absdeclor? ?new-table)
        (dimb-absdeclor-option absdeclor? table)))
    (implies (not erp)
             (absdeclor-option-unambp new-absdeclor?))))

Theorem: dirabsdeclor-unambp-of-dimb-dirabsdeclor

(defthm dirabsdeclor-unambp-of-dimb-dirabsdeclor
  (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-table)
        (dimb-dirabsdeclor dirabsdeclor table)))
    (implies (not erp)
             (dirabsdeclor-unambp new-dirabsdeclor))))

Theorem: dirabsdeclor-option-unambp-of-dimb-dirabsdeclor-option

(defthm dirabsdeclor-option-unambp-of-dimb-dirabsdeclor-option
  (b* (((mv acl2::?erp
            ?new-dirabsdeclor? ?new-table)
        (dimb-dirabsdeclor-option dirabsdeclor? table)))
    (implies (not erp)
             (dirabsdeclor-option-unambp new-dirabsdeclor?))))

Theorem: param-declon-unambp-of-dimb-param-declon

(defthm param-declon-unambp-of-dimb-param-declon
  (b* (((mv acl2::?erp ?new-param ?new-table)
        (dimb-param-declon param table)))
    (implies (not erp)
             (param-declon-unambp new-param))))

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

(defthm param-declon-list-unambp-of-dimb-param-declon-list
  (b* (((mv acl2::?erp ?new-params ?new-table)
        (dimb-param-declon-list params table)))
    (implies (not erp)
             (param-declon-list-unambp new-params))))

Theorem: param-declor-unambp-of-dimb-param-declor

(defthm param-declor-unambp-of-dimb-param-declor
  (b* (((mv acl2::?erp ?new-paramdeclor ?new-table)
        (dimb-param-declor paramdeclor table)))
    (implies (not erp)
             (param-declor-unambp new-paramdeclor))))

Theorem: tyname-unambp-of-dimb-tyname

(defthm tyname-unambp-of-dimb-tyname
  (b* (((mv acl2::?erp ?new-tyname ?new-table)
        (dimb-tyname tyname table)))
    (implies (not erp)
             (tyname-unambp new-tyname))))

Theorem: struni-spec-unambp-of-dimb-struni-spec

(defthm struni-spec-unambp-of-dimb-struni-spec
  (b* (((mv acl2::?erp ?new-struni-spec ?new-table)
        (dimb-struni-spec struni-spec table)))
    (implies (not erp)
             (struni-spec-unambp new-struni-spec))))

Theorem: struct-declon-unambp-of-dimb-struct-declon

(defthm struct-declon-unambp-of-dimb-struct-declon
  (b* (((mv acl2::?erp ?new-structdeclon ?new-table)
        (dimb-struct-declon structdeclon table)))
    (implies (not erp)
             (struct-declon-unambp new-structdeclon))))

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

(defthm struct-declon-list-unambp-of-dimb-struct-declon-list
  (b* (((mv acl2::?erp
            ?new-structdeclons ?new-table)
        (dimb-struct-declon-list structdeclons table)))
    (implies (not erp)
             (struct-declon-list-unambp new-structdeclons))))

Theorem: struct-declor-unambp-of-dimb-struct-declor

(defthm struct-declor-unambp-of-dimb-struct-declor
  (b* (((mv acl2::?erp ?new-structdeclor ?new-table)
        (dimb-struct-declor structdeclor table)))
    (implies (not erp)
             (struct-declor-unambp new-structdeclor))))

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

(defthm struct-declor-list-unambp-of-dimb-struct-declor-list
  (b* (((mv acl2::?erp
            ?new-structdeclors ?new-table)
        (dimb-struct-declor-list structdeclors table)))
    (implies (not erp)
             (struct-declor-list-unambp new-structdeclors))))

Theorem: enum-spec-unambp-of-dimb-enum-spec

(defthm enum-spec-unambp-of-dimb-enum-spec
  (b* (((mv acl2::?erp ?new-enumspec ?new-table)
        (dimb-enum-spec enumspec table)))
    (implies (not erp)
             (enum-spec-unambp new-enumspec))))

Theorem: enumer-unambp-of-dimb-enumer

(defthm enumer-unambp-of-dimb-enumer
  (b* (((mv acl2::?erp ?new-enumer ?new-table)
        (dimb-enumer enumer table)))
    (implies (not erp)
             (enumer-unambp new-enumer))))

Theorem: enumer-list-unambp-of-dimb-enumer-list

(defthm enumer-list-unambp-of-dimb-enumer-list
  (b* (((mv acl2::?erp ?new-enumers ?new-table)
        (dimb-enumer-list enumers table)))
    (implies (not erp)
             (enumer-list-unambp new-enumers))))

Theorem: statassert-unambp-of-dimb-statassert

(defthm statassert-unambp-of-dimb-statassert
  (b* (((mv acl2::?erp ?new-statassert ?new-table)
        (dimb-statassert statassert table)))
    (implies (not erp)
             (statassert-unambp new-statassert))))

Theorem: initdeclor-unambp-of-dimb-initdeclor

(defthm initdeclor-unambp-of-dimb-initdeclor
  (b* (((mv acl2::?erp ?new-ideclor ?new-table)
        (dimb-initdeclor ideclor kind table)))
    (implies (not erp)
             (initdeclor-unambp new-ideclor))))

Theorem: initdeclor-list-unambp-of-dimb-initdeclor-list

(defthm initdeclor-list-unambp-of-dimb-initdeclor-list
  (b* (((mv acl2::?erp ?new-ideclors ?new-table)
        (dimb-initdeclor-list ideclors kind table)))
    (implies (not erp)
             (initdeclor-list-unambp new-ideclors))))

Theorem: decl-unambp-of-dimb-decl

(defthm decl-unambp-of-dimb-decl
  (b* (((mv acl2::?erp ?new-decl ?new-table)
        (dimb-decl decl table)))
    (implies (not erp)
             (decl-unambp new-decl))))

Theorem: decl-list-unambp-of-dimb-decl-list

(defthm decl-list-unambp-of-dimb-decl-list
  (b* (((mv acl2::?erp ?new-decls ?new-table)
        (dimb-decl-list decls table)))
    (implies (not erp)
             (decl-list-unambp new-decls))))

Theorem: label-unambp-of-dimb-label

(defthm label-unambp-of-dimb-label
  (b* (((mv acl2::?erp ?new-label ?new-table)
        (dimb-label label table)))
    (implies (not erp)
             (label-unambp new-label))))

Theorem: stmt-unambp-of-dimb-stmt

(defthm stmt-unambp-of-dimb-stmt
  (b* (((mv acl2::?erp ?new-stmt ?new-table)
        (dimb-stmt stmt table)))
    (implies (not erp)
             (stmt-unambp new-stmt))))

Theorem: comp-stmt-unambp-of-dimb-comp-stmt

(defthm comp-stmt-unambp-of-dimb-comp-stmt
  (b* (((mv acl2::?erp ?new-cstmt ?new-table)
        (dimb-comp-stmt cstmt fundefp table)))
    (implies (not erp)
             (comp-stmt-unambp new-cstmt))))

Theorem: block-item-unambp-of-dimb-block-item

(defthm block-item-unambp-of-dimb-block-item
  (b* (((mv acl2::?erp ?new-item ?new-table)
        (dimb-block-item item table)))
    (implies (not erp)
             (block-item-unambp new-item))))

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

(defthm block-item-list-unambp-of-dimb-block-item-list
  (b* (((mv acl2::?erp ?new-items ?new-table)
        (dimb-block-item-list items table)))
    (implies (not erp)
             (block-item-list-unambp new-items))))

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

(defthm expr/tyname-unambp-of-dimb-amb-expr/tyname
  (b* (((mv acl2::?erp ?expr-or-tyname ?new-table)
        (dimb-amb-expr/tyname expr/tyname add-parens-p table)))
    (implies (not erp)
             (expr/tyname-unambp expr-or-tyname))))

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

(defthm declor/absdeclor-unambp-of-dimb-amb-declor/absdeclor
  (b* (((mv acl2::?erp
            ?declor-or-absdeclor ?ident? ?new-table)
        (dimb-amb-declor/absdeclor declor/absdeclor table)))
    (implies (not erp)
             (declor/absdeclor-unambp declor-or-absdeclor))))

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

(defthm decl/stmt-unambp-of-dimb-amb-decl/stmt
  (b* (((mv acl2::?erp ?decl-or-stmt ?new-table)
        (dimb-amb-decl/stmt decl/stmt table)))
    (implies (not erp)
             (decl/stmt-unambp decl-or-stmt))))

Subtopics

Dimb-dirdeclor: Disambiguate a direct declarator.
Dimb-expr: Disambiguate an expression.
Dimb-amb-declor/absdeclor: Disambiguate an ambiguous declarator or abstract declarator.
Dimb-amb-expr/tyname: Disambiguate an ambiguous expression or type name.
Dimb-declor: Disambiguate a declarator.
Dimb-type-spec: Disambiguate a type specifier.
Dimb-param-declor: Disambiguate a parameter declarator.
Dimb-decl-spec: Disambiguate a declaration specifier.
Dimb-param-declon: Disambiguate a parameter declaration.
Dimb-amb-decl/stmt: Disambiguate an ambiguous declaration or statement.
Dimb-initdeclor: Disambiguate an initializer declarator.
Dimb-stmt: Disambiguate a statement.
Dimb-comp-stmt: Disambiguate a compound statement.
Dimb-declor-option: Disambiguate an optional declarator.
Dimb-enum-spec: Disambiguate an enumeration specifier.
Dimb-decl: Disambiguate a declaration.
Dimb-struct-declor: Disambiguate a structure declarator.
Dimb-initdeclor-list: Disambiguate a list of initializer declarators.
Dimb-decl-spec-list: Disambiguate a list of declaration specifiers.
Dimb-absdeclor: Disambiguate an abstract declarator.
Dimb-dirabsdeclor: Disambiguate a direct abstract declarator.
Dimb-align-spec: Disambiguate an alignment specifier.
Dimb-struni-spec: Disambiguate a structure or union specifier.
Dimb-spec/qual-list: Disambiguate a list of specifiers and qualifiers.
Dimb-spec/qual: Disambiguate a specifier or qualifier.
Dimb-param-declon-list: Disambiguate a list of parameter declarations.
Dimb-enumer-list: Disambiguate a list of enumerators.
Dimb-enumer: Disambiguate an enumerator.
Dimb-dirabsdeclor-option: Disambiguate an optional direct abstract declarator.
Dimb-block-item: Disambiguate a block item.
Dimb-struct-declor-list: Disambiguate a list of structure declarators.
Dimb-struct-declon-list: Disambiguate a list of structure declarations.
Dimb-struct-declon: Disambiguate a structure declaration.
Dimb-statassert: Disambiguate a static assertion declaration.
Dimb-label: Disambiguate a label.
Dimb-desiniter-list: Disambiguate a list of initializers with optional designations.
Dimb-desiniter: Disambiguate an initializer with optional designations.
Dimb-decl-list: Disambiguate a list of declarations.
Dimb-const-expr-option: Disambiguate an optional constant expression.
Dimb-absdeclor-option: Disambiguate an optional abstract declarator.
Dimb-member-designor: Disambiguate a member designator.
Dimb-initer-option: Disambiguate an optional initializer.
Dimb-genassoc-list: Disambiguate a list of generic associations.
Dimb-genassoc: Disambiguate a generic association.
Dimb-expr-option: Disambiguate an optional expression.
Dimb-expr-list: Disambiguate a list of expressions.
Dimb-designor-list: Disambiguate a list of designators.
Dimb-designor: Disambiguate a designator.
Dimb-const-expr: Disambiguate a constant expression.
Dimb-block-item-list: Disambiguate a list of block items.
Dimb-tyname: Disambiguate a type name.
Dimb-initer: Disambiguate an initializer.