		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-exprs/decls/stmts

Transform expressions, declarations, statements, and related entities.

For now we only generate theorems for certain kinds of expressions. We are in the process of extending the implementation to generate theorems for additional kinds of expressions and for other constructs.

Definitions and Theorems

Function: simpadd0-expr

(defun simpadd0-expr (expr gin)
 (declare (xargs :guard (and (exprp expr) (ginp gin))))
 (declare (xargs :guard (and (expr-unambp expr)
                             (expr-annop expr))))
 (let ((__function__ 'simpadd0-expr))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (expr-case
       expr :ident
       (xeq-expr-ident expr.ident expr.info gin)
       :const
       (xeq-expr-const expr.const expr.info gin)
       :string
       (mv (expr-fix expr) (gout-no-thm gin))
       :paren
       (b* (((mv new-inner gout)
             (simpadd0-expr expr.inner gin)))
         (mv (expr-paren new-inner) gout))
       :gensel
       (b* (((mv new-control (gout gout-control))
             (simpadd0-expr expr.control gin))
            (gin (gin-update gin gout-control))
            ((mv new-assocs (gout gout-assocs))
             (simpadd0-genassoc-list expr.assocs gin))
            (gin (gin-update gin gout-assocs)))
         (mv (make-expr-gensel :control new-control
                               :assocs new-assocs)
             (gout-no-thm gin)))
       :arrsub
       (b* (((mv new-arg1 (gout gout-arg1))
             (simpadd0-expr expr.arg1 gin))
            (gin (gin-update gin gout-arg1))
            ((mv new-arg2 (gout gout-arg2))
             (simpadd0-expr expr.arg2 gin))
            (gin (gin-update gin gout-arg2)))
         (mv (make-expr-arrsub :arg1 new-arg1
                               :arg2 new-arg2
                               :info expr.info)
             (gout-no-thm gin)))
       :funcall
       (b* (((mv new-fun (gout gout-fun))
             (simpadd0-expr expr.fun gin))
            (gin (gin-update gin gout-fun))
            ((mv new-args (gout gout-args))
             (simpadd0-expr-list expr.args gin))
            (gin (gin-update gin gout-args)))
         (mv (make-expr-funcall :fun new-fun
                                :args new-args
                                :info expr.info)
             (gout-no-thm gin)))
       :member
       (b* (((mv new-arg (gout gout-arg))
             (simpadd0-expr expr.arg gin))
            (gin (gin-update gin gout-arg)))
         (mv (make-expr-member :arg new-arg
                               :name expr.name)
             (gout-no-thm gin)))
       :memberp
       (b* (((mv new-arg (gout gout-arg))
             (simpadd0-expr expr.arg gin))
            (gin (gin-update gin gout-arg)))
         (mv (make-expr-memberp :arg new-arg
                                :name expr.name)
             (gout-no-thm gin)))
       :complit
       (b* (((mv new-type (gout gout-type))
             (simpadd0-tyname expr.type gin))
            (gin (gin-update gin gout-type))
            ((mv new-elems (gout gout-elems))
             (simpadd0-desiniter-list expr.elems gin))
            (gin (gin-update gin gout-elems)))
         (mv (make-expr-complit :type new-type
                                :elems new-elems
                                :final-comma expr.final-comma)
             (gout-no-thm gin)))
       :unary
       (b* (((mv new-arg (gout gout-arg))
             (simpadd0-expr expr.arg gin))
            (gin (gin-update gin gout-arg)))
         (xeq-expr-unary expr.op expr.arg new-arg
                         gout-arg.thm-name expr.info gin))
       :label-addr
       (mv (expr-fix expr) (gout-no-thm gin))
       :sizeof
       (b* (((mv new-type (gout gout-type))
             (simpadd0-tyname expr.type gin))
            (gin (gin-update gin gout-type)))
         (mv (expr-sizeof new-type)
             (gout-no-thm gin)))
       :alignof
       (b* (((mv new-type (gout gout-type))
             (simpadd0-tyname expr.type gin))
            (gin (gin-update gin gout-type)))
         (mv (make-expr-alignof :type new-type
                                :uscores expr.uscores)
             (gout-no-thm gin)))
       :cast
       (b* (((mv new-type (gout gout-type))
             (simpadd0-tyname expr.type gin))
            (gin (gin-update gin gout-type))
            ((mv new-arg (gout gout-arg))
             (simpadd0-expr expr.arg gin))
            (gin (gin-update gin gout-arg)))
         (xeq-expr-cast expr.type new-type gout-type.thm-name
                        expr.arg new-arg gout-arg.thm-name
                        (tyname->info expr.type)
                        gin))
       :binary
       (b* (((mv new-arg1 (gout gout-arg1))
             (simpadd0-expr expr.arg1 gin))
            (gin (gin-update gin gout-arg1))
            ((mv new-arg2 (gout gout-arg2))
             (simpadd0-expr expr.arg2 gin))
            (gin (gin-update gin gout-arg2)))
         (simpadd0-expr-binary expr.op expr.arg1 new-arg1
                               gout-arg1.thm-name expr.arg2 new-arg2
                               gout-arg2.thm-name expr.info gin))
       :cond
       (b* (((mv new-test (gout gout-test))
             (simpadd0-expr expr.test gin))
            (gin (gin-update gin gout-test))
            ((mv new-then (gout gout-then))
             (simpadd0-expr-option expr.then gin))
            (gin (gin-update gin gout-then))
            ((mv new-else (gout gout-else))
             (simpadd0-expr expr.else gin))
            (gin (gin-update gin gout-else)))
         (xeq-expr-cond expr.test
                        new-test gout-test.thm-name expr.then
                        new-then gout-then.thm-name expr.else
                        new-else gout-else.thm-name gin))
       :comma
       (b* (((mv new-first (gout gout-first))
             (simpadd0-expr expr.first gin))
            (gin (gin-update gin gout-first))
            ((mv new-next (gout gout-next))
             (simpadd0-expr expr.next gin))
            (gin (gin-update gin gout-next)))
         (mv (make-expr-comma :first new-first
                              :next new-next)
             (gout-no-thm gin)))
       :stmt
       (b* (((mv new-cstmt (gout gout-cstmt))
             (simpadd0-comp-stmt expr.stmt gin))
            (gin (gin-update gin gout-cstmt)))
         (mv (expr-stmt new-cstmt)
             (gout-no-thm gin)))
       :tycompat
       (b* (((mv new-type1 (gout gout-type1))
             (simpadd0-tyname expr.type1 gin))
            (gin (gin-update gin gout-type1))
            ((mv new-type2 (gout gout-type2))
             (simpadd0-tyname expr.type2 gin))
            (gin (gin-update gin gout-type2)))
         (mv (make-expr-tycompat :type1 new-type1
                                 :type2 new-type2)
             (gout-no-thm gin)))
       :offsetof
       (b* (((mv new-type (gout gout-type))
             (simpadd0-tyname expr.type gin))
            (gin (gin-update gin gout-type))
            ((mv new-member (gout gout-member))
             (simpadd0-member-designor expr.member gin))
            (gin (gin-update gin gout-member)))
         (mv (make-expr-offsetof :type new-type
                                 :member new-member)
             (gout-no-thm gin)))
       :va-arg
       (b* (((mv new-list (gout gout-list))
             (simpadd0-expr expr.list gin))
            (gin (gin-update gin gout-list))
            ((mv new-type (gout gout-type))
             (simpadd0-tyname expr.type gin))
            (gin (gin-update gin gout-type)))
         (mv (make-expr-va-arg :list new-list
                               :type new-type)
             (gout-no-thm gin)))
       :extension
       (b* (((mv new-expr (gout gout-expr))
             (simpadd0-expr expr.expr gin))
            (gin (gin-update gin gout-expr)))
         (mv (expr-extension new-expr)
             (gout-no-thm gin)))
       :otherwise (prog2$ (impossible)
                          (mv (irr-expr) (irr-gout)))))))

Function: simpadd0-expr-list

(defun simpadd0-expr-list (exprs gin)
  (declare (xargs :guard (and (expr-listp exprs) (ginp gin))))
  (declare (xargs :guard (and (expr-list-unambp exprs)
                              (expr-list-annop exprs))))
  (let ((__function__ 'simpadd0-expr-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp exprs))
          (mv nil (gout-no-thm gin)))
         ((mv new-expr (gout gout-expr))
          (simpadd0-expr (car exprs) gin))
         (gin (gin-update gin gout-expr))
         ((mv new-exprs (gout gout-exprs))
          (simpadd0-expr-list (cdr exprs) gin))
         (gin (gin-update gin gout-exprs)))
      (mv (cons new-expr new-exprs)
          (gout-no-thm gin)))))

Function: simpadd0-expr-option

(defun simpadd0-expr-option (expr? gin)
  (declare (xargs :guard (and (expr-optionp expr?) (ginp gin))))
  (declare (xargs :guard (and (expr-option-unambp expr?)
                              (expr-option-annop expr?))))
  (let ((__function__ 'simpadd0-expr-option))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (expr-option-case expr?
                        :some (simpadd0-expr expr?.val gin)
                        :none (mv nil (gout-no-thm gin))))))

Function: simpadd0-const-expr

(defun simpadd0-const-expr (cexpr gin)
  (declare (xargs :guard (and (const-exprp cexpr) (ginp gin))))
  (declare (xargs :guard (and (const-expr-unambp cexpr)
                              (const-expr-annop cexpr))))
  (let ((__function__ 'simpadd0-const-expr))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((mv new-expr (gout gout-expr))
          (simpadd0-expr (const-expr->expr cexpr)
                         gin))
         (gin (gin-update gin gout-expr)))
      (mv (const-expr new-expr)
          (gout-no-thm gin)))))

Function: simpadd0-const-expr-option

(defun simpadd0-const-expr-option (cexpr? gin)
  (declare (xargs :guard (and (const-expr-optionp cexpr?)
                              (ginp gin))))
  (declare (xargs :guard (and (const-expr-option-unambp cexpr?)
                              (const-expr-option-annop cexpr?))))
  (let ((__function__ 'simpadd0-const-expr-option))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (const-expr-option-case
           cexpr?
           :some (simpadd0-const-expr cexpr?.val gin)
           :none (mv nil (gout-no-thm gin))))))

Function: simpadd0-genassoc

(defun simpadd0-genassoc (genassoc gin)
  (declare (xargs :guard (and (genassocp genassoc) (ginp gin))))
  (declare (xargs :guard (and (genassoc-unambp genassoc)
                              (genassoc-annop genassoc))))
  (let ((__function__ 'simpadd0-genassoc))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (genassoc-case genassoc :type
                     (b* (((mv new-type (gout gout-type))
                           (simpadd0-tyname genassoc.type gin))
                          (gin (gin-update gin gout-type))
                          ((mv new-expr (gout gout-expr))
                           (simpadd0-expr genassoc.expr gin))
                          (gin (gin-update gin gout-expr)))
                       (mv (make-genassoc-type :type new-type
                                               :expr new-expr)
                           (gout-no-thm gin)))
                     :default
                     (b* (((mv new-expr (gout gout-expr))
                           (simpadd0-expr genassoc.expr gin))
                          (gin (gin-update gin gout-expr)))
                       (mv (genassoc-default new-expr)
                           (gout-no-thm gin)))))))

Function: simpadd0-genassoc-list

(defun simpadd0-genassoc-list (genassocs gin)
  (declare (xargs :guard (and (genassoc-listp genassocs)
                              (ginp gin))))
  (declare (xargs :guard (and (genassoc-list-unambp genassocs)
                              (genassoc-list-annop genassocs))))
  (let ((__function__ 'simpadd0-genassoc-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp genassocs))
          (mv nil (gout-no-thm gin)))
         ((mv new-assoc (gout gout-assoc))
          (simpadd0-genassoc (car genassocs) gin))
         (gin (gin-update gin gout-assoc))
         ((mv new-assocs (gout gout-assocs))
          (simpadd0-genassoc-list (cdr genassocs)
                                  gin))
         (gin (gin-update gin gout-assocs)))
      (mv (cons new-assoc new-assocs)
          (gout-no-thm gin)))))

Function: simpadd0-member-designor

(defun simpadd0-member-designor (memdes gin)
  (declare (xargs :guard (and (member-designorp memdes)
                              (ginp gin))))
  (declare (xargs :guard (and (member-designor-unambp memdes)
                              (member-designor-annop memdes))))
  (let ((__function__ 'simpadd0-member-designor))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (member-designor-case
           memdes :ident
           (mv (member-designor-fix memdes)
               (gout-no-thm gin))
           :dot
           (b* (((mv new-member (gout gout-member))
                 (simpadd0-member-designor memdes.member gin))
                (gin (gin-update gin gout-member)))
             (mv (make-member-designor-dot :member new-member
                                           :name memdes.name)
                 (gout-no-thm gin)))
           :sub
           (b* (((mv new-member (gout gout-member))
                 (simpadd0-member-designor memdes.member gin))
                (gin (gin-update gin gout-member))
                ((mv new-index (gout gout-index))
                 (simpadd0-expr memdes.index gin))
                (gin (gin-update gin gout-member)))
             (mv (make-member-designor-sub :member new-member
                                           :index new-index)
                 (gout-no-thm gin)))))))

Function: simpadd0-type-spec

(defun simpadd0-type-spec (tyspec gin)
 (declare (xargs :guard (and (type-specp tyspec) (ginp gin))))
 (declare (xargs :guard (and (type-spec-unambp tyspec)
                             (type-spec-annop tyspec))))
 (let ((__function__ 'simpadd0-type-spec))
   (declare (ignorable __function__))
   (b* (((gin gin) gin)
        (gout0 (gout-no-thm gin)))
     (type-spec-case
          tyspec
          :void (mv (type-spec-fix tyspec) gout0)
          :char (mv (type-spec-fix tyspec) gout0)
          :short (mv (type-spec-fix tyspec) gout0)
          :int (mv (type-spec-fix tyspec) gout0)
          :long (mv (type-spec-fix tyspec) gout0)
          :float (mv (type-spec-fix tyspec) gout0)
          :double
          (mv (type-spec-fix tyspec) gout0)
          :signed
          (mv (type-spec-fix tyspec) gout0)
          :unsigned
          (mv (type-spec-fix tyspec) gout0)
          :bool (mv (type-spec-fix tyspec) gout0)
          :complex
          (mv (type-spec-fix tyspec) gout0)
          :atomic
          (b* (((mv new-type (gout gout-type))
                (simpadd0-tyname tyspec.type gin))
               (gin (gin-update gin gout-type)))
            (mv (type-spec-atomic new-type)
                (gout-no-thm gin)))
          :struct
          (b* (((mv new-spec (gout gout-spec))
                (simpadd0-struni-spec tyspec.spec gin))
               (gin (gin-update gin gout-spec)))
            (mv (type-spec-struct new-spec)
                (gout-no-thm gin)))
          :union
          (b* (((mv new-spec (gout gout-spec))
                (simpadd0-struni-spec tyspec.spec gin))
               (gin (gin-update gin gout-spec)))
            (mv (type-spec-union new-spec)
                (gout-no-thm gin)))
          :enum
          (b* (((mv new-spec (gout gout-spec))
                (simpadd0-enum-spec tyspec.spec gin))
               (gin (gin-update gin gout-spec)))
            (mv (type-spec-enum new-spec)
                (gout-no-thm gin)))
          :typedef
          (mv (type-spec-fix tyspec) gout0)
          :int128
          (mv (type-spec-fix tyspec) gout0)
          :locase-float80
          (mv (type-spec-fix tyspec) gout0)
          :locase-float128
          (mv (type-spec-fix tyspec) gout0)
          :float16
          (mv (type-spec-fix tyspec) gout0)
          :float16x
          (mv (type-spec-fix tyspec) gout0)
          :float32
          (mv (type-spec-fix tyspec) gout0)
          :float32x
          (mv (type-spec-fix tyspec) gout0)
          :float64
          (mv (type-spec-fix tyspec) gout0)
          :float64x
          (mv (type-spec-fix tyspec) gout0)
          :float128
          (mv (type-spec-fix tyspec) gout0)
          :float128x
          (mv (type-spec-fix tyspec) gout0)
          :builtin-va-list
          (mv (type-spec-fix tyspec) gout0)
          :struct-empty
          (mv (type-spec-fix tyspec) gout0)
          :typeof-expr
          (b* (((mv new-expr (gout gout-expr))
                (simpadd0-expr tyspec.expr gin))
               (gin (gin-update gin gout-expr)))
            (mv (make-type-spec-typeof-expr :expr new-expr
                                            :uscores tyspec.uscores)
                (gout-no-thm gin)))
          :typeof-type
          (b* (((mv new-type (gout gout-type))
                (simpadd0-tyname tyspec.type gin))
               (gin (gin-update gin gout-type)))
            (mv (make-type-spec-typeof-type :type new-type
                                            :uscores tyspec.uscores)
                (gout-no-thm gin)))
          :typeof-ambig (prog2$ (impossible)
                                (mv (irr-type-spec) (irr-gout)))
          :auto-type (mv (type-spec-fix tyspec) gout0)))))

Function: simpadd0-spec/qual

(defun simpadd0-spec/qual (specqual gin)
  (declare (xargs :guard (and (spec/qual-p specqual)
                              (ginp gin))))
  (declare (xargs :guard (and (spec/qual-unambp specqual)
                              (spec/qual-annop specqual))))
  (let ((__function__ 'simpadd0-spec/qual))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (spec/qual-case specqual :typespec
                      (b* (((mv new-spec (gout gout-spec))
                            (simpadd0-type-spec specqual.spec gin))
                           (gin (gin-update gin gout-spec)))
                        (mv (spec/qual-typespec new-spec)
                            (gout-no-thm gin)))
                      :typequal
                      (mv (spec/qual-fix specqual)
                          (gout-no-thm gin))
                      :align
                      (b* (((mv new-spec (gout gout-spec))
                            (simpadd0-align-spec specqual.spec gin))
                           (gin (gin-update gin gout-spec)))
                        (mv (spec/qual-align new-spec)
                            (gout-no-thm gin)))
                      :attrib (mv (spec/qual-fix specqual)
                                  (gout-no-thm gin))))))

Function: simpadd0-spec/qual-list

(defun simpadd0-spec/qual-list (specquals gin)
  (declare (xargs :guard (and (spec/qual-listp specquals)
                              (ginp gin))))
  (declare (xargs :guard (and (spec/qual-list-unambp specquals)
                              (spec/qual-list-annop specquals))))
  (let ((__function__ 'simpadd0-spec/qual-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp specquals))
          (mv nil (gout-no-thm gin)))
         ((mv new-specqual (gout gout-specqual))
          (simpadd0-spec/qual (car specquals)
                              gin))
         (gin (gin-update gin gout-specqual))
         ((mv new-specquals (gout gout-specquals))
          (simpadd0-spec/qual-list (cdr specquals)
                                   gin))
         (gin (gin-update gin gout-specquals)))
      (mv (cons new-specqual new-specquals)
          (gout-no-thm gin)))))

Function: simpadd0-align-spec

(defun simpadd0-align-spec (alignspec gin)
 (declare (xargs :guard (and (align-specp alignspec)
                             (ginp gin))))
 (declare (xargs :guard (and (align-spec-unambp alignspec)
                             (align-spec-annop alignspec))))
 (let ((__function__ 'simpadd0-align-spec))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (align-spec-case
        alignspec :alignas-type
        (b* (((mv new-type (gout gout-type))
              (simpadd0-tyname alignspec.type gin))
             (gin (gin-update gin gout-type)))
          (mv (align-spec-alignas-type new-type)
              (gout-no-thm gin)))
        :alignas-expr
        (b* (((mv new-expr (gout gout-expr))
              (simpadd0-const-expr alignspec.expr gin))
             (gin (gin-update gin gout-expr)))
          (mv (align-spec-alignas-expr new-expr)
              (gout-no-thm gin)))
        :alignas-ambig (prog2$ (impossible)
                               (mv (irr-align-spec) (irr-gout)))))))

Function: simpadd0-decl-spec

(defun simpadd0-decl-spec (declspec gin)
  (declare (xargs :guard (and (decl-specp declspec) (ginp gin))))
  (declare (xargs :guard (and (decl-spec-unambp declspec)
                              (decl-spec-annop declspec))))
  (let ((__function__ 'simpadd0-decl-spec))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (decl-spec-case declspec :stoclass
                      (mv (decl-spec-fix declspec)
                          (gout-no-thm gin))
                      :typespec
                      (b* (((mv new-spec (gout gout-spec))
                            (simpadd0-type-spec declspec.spec gin))
                           (gin (gin-update gin gout-spec)))
                        (mv (decl-spec-typespec new-spec)
                            (gout-no-thm gin)))
                      :typequal
                      (mv (decl-spec-fix declspec)
                          (gout-no-thm gin))
                      :function
                      (mv (decl-spec-fix declspec)
                          (gout-no-thm gin))
                      :align
                      (b* (((mv new-spec (gout gout-spec))
                            (simpadd0-align-spec declspec.spec gin))
                           (gin (gin-update gin gout-spec)))
                        (mv (decl-spec-align new-spec)
                            (gout-no-thm gin)))
                      :attrib (mv (decl-spec-fix declspec)
                                  (gout-no-thm gin))
                      :stdcall (mv (decl-spec-fix declspec)
                                   (gout-no-thm gin))
                      :declspec (mv (decl-spec-fix declspec)
                                    (gout-no-thm gin))))))

Function: simpadd0-decl-spec-list

(defun simpadd0-decl-spec-list (declspecs gin)
  (declare (xargs :guard (and (decl-spec-listp declspecs)
                              (ginp gin))))
  (declare (xargs :guard (and (decl-spec-list-unambp declspecs)
                              (decl-spec-list-annop declspecs))))
  (let ((__function__ 'simpadd0-decl-spec-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp declspecs))
          (mv nil (gout-no-thm gin)))
         ((mv new-declspec (gout gout-declspec))
          (simpadd0-decl-spec (car declspecs)
                              gin))
         (gin (gin-update gin gout-declspec))
         ((mv new-declspecs (gout gout-declspecs))
          (simpadd0-decl-spec-list (cdr declspecs)
                                   gin))
         (gin (gin-update gin gout-declspecs)))
      (mv (cons new-declspec new-declspecs)
          (gout-no-thm gin)))))

Function: simpadd0-initer

(defun simpadd0-initer (initer gin)
  (declare (xargs :guard (and (initerp initer) (ginp gin))))
  (declare (xargs :guard (and (initer-unambp initer)
                              (initer-annop initer))))
  (let ((__function__ 'simpadd0-initer))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (initer-case
           initer :single
           (b* (((mv new-expr (gout gout-expr))
                 (simpadd0-expr initer.expr gin))
                (gin (gin-update gin gout-expr)))
             (xeq-initer-single initer.expr
                                new-expr gout-expr.thm-name gin))
           :list
           (b* (((mv new-elems (gout gout-elems))
                 (simpadd0-desiniter-list initer.elems gin))
                (gin (gin-update gin gout-elems)))
             (mv (make-initer-list :elems new-elems
                                   :final-comma initer.final-comma)
                 (gout-no-thm gin)))))))

Function: simpadd0-initer-option

(defun simpadd0-initer-option (initer? gin)
  (declare (xargs :guard (and (initer-optionp initer?)
                              (ginp gin))))
  (declare (xargs :guard (and (initer-option-unambp initer?)
                              (initer-option-annop initer?))))
  (let ((__function__ 'simpadd0-initer-option))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (initer-option-case initer?
                          :some (simpadd0-initer initer?.val gin)
                          :none (mv nil (gout-no-thm gin))))))

Function: simpadd0-desiniter

(defun simpadd0-desiniter (desiniter gin)
  (declare (xargs :guard (and (desiniterp desiniter)
                              (ginp gin))))
  (declare (xargs :guard (and (desiniter-unambp desiniter)
                              (desiniter-annop desiniter))))
  (let ((__function__ 'simpadd0-desiniter))
    (declare (ignorable __function__))
    (b* (((desiniter desiniter) desiniter)
         ((mv new-designors (gout gout-designors))
          (simpadd0-designor-list desiniter.designors gin))
         ((mv new-initer (gout gout-initer))
          (simpadd0-initer desiniter.initer gin))
         (gin (gin-update gin gout-initer)))
      (mv (make-desiniter :designors new-designors
                          :initer new-initer)
          (gout-no-thm gin)))))

Function: simpadd0-desiniter-list

(defun simpadd0-desiniter-list (desiniters gin)
  (declare (xargs :guard (and (desiniter-listp desiniters)
                              (ginp gin))))
  (declare (xargs :guard (and (desiniter-list-unambp desiniters)
                              (desiniter-list-annop desiniters))))
  (let ((__function__ 'simpadd0-desiniter-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp desiniters))
          (mv nil (gout-no-thm gin)))
         ((mv new-desiniter (gout gout-desiniter))
          (simpadd0-desiniter (car desiniters)
                              gin))
         (gin (gin-update gin gout-desiniter))
         ((mv new-desiniters (gout gout-desiniters))
          (simpadd0-desiniter-list (cdr desiniters)
                                   gin))
         (gin (gin-update gin gout-desiniters)))
      (mv (cons new-desiniter new-desiniters)
          (gout-no-thm gin)))))

Function: simpadd0-designor

(defun simpadd0-designor (designor gin)
  (declare (xargs :guard (and (designorp designor) (ginp gin))))
  (declare (xargs :guard (and (designor-unambp designor)
                              (designor-annop designor))))
  (let ((__function__ 'simpadd0-designor))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (designor-case
           designor :sub
           (b* (((mv new-index (gout gout-index))
                 (simpadd0-const-expr designor.index gin))
                (gin (gin-update gin gout-index))
                ((mv new-range? (gout gout-range?))
                 (simpadd0-const-expr-option designor.range? gin))
                (gin (gin-update gin gout-range?)))
             (mv (make-designor-sub :index new-index
                                    :range? new-range?)
                 (gout-no-thm gin)))
           :dot (mv (designor-fix designor)
                    (gout-no-thm gin))))))

Function: simpadd0-designor-list

(defun simpadd0-designor-list (designors gin)
  (declare (xargs :guard (and (designor-listp designors)
                              (ginp gin))))
  (declare (xargs :guard (and (designor-list-unambp designors)
                              (designor-list-annop designors))))
  (let ((__function__ 'simpadd0-designor-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp designors))
          (mv nil (gout-no-thm gin)))
         ((mv new-designor (gout gout-designor))
          (simpadd0-designor (car designors) gin))
         (gin (gin-update gin gout-designor))
         ((mv new-designors (gout gout-designors))
          (simpadd0-designor-list (cdr designors)
                                  gin))
         (gin (gin-update gin gout-designors)))
      (mv (cons new-designor new-designors)
          (gout-no-thm gin)))))

Function: simpadd0-declor

(defun simpadd0-declor (declor fundefp gin)
  (declare (xargs :guard (and (declorp declor)
                              (booleanp fundefp)
                              (ginp gin))))
  (declare (xargs :guard (and (declor-unambp declor)
                              (declor-annop declor))))
  (let ((__function__ 'simpadd0-declor))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((declor declor) declor)
         ((mv new-direct fundefp (gout gout-direct))
          (simpadd0-dirdeclor declor.direct fundefp gin))
         (gin (gin-update gin gout-direct)))
      (mv (make-declor :pointers declor.pointers
                       :direct new-direct)
          fundefp
          (change-gout (gout-no-thm gin)
                       :vartys gout-direct.vartys)))))

Function: simpadd0-declor-option

(defun simpadd0-declor-option (declor? gin)
 (declare (xargs :guard (and (declor-optionp declor?)
                             (ginp gin))))
 (declare (xargs :guard (and (declor-option-unambp declor?)
                             (declor-option-annop declor?))))
 (let ((__function__ 'simpadd0-declor-option))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (declor-option-case declor? :some
                       (b* (((mv new-declor & gout)
                             (simpadd0-declor declor?.val nil gin)))
                         (mv new-declor gout))
                       :none (mv nil (gout-no-thm gin))))))

Function: simpadd0-dirdeclor

(defun simpadd0-dirdeclor (dirdeclor fundefp gin)
 (declare (xargs :guard (and (dirdeclorp dirdeclor)
                             (booleanp fundefp)
                             (ginp gin))))
 (declare (xargs :guard (and (dirdeclor-unambp dirdeclor)
                             (dirdeclor-annop dirdeclor))))
 (let ((__function__ 'simpadd0-dirdeclor))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (dirdeclor-case
    dirdeclor :ident
    (mv (dirdeclor-fix dirdeclor)
        (acl2::bool-fix fundefp)
        (gout-no-thm gin))
    :paren
    (b* (((mv new-declor fundefp (gout gout-declor))
          (simpadd0-declor dirdeclor.inner fundefp gin))
         (gin (gin-update gin gout-declor)))
      (mv (dirdeclor-paren new-declor)
          fundefp (gout-no-thm gin)))
    :array
    (b* (((mv new-decl fundefp (gout gout-decl))
          (simpadd0-dirdeclor dirdeclor.declor fundefp gin))
         (gin (gin-update gin gout-decl))
         ((mv new-expr? (gout gout-expr?))
          (simpadd0-expr-option dirdeclor.size? gin))
         (gin (gin-update gin gout-expr?)))
      (mv (make-dirdeclor-array :declor new-decl
                                :qualspecs dirdeclor.qualspecs
                                :size? new-expr?)
          fundefp (gout-no-thm gin)))
    :array-static1
    (b* (((mv new-decl fundefp (gout gout-decl))
          (simpadd0-dirdeclor dirdeclor.declor fundefp gin))
         (gin (gin-update gin gout-decl))
         ((mv new-expr (gout gout-expr))
          (simpadd0-expr dirdeclor.size gin))
         (gin (gin-update gin gout-expr)))
     (mv
        (make-dirdeclor-array-static1 :declor new-decl
                                      :qualspecs dirdeclor.qualspecs
                                      :size new-expr)
        fundefp (gout-no-thm gin)))
    :array-static2
    (b* (((mv new-decl fundefp (gout gout-decl))
          (simpadd0-dirdeclor dirdeclor.declor fundefp gin))
         (gin (gin-update gin gout-decl))
         ((mv new-expr (gout gout-expr))
          (simpadd0-expr dirdeclor.size gin))
         (gin (gin-update gin gout-expr)))
     (mv
        (make-dirdeclor-array-static2 :declor new-decl
                                      :qualspecs dirdeclor.qualspecs
                                      :size new-expr)
        fundefp (gout-no-thm gin)))
    :array-star
    (b* (((mv new-decl fundefp (gout gout-decl))
          (simpadd0-dirdeclor dirdeclor.declor fundefp gin))
         (gin (gin-update gin gout-decl)))
      (mv (make-dirdeclor-array-star :declor new-decl
                                     :qualspecs dirdeclor.qualspecs)
          fundefp (gout-no-thm gin)))
    :function-params
    (b* (((mv new-declor fundefp (gout gout-declor))
          (simpadd0-dirdeclor dirdeclor.declor fundefp gin))
         (gin (gin-update gin gout-declor))
         ((mv new-params (gout gout-params))
          (simpadd0-param-declon-list dirdeclor.params gin))
         (gin (gin-update gin gout-params))
         (gout (if fundefp (change-gout (gout-no-thm gin)
                                        :vartys gout-params.vartys)
                 (gout-no-thm gin))))
     (mv
       (make-dirdeclor-function-params :declor new-declor
                                       :params new-params
                                       :ellipsis dirdeclor.ellipsis)
       nil gout))
    :function-names
    (b* (((mv new-declor & (gout gout-declor))
          (simpadd0-dirdeclor dirdeclor.declor fundefp gin))
         (gin (gin-update gin gout-declor)))
      (mv (make-dirdeclor-function-names :declor new-declor
                                         :names dirdeclor.names)
          nil (gout-no-thm gin)))))))

Function: simpadd0-absdeclor

(defun simpadd0-absdeclor (absdeclor gin)
  (declare (xargs :guard (and (absdeclorp absdeclor)
                              (ginp gin))))
  (declare (xargs :guard (and (absdeclor-unambp absdeclor)
                              (absdeclor-annop absdeclor))))
  (let ((__function__ 'simpadd0-absdeclor))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((absdeclor absdeclor) absdeclor)
         ((mv new-direct? (gout gout-direct?))
          (simpadd0-dirabsdeclor-option absdeclor.direct? gin))
         (gin (gin-update gin gout-direct?)))
      (mv (make-absdeclor :pointers absdeclor.pointers
                          :direct? new-direct?)
          (gout-no-thm gin)))))

Function: simpadd0-absdeclor-option

(defun simpadd0-absdeclor-option (absdeclor? gin)
  (declare (xargs :guard (and (absdeclor-optionp absdeclor?)
                              (ginp gin))))
  (declare (xargs :guard (and (absdeclor-option-unambp absdeclor?)
                              (absdeclor-option-annop absdeclor?))))
  (let ((__function__ 'simpadd0-absdeclor-option))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (absdeclor-option-case
           absdeclor?
           :some (simpadd0-absdeclor absdeclor?.val gin)
           :none (mv nil (gout-no-thm gin))))))

Function: simpadd0-dirabsdeclor

(defun simpadd0-dirabsdeclor (dirabsdeclor gin)
 (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor)
                             (ginp gin))))
 (declare (xargs :guard (and (dirabsdeclor-unambp dirabsdeclor)
                             (dirabsdeclor-annop dirabsdeclor))))
 (let ((__function__ 'simpadd0-dirabsdeclor))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (dirabsdeclor-case
    dirabsdeclor :dummy-base
    (prog2$ (raise "Misusage error: ~x0."
                   (dirabsdeclor-fix dirabsdeclor))
            (mv (irr-dirabsdeclor) (irr-gout)))
    :paren
    (b* (((mv new-inner (gout gout-inner))
          (simpadd0-absdeclor dirabsdeclor.inner gin))
         (gin (gin-update gin gout-inner)))
      (mv (dirabsdeclor-paren new-inner)
          (gout-no-thm gin)))
    :array
    (b* (((mv new-declor? (gout gout-declor?))
          (simpadd0-dirabsdeclor-option dirabsdeclor.declor? gin))
         (gin (gin-update gin gout-declor?))
         ((mv new-size? (gout gout-expr?))
          (simpadd0-expr-option dirabsdeclor.size? gin))
         (gin (gin-update gin gout-expr?)))
      (mv (make-dirabsdeclor-array :declor? new-declor?
                                   :qualspecs dirabsdeclor.qualspecs
                                   :size? new-size?)
          (gout-no-thm gin)))
    :array-static1
    (b* (((mv new-declor? (gout gout-declor?))
          (simpadd0-dirabsdeclor-option dirabsdeclor.declor? gin))
         (gin (gin-update gin gout-declor?))
         ((mv new-size (gout gout-expr))
          (simpadd0-expr dirabsdeclor.size gin))
         (gin (gin-update gin gout-expr)))
      (mv (make-dirabsdeclor-array-static1
               :declor? new-declor?
               :qualspecs dirabsdeclor.qualspecs
               :size new-size)
          (gout-no-thm gin)))
    :array-static2
    (b* (((mv new-declor? (gout gout-declor?))
          (simpadd0-dirabsdeclor-option dirabsdeclor.declor? gin))
         (gin (gin-update gin gout-declor?))
         ((mv new-size (gout gout-expr))
          (simpadd0-expr dirabsdeclor.size gin))
         (gin (gin-update gin gout-expr)))
      (mv (make-dirabsdeclor-array-static2
               :declor? new-declor?
               :qualspecs dirabsdeclor.qualspecs
               :size new-size)
          (gout-no-thm gin)))
    :array-star
    (b* (((mv new-declor? (gout gout-declor?))
          (simpadd0-dirabsdeclor-option dirabsdeclor.declor? gin))
         (gin (gin-update gin gout-declor?)))
      (mv (dirabsdeclor-array-star new-declor?)
          (gout-no-thm gin)))
    :function
    (b* (((mv new-declor? (gout gout-declor?))
          (simpadd0-dirabsdeclor-option dirabsdeclor.declor? gin))
         (gin (gin-update gin gout-declor?))
         ((mv new-params (gout gout-params))
          (simpadd0-param-declon-list dirabsdeclor.params gin))
         (gin (gin-update gin gout-params)))
     (mv
        (make-dirabsdeclor-function :declor? new-declor?
                                    :params new-params
                                    :ellipsis dirabsdeclor.ellipsis)
        (gout-no-thm gin)))))))

Function: simpadd0-dirabsdeclor-option

(defun simpadd0-dirabsdeclor-option (dirabsdeclor? gin)
 (declare (xargs :guard (and (dirabsdeclor-optionp dirabsdeclor?)
                             (ginp gin))))
 (declare
     (xargs :guard (and (dirabsdeclor-option-unambp dirabsdeclor?)
                        (dirabsdeclor-option-annop dirabsdeclor?))))
 (let ((__function__ 'simpadd0-dirabsdeclor-option))
   (declare (ignorable __function__))
   (b* (((gin gin) gin))
     (dirabsdeclor-option-case
          dirabsdeclor?
          :some (simpadd0-dirabsdeclor dirabsdeclor?.val gin)
          :none (mv nil (gout-no-thm gin))))))

Function: simpadd0-param-declon

(defun simpadd0-param-declon (paramdeclon gin)
  (declare (xargs :guard (and (param-declonp paramdeclon)
                              (ginp gin))))
  (declare (xargs :guard (and (param-declon-unambp paramdeclon)
                              (param-declon-annop paramdeclon))))
  (let ((__function__ 'simpadd0-param-declon))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((param-declon paramdeclon) paramdeclon)
         ((mv new-specs (gout gout-specs))
          (simpadd0-decl-spec-list paramdeclon.specs gin))
         (gin (gin-update gin gout-specs))
         ((mv new-declor (gout gout-declor))
          (simpadd0-param-declor paramdeclon.declor gin))
         (gin (gin-update gin gout-declor)))
      (mv (make-param-declon :specs new-specs
                             :declor new-declor
                             :attribs paramdeclon.attribs)
          (change-gout (gout-no-thm gin)
                       :vartys gout-declor.vartys)))))

Function: simpadd0-param-declon-list

(defun simpadd0-param-declon-list (paramdeclons gin)
  (declare (xargs :guard (and (param-declon-listp paramdeclons)
                              (ginp gin))))
  (declare
       (xargs :guard (and (param-declon-list-unambp paramdeclons)
                          (param-declon-list-annop paramdeclons))))
  (let ((__function__ 'simpadd0-param-declon-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp paramdeclons))
          (mv nil (gout-no-thm gin)))
         ((mv new-paramdeclon (gout gout-paramdeclon))
          (simpadd0-param-declon (car paramdeclons)
                                 gin))
         (gin (gin-update gin gout-paramdeclon))
         ((mv new-paramdeclons
              (gout gout-paramdeclons))
          (simpadd0-param-declon-list
               (cdr paramdeclons)
               (change-gin gin
                           :vartys gout-paramdeclon.vartys)))
         (gin (gin-update gin gout-paramdeclons)))
      (mv (cons new-paramdeclon new-paramdeclons)
          (change-gout (gout-no-thm gin)
                       :vartys gout-paramdeclons.vartys)))))

Function: simpadd0-param-declor

(defun simpadd0-param-declor (paramdeclor gin)
 (declare (xargs :guard (and (param-declorp paramdeclor)
                             (ginp gin))))
 (declare (xargs :guard (and (param-declor-unambp paramdeclor)
                             (param-declor-annop paramdeclor))))
 (let ((__function__ 'simpadd0-param-declor))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (param-declor-case
     paramdeclor :nonabstract
     (b*
      (((mv new-declor & (gout gout-declor))
        (simpadd0-declor paramdeclor.declor nil gin))
       (gin (gin-update gin gout-declor))
       (type (param-declor-nonabstract-info->type paramdeclor.info))
       (ident (declor->ident paramdeclor.declor))
       (post-vartys (if (and (ident-formalp ident)
                             (type-formalp type)
                             (not (type-case type :void))
                             (not (type-case type :char)))
                        (b* (((mv & cvar) (ldm-ident ident))
                             ((mv & ctype) (ldm-type type)))
                          (omap::update cvar ctype gin.vartys))
                      gin.vartys)))
      (mv (make-param-declor-nonabstract :declor new-declor
                                         :info paramdeclor.info)
          (change-gout (gout-no-thm gin)
                       :vartys post-vartys)))
     :abstract
     (b* (((mv new-absdeclor (gout gout-absdeclor))
           (simpadd0-absdeclor paramdeclor.declor gin))
          (gin (gin-update gin gout-absdeclor)))
       (mv (param-declor-abstract new-absdeclor)
           (gout-no-thm gin)))
     :none (mv (param-declor-none)
               (gout-no-thm gin))
     :ambig (prog2$ (impossible)
                    (mv (irr-param-declor) (irr-gout)))))))

Function: simpadd0-tyname

(defun simpadd0-tyname (tyname gin)
  (declare (xargs :guard (and (tynamep tyname) (ginp gin))))
  (declare (xargs :guard (and (tyname-unambp tyname)
                              (tyname-annop tyname))))
  (let ((__function__ 'simpadd0-tyname))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((tyname tyname) tyname)
         ((mv new-specquals (gout gout-specqual))
          (simpadd0-spec/qual-list tyname.specquals gin))
         (gin (gin-update gin gout-specqual))
         ((mv new-declor? (gout gout-declor?))
          (simpadd0-absdeclor-option tyname.declor? gin))
         (gin (gin-update gin gout-declor?)))
      (mv (make-tyname :specquals new-specquals
                       :declor? new-declor?
                       :info tyname.info)
          (gout-no-thm gin)))))

Function: simpadd0-struni-spec

(defun simpadd0-struni-spec (struni-spec gin)
  (declare (xargs :guard (and (struni-specp struni-spec)
                              (ginp gin))))
  (declare (xargs :guard (and (struni-spec-unambp struni-spec)
                              (struni-spec-annop struni-spec))))
  (let ((__function__ 'simpadd0-struni-spec))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((struni-spec struni-spec) struni-spec)
         ((mv new-members (gout gout-members))
          (simpadd0-struct-declon-list struni-spec.members gin))
         (gin (gin-update gin gout-members)))
      (mv (make-struni-spec :attribs struni-spec.attribs
                            :name? struni-spec.name?
                            :members new-members)
          (gout-no-thm gin)))))

Function: simpadd0-struct-declon

(defun simpadd0-struct-declon (structdeclon gin)
 (declare (xargs :guard (and (struct-declonp structdeclon)
                             (ginp gin))))
 (declare (xargs :guard (and (struct-declon-unambp structdeclon)
                             (struct-declon-annop structdeclon))))
 (let ((__function__ 'simpadd0-struct-declon))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (struct-declon-case
    structdeclon :member
    (b* (((mv new-specquals (gout gout-specqual))
          (simpadd0-spec/qual-list structdeclon.specquals gin))
         (gin (gin-update gin gout-specqual))
         ((mv new-declors (gout gout-declor))
          (simpadd0-struct-declor-list structdeclon.declors gin))
         (gin (gin-update gin gout-declor)))
     (mv
        (make-struct-declon-member :extension structdeclon.extension
                                   :specquals new-specquals
                                   :declors new-declors
                                   :attribs structdeclon.attribs)
        (gout-no-thm gin)))
    :statassert
    (b* (((mv new-structdeclon
              (gout gout-structdeclon))
          (simpadd0-statassert structdeclon.statassert gin))
         (gin (gin-update gin gout-structdeclon)))
      (mv (struct-declon-statassert new-structdeclon)
          (gout-no-thm gin)))
    :empty (mv (struct-declon-empty)
               (gout-no-thm gin))))))

Function: simpadd0-struct-declon-list

(defun simpadd0-struct-declon-list (structdeclons gin)
 (declare (xargs :guard (and (struct-declon-listp structdeclons)
                             (ginp gin))))
 (declare
      (xargs :guard (and (struct-declon-list-unambp structdeclons)
                         (struct-declon-list-annop structdeclons))))
 (let ((__function__ 'simpadd0-struct-declon-list))
   (declare (ignorable __function__))
   (b* (((gin gin) gin)
        ((when (endp structdeclons))
         (mv nil (gout-no-thm gin)))
        ((mv new-structdeclon
             (gout gout-structdeclon))
         (simpadd0-struct-declon (car structdeclons)
                                 gin))
        (gin (gin-update gin gout-structdeclon))
        ((mv new-structdeclons
             (gout gout-structdeclons))
         (simpadd0-struct-declon-list (cdr structdeclons)
                                      gin))
        (gin (gin-update gin gout-structdeclons)))
     (mv (cons new-structdeclon new-structdeclons)
         (gout-no-thm gin)))))

Function: simpadd0-struct-declor

(defun simpadd0-struct-declor (structdeclor gin)
  (declare (xargs :guard (and (struct-declorp structdeclor)
                              (ginp gin))))
  (declare (xargs :guard (and (struct-declor-unambp structdeclor)
                              (struct-declor-annop structdeclor))))
  (let ((__function__ 'simpadd0-struct-declor))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((struct-declor structdeclor)
          structdeclor)
         ((mv new-declor? (gout gout-declor?))
          (simpadd0-declor-option structdeclor.declor? gin))
         (gin (gin-update gin gout-declor?))
         ((mv new-expr? (gout gout-expr?))
          (simpadd0-const-expr-option structdeclor.expr? gin))
         (gin (gin-update gin gout-expr?)))
      (mv (make-struct-declor :declor? new-declor?
                              :expr? new-expr?)
          (gout-no-thm gin)))))

Function: simpadd0-struct-declor-list

(defun simpadd0-struct-declor-list (structdeclors gin)
 (declare (xargs :guard (and (struct-declor-listp structdeclors)
                             (ginp gin))))
 (declare
      (xargs :guard (and (struct-declor-list-unambp structdeclors)
                         (struct-declor-list-annop structdeclors))))
 (let ((__function__ 'simpadd0-struct-declor-list))
   (declare (ignorable __function__))
   (b* (((gin gin) gin)
        ((when (endp structdeclors))
         (mv nil (gout-no-thm gin)))
        ((mv new-structdeclor
             (gout gout-structdeclor))
         (simpadd0-struct-declor (car structdeclors)
                                 gin))
        (gin (gin-update gin gout-structdeclor))
        ((mv new-structdeclors
             (gout gout-structdeclors))
         (simpadd0-struct-declor-list (cdr structdeclors)
                                      gin))
        (gin (gin-update gin gout-structdeclors)))
     (mv (cons new-structdeclor new-structdeclors)
         (gout-no-thm gin)))))

Function: simpadd0-enum-spec

(defun simpadd0-enum-spec (enumspec gin)
  (declare (xargs :guard (and (enum-specp enumspec) (ginp gin))))
  (declare (xargs :guard (and (enum-spec-unambp enumspec)
                              (enum-spec-annop enumspec))))
  (let ((__function__ 'simpadd0-enum-spec))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((enum-spec enumspec) enumspec)
         ((mv new-list (gout gout-list))
          (simpadd0-enumer-list enumspec.list gin))
         (gin (gin-update gin gout-list)))
      (mv (make-enum-spec :name enumspec.name
                          :list new-list
                          :final-comma enumspec.final-comma)
          (gout-no-thm gin)))))

Function: simpadd0-enumer

(defun simpadd0-enumer (enumer gin)
  (declare (xargs :guard (and (enumerp enumer) (ginp gin))))
  (declare (xargs :guard (and (enumer-unambp enumer)
                              (enumer-annop enumer))))
  (let ((__function__ 'simpadd0-enumer))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((enumer enumer) enumer)
         ((mv new-value (gout gout-value))
          (simpadd0-const-expr-option enumer.value gin))
         (gin (gin-update gin gout-value)))
      (mv (make-enumer :name enumer.name
                       :value new-value)
          (gout-no-thm gin)))))

Function: simpadd0-enumer-list

(defun simpadd0-enumer-list (enumers gin)
  (declare (xargs :guard (and (enumer-listp enumers)
                              (ginp gin))))
  (declare (xargs :guard (and (enumer-list-unambp enumers)
                              (enumer-list-annop enumers))))
  (let ((__function__ 'simpadd0-enumer-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp enumers))
          (mv nil (gout-no-thm gin)))
         ((mv new-enumer (gout gout-enumer))
          (simpadd0-enumer (car enumers) gin))
         (gin (gin-update gin gout-enumer))
         ((mv new-enumers (gout gout-enumers))
          (simpadd0-enumer-list (cdr enumers)
                                gin))
         (gin (gin-update gin gout-enumers)))
      (mv (cons new-enumer new-enumers)
          (gout-no-thm gin)))))

Function: simpadd0-statassert

(defun simpadd0-statassert (statassert gin)
  (declare (xargs :guard (and (statassertp statassert)
                              (ginp gin))))
  (declare (xargs :guard (and (statassert-unambp statassert)
                              (statassert-annop statassert))))
  (let ((__function__ 'simpadd0-statassert))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((statassert statassert) statassert)
         ((mv new-test (gout gout-test))
          (simpadd0-const-expr statassert.test gin))
         (gin (gin-update gin gout-test)))
      (mv (make-statassert :test new-test
                           :message statassert.message)
          (gout-no-thm gin)))))

Function: simpadd0-initdeclor

(defun simpadd0-initdeclor (initdeclor gin)
 (declare (xargs :guard (and (initdeclorp initdeclor)
                             (ginp gin))))
 (declare (xargs :guard (and (initdeclor-unambp initdeclor)
                             (initdeclor-annop initdeclor))))
 (let ((__function__ 'simpadd0-initdeclor))
  (declare (ignorable __function__))
  (b*
   (((initdeclor initdeclor) initdeclor)
    ((mv new-declor & (gout gout-declor))
     (simpadd0-declor initdeclor.declor nil gin))
    (gin (gin-update gin gout-declor))
    ((mv new-init? (gout gout-init?))
     (simpadd0-initer-option
          initdeclor.init?
          (change-gin gin
                      :vartys gout-declor.vartys)))
    ((gin gin) (gin-update gin gout-init?))
    (type (initdeclor-info->type initdeclor.info))
    (ident (declor->ident initdeclor.declor))
    (post-vartys
         (if (and (not (initdeclor-info->typedefp initdeclor.info))
                  (ident-formalp ident)
                  (type-formalp type)
                  (not (type-case type :void))
                  (not (type-case type :char)))
             (b* (((mv & cvar) (ldm-ident ident))
                  ((mv & ctype) (ldm-type type)))
               (omap::update cvar ctype gout-init?.vartys))
           gout-init?.vartys)))
   (mv
    (make-initdeclor :declor new-declor
                     :asm? initdeclor.asm?
                     :attribs initdeclor.attribs
                     :init? new-init?
                     :info initdeclor.info)
    (if gout-init?.thm-name (make-gout :events gin.events
                                       :thm-index gin.thm-index
                                       :thm-name gout-init?.thm-name
                                       :vartys post-vartys)
      (change-gout (gout-no-thm gin)
                   :vartys post-vartys))))))

Function: simpadd0-initdeclor-list

(defun simpadd0-initdeclor-list (initdeclors gin)
  (declare (xargs :guard (and (initdeclor-listp initdeclors)
                              (ginp gin))))
  (declare (xargs :guard (and (initdeclor-list-unambp initdeclors)
                              (initdeclor-list-annop initdeclors))))
  (let ((__function__ 'simpadd0-initdeclor-list))
    (declare (ignorable __function__))
    (b* (((when (endp initdeclors))
          (mv nil (gout-no-thm gin)))
         ((mv new-initdeclor (gout gout-initdeclor))
          (simpadd0-initdeclor (car initdeclors)
                               gin))
         (gin (gin-update gin gout-initdeclor))
         ((mv new-initdeclors (gout gout-initdeclors))
          (simpadd0-initdeclor-list
               (cdr initdeclors)
               (change-gin gin
                           :vartys gout-initdeclor.vartys)))
         ((gin gin)
          (gin-update gin gout-initdeclors)))
      (mv (cons new-initdeclor new-initdeclors)
          (if (and (not (consp new-initdeclors))
                   gout-initdeclor.thm-name)
              (make-gout :events gin.events
                         :thm-index gin.thm-index
                         :thm-name gout-initdeclor.thm-name
                         :vartys gout-initdeclor.vartys)
            (change-gout (gout-no-thm gin)
                         :vartys gout-initdeclors.vartys))))))

Function: simpadd0-decl

(defun simpadd0-decl (decl gin)
  (declare (xargs :guard (and (declp decl) (ginp gin))))
  (declare (xargs :guard (and (decl-unambp decl)
                              (decl-annop decl))))
  (let ((__function__ 'simpadd0-decl))
    (declare (ignorable __function__))
    (decl-case
         decl :decl
         (b* (((mv new-specs (gout gout-specs))
               (simpadd0-decl-spec-list decl.specs gin))
              (gin (gin-update gin gout-specs))
              ((mv new-init (gout gout-init))
               (simpadd0-initdeclor-list decl.init gin))
              ((gin gin) (gin-update gin gout-init)))
           (xeq-decl-decl decl.extension
                          decl.specs new-specs gout-specs.thm-name
                          decl.init new-init gout-init.thm-name
                          gout-init.vartys gin))
         :statassert
         (b* (((mv new-decl (gout gout-decl))
               (simpadd0-statassert decl.statassert gin))
              (gin (gin-update gin gout-decl)))
           (mv (decl-statassert new-decl)
               (gout-no-thm gin))))))

Function: simpadd0-decl-list

(defun simpadd0-decl-list (decls gin)
 (declare (xargs :guard (and (decl-listp decls) (ginp gin))))
 (declare (xargs :guard (and (decl-list-unambp decls)
                             (decl-list-annop decls))))
 (let ((__function__ 'simpadd0-decl-list))
   (declare (ignorable __function__))
   (b* (((gin gin) gin)
        ((when (endp decls))
         (mv nil (gout-no-thm gin)))
        ((mv new-decl (gout gout-decl))
         (simpadd0-decl (car decls) gin))
        (gin (gin-update gin gout-decl))
        ((mv new-decls (gout gout-decls))
         (simpadd0-decl-list (cdr decls)
                             (change-gin gin
                                         :vartys gout-decl.vartys)))
        (gin (gin-update gin gout-decls)))
     (mv (cons new-decl new-decls)
         (change-gout (gout-no-thm gin)
                      :vartys gout-decls.vartys)))))

Function: simpadd0-label

(defun simpadd0-label (label gin)
 (declare (xargs :guard (and (labelp label) (ginp gin))))
 (declare (xargs :guard (and (label-unambp label)
                             (label-annop label))))
 (let ((__function__ 'simpadd0-label))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
    (label-case label :name
                (mv (label-fix label) (gout-no-thm gin))
                :casexpr
                (b* (((mv new-expr (gout gout-expr))
                      (simpadd0-const-expr label.expr gin))
                     (gin (gin-update gin gout-expr))
                     ((mv new-range? (gout gout-range?))
                      (simpadd0-const-expr-option label.range? gin))
                     (gin (gin-update gin gout-range?)))
                  (mv (make-label-casexpr :expr new-expr
                                          :range? new-range?)
                      (gout-no-thm gin)))
                :default (mv (label-fix label)
                             (gout-no-thm gin))))))

Function: simpadd0-stmt

(defun simpadd0-stmt (stmt gin)
  (declare (xargs :guard (and (stmtp stmt) (ginp gin))))
  (declare (xargs :guard (and (stmt-unambp stmt)
                              (stmt-annop stmt))))
  (let ((__function__ 'simpadd0-stmt))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (stmt-case
           stmt :labeled
           (b* (((mv new-label (gout gout-label))
                 (simpadd0-label stmt.label gin))
                (gin (gin-update gin gout-label))
                ((mv new-stmt (gout gout-stmt))
                 (simpadd0-stmt stmt.stmt gin))
                (gin (gin-update gin gout-stmt)))
             (mv (make-stmt-labeled :label new-label
                                    :stmt new-stmt)
                 (gout-no-thm gin)))
           :compound
           (b* (((mv new-cstmt (gout gout-cstmt))
                 (simpadd0-comp-stmt stmt.stmt gin))
                (gin (gin-update gin gout-cstmt)))
             (xeq-stmt-compound stmt.stmt
                                new-cstmt gout-cstmt.thm-name gin))
           :expr
           (b* (((mv new-expr? (gout gout-expr?))
                 (simpadd0-expr-option stmt.expr? gin))
                (gin (gin-update gin gout-expr?)))
             (xeq-stmt-expr stmt.expr? new-expr?
                            gout-expr?.thm-name stmt.info gin))
           :if
           (b* (((mv new-test (gout gout-test))
                 (simpadd0-expr stmt.test gin))
                (gin (gin-update gin gout-test))
                ((mv new-then (gout gout-then))
                 (simpadd0-stmt stmt.then gin))
                (gin (gin-update gin gout-then)))
             (xeq-stmt-if stmt.test
                          new-test gout-test.thm-name stmt.then
                          new-then gout-then.thm-name gin))
           :ifelse
           (b* (((mv new-test (gout gout-test))
                 (simpadd0-expr stmt.test gin))
                (gin (gin-update gin gout-test))
                ((mv new-then (gout gout-then))
                 (simpadd0-stmt stmt.then gin))
                (gin (gin-update gin gout-then))
                ((mv new-else (gout gout-else))
                 (simpadd0-stmt stmt.else gin))
                (gin (gin-update gin gout-else)))
             (xeq-stmt-ifelse stmt.test
                              new-test gout-test.thm-name stmt.then
                              new-then gout-then.thm-name stmt.else
                              new-else gout-else.thm-name gin))
           :switch
           (b* (((mv new-target (gout gout-target))
                 (simpadd0-expr stmt.target gin))
                (gin (gin-update gin gout-target))
                ((mv new-body (gout gout-body))
                 (simpadd0-stmt stmt.body gin))
                (gin (gin-update gin gout-body)))
             (mv (make-stmt-switch :target new-target
                                   :body new-body)
                 (gout-no-thm gin)))
           :while
           (b* (((mv new-test (gout gout-test))
                 (simpadd0-expr stmt.test gin))
                (gin (gin-update gin gout-test))
                ((mv new-body (gout gout-body))
                 (simpadd0-stmt stmt.body gin))
                (gin (gin-update gin gout-body)))
             (xeq-stmt-while stmt.test
                             new-test gout-test.thm-name stmt.body
                             new-body gout-body.thm-name gin))
           :dowhile
           (b* (((mv new-body (gout gout-body))
                 (simpadd0-stmt stmt.body gin))
                (gin (gin-update gin gout-body))
                ((mv new-test (gout gout-test))
                 (simpadd0-expr stmt.test gin))
                (gin (gin-update gin gout-test)))
             (xeq-stmt-dowhile stmt.body
                               new-body gout-body.thm-name stmt.test
                               new-test gout-test.thm-name gin))
           :for-expr
           (b* (((mv new-init (gout gout-init))
                 (simpadd0-expr-option stmt.init gin))
                (gin (gin-update gin gout-init))
                ((mv new-test (gout gout-test))
                 (simpadd0-expr-option stmt.test gin))
                (gin (gin-update gin gout-test))
                ((mv new-next (gout gout-next))
                 (simpadd0-expr-option stmt.next gin))
                (gin (gin-update gin gout-next))
                ((mv new-body (gout gout-body))
                 (simpadd0-stmt stmt.body gin))
                (gin (gin-update gin gout-body)))
             (mv (make-stmt-for-expr :init new-init
                                     :test new-test
                                     :next new-next
                                     :body new-body)
                 (gout-no-thm gin)))
           :for-decl
           (b* (((mv new-init (gout gout-init))
                 (simpadd0-decl stmt.init gin))
                (gin (gin-update gin gout-init))
                (gin1 (change-gin gin
                                  :vartys gout-init.vartys))
                ((mv new-test (gout gout-test))
                 (simpadd0-expr-option stmt.test gin1))
                (gin (gin-update gin gout-test))
                ((mv new-next (gout gout-next))
                 (simpadd0-expr-option stmt.next gin1))
                (gin (gin-update gin gout-next))
                ((mv new-body (gout gout-body))
                 (simpadd0-stmt stmt.body gin1))
                (gin (gin-update gin gout-body)))
             (mv (make-stmt-for-decl :init new-init
                                     :test new-test
                                     :next new-next
                                     :body new-body)
                 (gout-no-thm gin)))
           :for-ambig
           (prog2$ (impossible)
                   (mv (irr-stmt) (irr-gout)))
           :goto
           (mv (stmt-fix stmt) (gout-no-thm gin))
           :gotoe
           (b* (((mv new-label gout)
                 (simpadd0-expr stmt.label gin)))
             (mv (stmt-gotoe new-label) gout))
           :continue
           (mv (stmt-fix stmt) (gout-no-thm gin))
           :break
           (mv (stmt-fix stmt) (gout-no-thm gin))
           :return
           (b* (((mv new-expr? (gout gout-expr?))
                 (simpadd0-expr-option stmt.expr? gin))
                (gin (gin-update gin gout-expr?)))
             (xeq-stmt-return stmt.expr? new-expr?
                              gout-expr?.thm-name stmt.info gin))
           :asm (mv (stmt-fix stmt)
                    (gout-no-thm gin))))))

Function: simpadd0-comp-stmt

(defun simpadd0-comp-stmt (cstmt gin)
  (declare (xargs :guard (and (comp-stmtp cstmt) (ginp gin))))
  (declare (xargs :guard (and (comp-stmt-unambp cstmt)
                              (comp-stmt-annop cstmt))))
  (let ((__function__ 'simpadd0-comp-stmt))
    (declare (ignorable __function__))
    (b* (((comp-stmt cstmt) cstmt)
         ((mv items gout)
          (simpadd0-block-item-list cstmt.items gin)))
      (mv (make-comp-stmt :labels cstmt.labels
                          :items items)
          gout))))

Function: simpadd0-block-item

(defun simpadd0-block-item (item gin)
 (declare (xargs :guard (and (block-itemp item) (ginp gin))))
 (declare (xargs :guard (and (block-item-unambp item)
                             (block-item-annop item))))
 (let ((__function__ 'simpadd0-block-item))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (block-item-case
        item :decl
        (b* (((mv new-decl (gout gout-decl))
              (simpadd0-decl item.decl gin))
             (gin (gin-update gin gout-decl)))
          (xeq-block-item-decl item.decl new-decl gout-decl.thm-name
                               item.info gout-decl.vartys gin))
        :stmt
        (b* (((mv new-stmt (gout gout-stmt))
              (simpadd0-stmt item.stmt gin))
             (gin (gin-update gin gout-stmt)))
          (xeq-block-item-stmt item.stmt new-stmt
                               gout-stmt.thm-name item.info gin))
        :ambig (prog2$ (impossible)
                       (mv (irr-block-item) (irr-gout)))))))

Function: simpadd0-block-item-list

(defun simpadd0-block-item-list (items gin)
 (declare (xargs :guard (and (block-item-listp items)
                             (ginp gin))))
 (declare (xargs :guard (and (block-item-list-unambp items)
                             (block-item-list-annop items))))
 (let ((__function__ 'simpadd0-block-item-list))
  (declare (ignorable __function__))
  (b* (((gin gin) gin)
       ((when (endp items))
        (mv nil (xeq-block-item-list-empty gin)))
       (item (car items))
       ((mv new-item (gout gout-item))
        (simpadd0-block-item item gin))
       (gin (gin-update gin gout-item))
       ((mv new-items (gout gout-items))
        (simpadd0-block-item-list
             (cdr items)
             (change-gin gin
                         :vartys gout-item.vartys)))
       (gin (gin-update gin gout-items)))
   (xeq-block-item-list-cons (car items)
                             new-item gout-item.thm-name (cdr items)
                             new-items gout-items.thm-name gin))))

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

(defthm return-type-of-simpadd0-expr.new-expr
  (b* (((mv ?new-expr ?gout)
        (simpadd0-expr expr gin)))
    (exprp new-expr))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-expr.gout

(defthm return-type-of-simpadd0-expr.gout
  (b* (((mv ?new-expr ?gout)
        (simpadd0-expr expr gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-expr-list.new-exprs
  (b* (((mv ?new-exprs ?gout)
        (simpadd0-expr-list exprs gin)))
    (expr-listp new-exprs))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-expr-list.gout

(defthm return-type-of-simpadd0-expr-list.gout
  (b* (((mv ?new-exprs ?gout)
        (simpadd0-expr-list exprs gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-expr-option.new-expr?
  (b* (((mv ?new-expr? ?gout)
        (simpadd0-expr-option expr? gin)))
    (expr-optionp new-expr?))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-expr-option.gout

(defthm return-type-of-simpadd0-expr-option.gout
  (b* (((mv ?new-expr? ?gout)
        (simpadd0-expr-option expr? gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-const-expr.new-cexpr
  (b* (((mv ?new-cexpr ?gout)
        (simpadd0-const-expr cexpr gin)))
    (const-exprp new-cexpr))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-const-expr.gout

(defthm return-type-of-simpadd0-const-expr.gout
  (b* (((mv ?new-cexpr ?gout)
        (simpadd0-const-expr cexpr gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-const-expr-option.new-cexpr?
  (b* (((mv ?new-cexpr? ?gout)
        (simpadd0-const-expr-option cexpr? gin)))
    (const-expr-optionp new-cexpr?))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-const-expr-option.gout

(defthm return-type-of-simpadd0-const-expr-option.gout
  (b* (((mv ?new-cexpr? ?gout)
        (simpadd0-const-expr-option cexpr? gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-genassoc.new-genassoc

(defthm return-type-of-simpadd0-genassoc.new-genassoc
  (b* (((mv ?new-genassoc ?gout)
        (simpadd0-genassoc genassoc gin)))
    (genassocp new-genassoc))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-genassoc.gout

(defthm return-type-of-simpadd0-genassoc.gout
  (b* (((mv ?new-genassoc ?gout)
        (simpadd0-genassoc genassoc gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-genassoc-list.new-genassocs

(defthm return-type-of-simpadd0-genassoc-list.new-genassocs
  (b* (((mv ?new-genassocs ?gout)
        (simpadd0-genassoc-list genassocs gin)))
    (genassoc-listp new-genassocs))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-genassoc-list.gout

(defthm return-type-of-simpadd0-genassoc-list.gout
  (b* (((mv ?new-genassocs ?gout)
        (simpadd0-genassoc-list genassocs gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-member-designor.new-memdes
  (b* (((mv ?new-memdes ?gout)
        (simpadd0-member-designor memdes gin)))
    (member-designorp new-memdes))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-member-designor.gout

(defthm return-type-of-simpadd0-member-designor.gout
  (b* (((mv ?new-memdes ?gout)
        (simpadd0-member-designor memdes gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-type-spec.new-tyspec
  (b* (((mv ?new-tyspec ?gout)
        (simpadd0-type-spec tyspec gin)))
    (type-specp new-tyspec))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-type-spec.gout

(defthm return-type-of-simpadd0-type-spec.gout
  (b* (((mv ?new-tyspec ?gout)
        (simpadd0-type-spec tyspec gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-spec/qual.new-specqual
  (b* (((mv ?new-specqual ?gout)
        (simpadd0-spec/qual specqual gin)))
    (spec/qual-p new-specqual))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-spec/qual.gout

(defthm return-type-of-simpadd0-spec/qual.gout
  (b* (((mv ?new-specqual ?gout)
        (simpadd0-spec/qual specqual gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-spec/qual-list.new-specquals
  (b* (((mv ?new-specquals ?gout)
        (simpadd0-spec/qual-list specquals gin)))
    (spec/qual-listp new-specquals))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-spec/qual-list.gout

(defthm return-type-of-simpadd0-spec/qual-list.gout
  (b* (((mv ?new-specquals ?gout)
        (simpadd0-spec/qual-list specquals gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-align-spec.new-alignspec
  (b* (((mv ?new-alignspec ?gout)
        (simpadd0-align-spec alignspec gin)))
    (align-specp new-alignspec))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-align-spec.gout

(defthm return-type-of-simpadd0-align-spec.gout
  (b* (((mv ?new-alignspec ?gout)
        (simpadd0-align-spec alignspec gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-decl-spec.new-declspec
  (b* (((mv ?new-declspec ?gout)
        (simpadd0-decl-spec declspec gin)))
    (decl-specp new-declspec))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-decl-spec.gout

(defthm return-type-of-simpadd0-decl-spec.gout
  (b* (((mv ?new-declspec ?gout)
        (simpadd0-decl-spec declspec gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-decl-spec-list.new-declspecs
  (b* (((mv ?new-declspecs ?gout)
        (simpadd0-decl-spec-list declspecs gin)))
    (decl-spec-listp new-declspecs))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-decl-spec-list.gout

(defthm return-type-of-simpadd0-decl-spec-list.gout
  (b* (((mv ?new-declspecs ?gout)
        (simpadd0-decl-spec-list declspecs gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-initer.new-initer
  (b* (((mv ?new-initer ?gout)
        (simpadd0-initer initer gin)))
    (initerp new-initer))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-initer.gout

(defthm return-type-of-simpadd0-initer.gout
  (b* (((mv ?new-initer ?gout)
        (simpadd0-initer initer gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-initer-option.new-initer?
  (b* (((mv ?new-initer? ?gout)
        (simpadd0-initer-option initer? gin)))
    (initer-optionp new-initer?))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-initer-option.gout

(defthm return-type-of-simpadd0-initer-option.gout
  (b* (((mv ?new-initer? ?gout)
        (simpadd0-initer-option initer? gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-desiniter.new-desiniter
  (b* (((mv ?new-desiniter ?gout)
        (simpadd0-desiniter desiniter gin)))
    (desiniterp new-desiniter))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-desiniter.gout

(defthm return-type-of-simpadd0-desiniter.gout
  (b* (((mv ?new-desiniter ?gout)
        (simpadd0-desiniter desiniter gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-desiniter-list.new-desiniters
  (b* (((mv ?new-desiniters ?gout)
        (simpadd0-desiniter-list desiniters gin)))
    (desiniter-listp new-desiniters))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-desiniter-list.gout

(defthm return-type-of-simpadd0-desiniter-list.gout
  (b* (((mv ?new-desiniters ?gout)
        (simpadd0-desiniter-list desiniters gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-designor.new-designor

(defthm return-type-of-simpadd0-designor.new-designor
  (b* (((mv ?new-designor ?gout)
        (simpadd0-designor designor gin)))
    (designorp new-designor))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-designor.gout

(defthm return-type-of-simpadd0-designor.gout
  (b* (((mv ?new-designor ?gout)
        (simpadd0-designor designor gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-designor-list.new-designors

(defthm return-type-of-simpadd0-designor-list.new-designors
  (b* (((mv ?new-designors ?gout)
        (simpadd0-designor-list designors gin)))
    (designor-listp new-designors))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-designor-list.gout

(defthm return-type-of-simpadd0-designor-list.gout
  (b* (((mv ?new-designors ?gout)
        (simpadd0-designor-list designors gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-declor.new-declor
  (b* (((mv ?new-declor ?new-fundefp ?gout)
        (simpadd0-declor declor fundefp gin)))
    (declorp new-declor))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-declor.new-fundefp

(defthm return-type-of-simpadd0-declor.new-fundefp
  (b* (((mv ?new-declor ?new-fundefp ?gout)
        (simpadd0-declor declor fundefp gin)))
    (booleanp new-fundefp))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-declor.gout

(defthm return-type-of-simpadd0-declor.gout
  (b* (((mv ?new-declor ?new-fundefp ?gout)
        (simpadd0-declor declor fundefp gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-declor-option.new-declor?
  (b* (((mv ?new-declor? ?gout)
        (simpadd0-declor-option declor? gin)))
    (declor-optionp new-declor?))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-declor-option.gout

(defthm return-type-of-simpadd0-declor-option.gout
  (b* (((mv ?new-declor? ?gout)
        (simpadd0-declor-option declor? gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-dirdeclor.new-dirdeclor
  (b* (((mv ?new-dirdeclor ?new-fundefp ?gout)
        (simpadd0-dirdeclor dirdeclor fundefp gin)))
    (dirdeclorp new-dirdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-dirdeclor.new-fundefp

(defthm return-type-of-simpadd0-dirdeclor.new-fundefp
  (b* (((mv ?new-dirdeclor ?new-fundefp ?gout)
        (simpadd0-dirdeclor dirdeclor fundefp gin)))
    (booleanp new-fundefp))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-dirdeclor.gout

(defthm return-type-of-simpadd0-dirdeclor.gout
  (b* (((mv ?new-dirdeclor ?new-fundefp ?gout)
        (simpadd0-dirdeclor dirdeclor fundefp gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-absdeclor.new-absdeclor
  (b* (((mv ?new-absdeclor ?gout)
        (simpadd0-absdeclor absdeclor gin)))
    (absdeclorp new-absdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-absdeclor.gout

(defthm return-type-of-simpadd0-absdeclor.gout
  (b* (((mv ?new-absdeclor ?gout)
        (simpadd0-absdeclor absdeclor gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-absdeclor-option.new-absdeclor?
  (b* (((mv ?new-absdeclor? ?gout)
        (simpadd0-absdeclor-option absdeclor? gin)))
    (absdeclor-optionp new-absdeclor?))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-absdeclor-option.gout

(defthm return-type-of-simpadd0-absdeclor-option.gout
  (b* (((mv ?new-absdeclor? ?gout)
        (simpadd0-absdeclor-option absdeclor? gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-dirabsdeclor.new-dirabsdeclor
  (b* (((mv ?new-dirabsdeclor ?gout)
        (simpadd0-dirabsdeclor dirabsdeclor gin)))
    (dirabsdeclorp new-dirabsdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-dirabsdeclor.gout

(defthm return-type-of-simpadd0-dirabsdeclor.gout
  (b* (((mv ?new-dirabsdeclor ?gout)
        (simpadd0-dirabsdeclor dirabsdeclor gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm
      return-type-of-simpadd0-dirabsdeclor-option.new-dirabsdeclor?
  (b* (((mv ?new-dirabsdeclor? ?gout)
        (simpadd0-dirabsdeclor-option dirabsdeclor? gin)))
    (dirabsdeclor-optionp new-dirabsdeclor?))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-dirabsdeclor-option.gout

(defthm return-type-of-simpadd0-dirabsdeclor-option.gout
  (b* (((mv ?new-dirabsdeclor? ?gout)
        (simpadd0-dirabsdeclor-option dirabsdeclor? gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-param-declon.new-paramdeclon

(defthm return-type-of-simpadd0-param-declon.new-paramdeclon
  (b* (((mv ?new-paramdeclon ?gout)
        (simpadd0-param-declon paramdeclon gin)))
    (param-declonp new-paramdeclon))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-param-declon.gout

(defthm return-type-of-simpadd0-param-declon.gout
  (b* (((mv ?new-paramdeclon ?gout)
        (simpadd0-param-declon paramdeclon gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-param-declon-list.new-paramdeclons

(defthm return-type-of-simpadd0-param-declon-list.new-paramdeclons
  (b* (((mv ?new-paramdeclons ?gout)
        (simpadd0-param-declon-list paramdeclons gin)))
    (param-declon-listp new-paramdeclons))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-param-declon-list.gout

(defthm return-type-of-simpadd0-param-declon-list.gout
  (b* (((mv ?new-paramdeclons ?gout)
        (simpadd0-param-declon-list paramdeclons gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-param-declor.new-paramdeclor
  (b* (((mv ?new-paramdeclor ?gout)
        (simpadd0-param-declor paramdeclor gin)))
    (param-declorp new-paramdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-param-declor.gout

(defthm return-type-of-simpadd0-param-declor.gout
  (b* (((mv ?new-paramdeclor ?gout)
        (simpadd0-param-declor paramdeclor gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-tyname.new-tyname
  (b* (((mv ?new-tyname ?gout)
        (simpadd0-tyname tyname gin)))
    (tynamep new-tyname))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-tyname.gout

(defthm return-type-of-simpadd0-tyname.gout
  (b* (((mv ?new-tyname ?gout)
        (simpadd0-tyname tyname gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-struni-spec.new-struni-spec
  (b* (((mv ?new-struni-spec ?gout)
        (simpadd0-struni-spec struni-spec gin)))
    (struni-specp new-struni-spec))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-struni-spec.gout

(defthm return-type-of-simpadd0-struni-spec.gout
  (b* (((mv ?new-struni-spec ?gout)
        (simpadd0-struni-spec struni-spec gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-struct-declon.new-structdeclon
  (b* (((mv ?new-structdeclon ?gout)
        (simpadd0-struct-declon structdeclon gin)))
    (struct-declonp new-structdeclon))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-struct-declon.gout

(defthm return-type-of-simpadd0-struct-declon.gout
  (b* (((mv ?new-structdeclon ?gout)
        (simpadd0-struct-declon structdeclon gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-struct-declon-list.new-structdeclons
  (b* (((mv ?new-structdeclons ?gout)
        (simpadd0-struct-declon-list structdeclons gin)))
    (struct-declon-listp new-structdeclons))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-struct-declon-list.gout

(defthm return-type-of-simpadd0-struct-declon-list.gout
  (b* (((mv ?new-structdeclons ?gout)
        (simpadd0-struct-declon-list structdeclons gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-struct-declor.new-structdeclor
  (b* (((mv ?new-structdeclor ?gout)
        (simpadd0-struct-declor structdeclor gin)))
    (struct-declorp new-structdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-struct-declor.gout

(defthm return-type-of-simpadd0-struct-declor.gout
  (b* (((mv ?new-structdeclor ?gout)
        (simpadd0-struct-declor structdeclor gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-struct-declor-list.new-structdeclors
  (b* (((mv ?new-structdeclors ?gout)
        (simpadd0-struct-declor-list structdeclors gin)))
    (struct-declor-listp new-structdeclors))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-struct-declor-list.gout

(defthm return-type-of-simpadd0-struct-declor-list.gout
  (b* (((mv ?new-structdeclors ?gout)
        (simpadd0-struct-declor-list structdeclors gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-enum-spec.new-enumspec
  (b* (((mv ?new-enumspec ?gout)
        (simpadd0-enum-spec enumspec gin)))
    (enum-specp new-enumspec))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-enum-spec.gout

(defthm return-type-of-simpadd0-enum-spec.gout
  (b* (((mv ?new-enumspec ?gout)
        (simpadd0-enum-spec enumspec gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-enumer.new-enumer
  (b* (((mv ?new-enumer ?gout)
        (simpadd0-enumer enumer gin)))
    (enumerp new-enumer))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-enumer.gout

(defthm return-type-of-simpadd0-enumer.gout
  (b* (((mv ?new-enumer ?gout)
        (simpadd0-enumer enumer gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-enumer-list.new-enumers
  (b* (((mv ?new-enumers ?gout)
        (simpadd0-enumer-list enumers gin)))
    (enumer-listp new-enumers))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-enumer-list.gout

(defthm return-type-of-simpadd0-enumer-list.gout
  (b* (((mv ?new-enumers ?gout)
        (simpadd0-enumer-list enumers gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-statassert.new-statassert
  (b* (((mv ?new-statassert ?gout)
        (simpadd0-statassert statassert gin)))
    (statassertp new-statassert))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-statassert.gout

(defthm return-type-of-simpadd0-statassert.gout
  (b* (((mv ?new-statassert ?gout)
        (simpadd0-statassert statassert gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-initdeclor.new-initdeclor

(defthm return-type-of-simpadd0-initdeclor.new-initdeclor
  (b* (((mv ?new-initdeclor ?gout)
        (simpadd0-initdeclor initdeclor gin)))
    (initdeclorp new-initdeclor))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-initdeclor.gout

(defthm return-type-of-simpadd0-initdeclor.gout
  (b* (((mv ?new-initdeclor ?gout)
        (simpadd0-initdeclor initdeclor gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-initdeclor-list.new-initdeclors

(defthm return-type-of-simpadd0-initdeclor-list.new-initdeclors
  (b* (((mv ?new-initdeclors ?gout)
        (simpadd0-initdeclor-list initdeclors gin)))
    (initdeclor-listp new-initdeclors))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-initdeclor-list.gout

(defthm return-type-of-simpadd0-initdeclor-list.gout
  (b* (((mv ?new-initdeclors ?gout)
        (simpadd0-initdeclor-list initdeclors gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-decl.new-decl
  (b* (((mv ?new-decl ?gout)
        (simpadd0-decl decl gin)))
    (declp new-decl))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-decl.gout

(defthm return-type-of-simpadd0-decl.gout
  (b* (((mv ?new-decl ?gout)
        (simpadd0-decl decl gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-decl-list.new-decls
  (b* (((mv ?new-decls ?gout)
        (simpadd0-decl-list decls gin)))
    (decl-listp new-decls))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-decl-list.gout

(defthm return-type-of-simpadd0-decl-list.gout
  (b* (((mv ?new-decls ?gout)
        (simpadd0-decl-list decls gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-label.new-label
  (b* (((mv ?new-label ?gout)
        (simpadd0-label label gin)))
    (labelp new-label))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-label.gout

(defthm return-type-of-simpadd0-label.gout
  (b* (((mv ?new-label ?gout)
        (simpadd0-label label gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-stmt.new-stmt
  (b* (((mv ?new-stmt ?gout)
        (simpadd0-stmt stmt gin)))
    (stmtp new-stmt))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-stmt.gout

(defthm return-type-of-simpadd0-stmt.gout
  (b* (((mv ?new-stmt ?gout)
        (simpadd0-stmt stmt gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-comp-stmt.new-cstmt
  (b* (((mv ?new-cstmt ?gout)
        (simpadd0-comp-stmt cstmt gin)))
    (comp-stmtp new-cstmt))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-comp-stmt.gout

(defthm return-type-of-simpadd0-comp-stmt.gout
  (b* (((mv ?new-cstmt ?gout)
        (simpadd0-comp-stmt cstmt gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-block-item.new-item
  (b* (((mv ?new-item ?gout)
        (simpadd0-block-item item gin)))
    (block-itemp new-item))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-block-item.gout

(defthm return-type-of-simpadd0-block-item.gout
  (b* (((mv ?new-item ?gout)
        (simpadd0-block-item item gin)))
    (goutp gout))
  :rule-classes :rewrite)

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

(defthm return-type-of-simpadd0-block-item-list.new-items
  (b* (((mv ?new-items ?gout)
        (simpadd0-block-item-list items gin)))
    (block-item-listp new-items))
  :rule-classes :rewrite)

Theorem: return-type-of-simpadd0-block-item-list.gout

(defthm return-type-of-simpadd0-block-item-list.gout
  (b* (((mv ?new-items ?gout)
        (simpadd0-block-item-list items gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: simpadd0-expr-option-iff-expr-option

(defthm simpadd0-expr-option-iff-expr-option
  (b* (((mv ?new-expr? ?gout)
        (simpadd0-expr-option expr? gin)))
    (iff new-expr? expr?)))

Theorem: simpadd0-expr-of-expr-fix-expr

(defthm simpadd0-expr-of-expr-fix-expr
  (equal (simpadd0-expr (expr-fix expr) gin)
         (simpadd0-expr expr gin)))

Theorem: simpadd0-expr-of-gin-fix-gin

(defthm simpadd0-expr-of-gin-fix-gin
  (equal (simpadd0-expr expr (gin-fix gin))
         (simpadd0-expr expr gin)))

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

(defthm simpadd0-expr-list-of-expr-list-fix-exprs
  (equal (simpadd0-expr-list (expr-list-fix exprs)
                             gin)
         (simpadd0-expr-list exprs gin)))

Theorem: simpadd0-expr-list-of-gin-fix-gin

(defthm simpadd0-expr-list-of-gin-fix-gin
  (equal (simpadd0-expr-list exprs (gin-fix gin))
         (simpadd0-expr-list exprs gin)))

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

(defthm simpadd0-expr-option-of-expr-option-fix-expr?
  (equal (simpadd0-expr-option (expr-option-fix expr?)
                               gin)
         (simpadd0-expr-option expr? gin)))

Theorem: simpadd0-expr-option-of-gin-fix-gin

(defthm simpadd0-expr-option-of-gin-fix-gin
  (equal (simpadd0-expr-option expr? (gin-fix gin))
         (simpadd0-expr-option expr? gin)))

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

(defthm simpadd0-const-expr-of-const-expr-fix-cexpr
  (equal (simpadd0-const-expr (c$::const-expr-fix cexpr)
                              gin)
         (simpadd0-const-expr cexpr gin)))

Theorem: simpadd0-const-expr-of-gin-fix-gin

(defthm simpadd0-const-expr-of-gin-fix-gin
  (equal (simpadd0-const-expr cexpr (gin-fix gin))
         (simpadd0-const-expr cexpr gin)))

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

(defthm simpadd0-const-expr-option-of-const-expr-option-fix-cexpr?
  (equal (simpadd0-const-expr-option (const-expr-option-fix cexpr?)
                                     gin)
         (simpadd0-const-expr-option cexpr? gin)))

Theorem: simpadd0-const-expr-option-of-gin-fix-gin

(defthm simpadd0-const-expr-option-of-gin-fix-gin
  (equal (simpadd0-const-expr-option cexpr? (gin-fix gin))
         (simpadd0-const-expr-option cexpr? gin)))

Theorem: simpadd0-genassoc-of-genassoc-fix-genassoc

(defthm simpadd0-genassoc-of-genassoc-fix-genassoc
  (equal (simpadd0-genassoc (genassoc-fix genassoc)
                            gin)
         (simpadd0-genassoc genassoc gin)))

Theorem: simpadd0-genassoc-of-gin-fix-gin

(defthm simpadd0-genassoc-of-gin-fix-gin
  (equal (simpadd0-genassoc genassoc (gin-fix gin))
         (simpadd0-genassoc genassoc gin)))

Theorem: simpadd0-genassoc-list-of-genassoc-list-fix-genassocs

(defthm simpadd0-genassoc-list-of-genassoc-list-fix-genassocs
  (equal (simpadd0-genassoc-list (genassoc-list-fix genassocs)
                                 gin)
         (simpadd0-genassoc-list genassocs gin)))

Theorem: simpadd0-genassoc-list-of-gin-fix-gin

(defthm simpadd0-genassoc-list-of-gin-fix-gin
  (equal (simpadd0-genassoc-list genassocs (gin-fix gin))
         (simpadd0-genassoc-list genassocs gin)))

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

(defthm simpadd0-member-designor-of-member-designor-fix-memdes
  (equal (simpadd0-member-designor (member-designor-fix memdes)
                                   gin)
         (simpadd0-member-designor memdes gin)))

Theorem: simpadd0-member-designor-of-gin-fix-gin

(defthm simpadd0-member-designor-of-gin-fix-gin
  (equal (simpadd0-member-designor memdes (gin-fix gin))
         (simpadd0-member-designor memdes gin)))

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

(defthm simpadd0-type-spec-of-type-spec-fix-tyspec
  (equal (simpadd0-type-spec (type-spec-fix tyspec)
                             gin)
         (simpadd0-type-spec tyspec gin)))

Theorem: simpadd0-type-spec-of-gin-fix-gin

(defthm simpadd0-type-spec-of-gin-fix-gin
  (equal (simpadd0-type-spec tyspec (gin-fix gin))
         (simpadd0-type-spec tyspec gin)))

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

(defthm simpadd0-spec/qual-of-spec/qual-fix-specqual
  (equal (simpadd0-spec/qual (spec/qual-fix specqual)
                             gin)
         (simpadd0-spec/qual specqual gin)))

Theorem: simpadd0-spec/qual-of-gin-fix-gin

(defthm simpadd0-spec/qual-of-gin-fix-gin
  (equal (simpadd0-spec/qual specqual (gin-fix gin))
         (simpadd0-spec/qual specqual gin)))

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

(defthm simpadd0-spec/qual-list-of-spec/qual-list-fix-specquals
  (equal (simpadd0-spec/qual-list (spec/qual-list-fix specquals)
                                  gin)
         (simpadd0-spec/qual-list specquals gin)))

Theorem: simpadd0-spec/qual-list-of-gin-fix-gin

(defthm simpadd0-spec/qual-list-of-gin-fix-gin
  (equal (simpadd0-spec/qual-list specquals (gin-fix gin))
         (simpadd0-spec/qual-list specquals gin)))

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

(defthm simpadd0-align-spec-of-align-spec-fix-alignspec
  (equal (simpadd0-align-spec (align-spec-fix alignspec)
                              gin)
         (simpadd0-align-spec alignspec gin)))

Theorem: simpadd0-align-spec-of-gin-fix-gin

(defthm simpadd0-align-spec-of-gin-fix-gin
  (equal (simpadd0-align-spec alignspec (gin-fix gin))
         (simpadd0-align-spec alignspec gin)))

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

(defthm simpadd0-decl-spec-of-decl-spec-fix-declspec
  (equal (simpadd0-decl-spec (decl-spec-fix declspec)
                             gin)
         (simpadd0-decl-spec declspec gin)))

Theorem: simpadd0-decl-spec-of-gin-fix-gin

(defthm simpadd0-decl-spec-of-gin-fix-gin
  (equal (simpadd0-decl-spec declspec (gin-fix gin))
         (simpadd0-decl-spec declspec gin)))

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

(defthm simpadd0-decl-spec-list-of-decl-spec-list-fix-declspecs
  (equal (simpadd0-decl-spec-list (decl-spec-list-fix declspecs)
                                  gin)
         (simpadd0-decl-spec-list declspecs gin)))

Theorem: simpadd0-decl-spec-list-of-gin-fix-gin

(defthm simpadd0-decl-spec-list-of-gin-fix-gin
  (equal (simpadd0-decl-spec-list declspecs (gin-fix gin))
         (simpadd0-decl-spec-list declspecs gin)))

Theorem: simpadd0-initer-of-initer-fix-initer

(defthm simpadd0-initer-of-initer-fix-initer
  (equal (simpadd0-initer (initer-fix initer)
                          gin)
         (simpadd0-initer initer gin)))

Theorem: simpadd0-initer-of-gin-fix-gin

(defthm simpadd0-initer-of-gin-fix-gin
  (equal (simpadd0-initer initer (gin-fix gin))
         (simpadd0-initer initer gin)))

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

(defthm simpadd0-initer-option-of-initer-option-fix-initer?
  (equal (simpadd0-initer-option (initer-option-fix initer?)
                                 gin)
         (simpadd0-initer-option initer? gin)))

Theorem: simpadd0-initer-option-of-gin-fix-gin

(defthm simpadd0-initer-option-of-gin-fix-gin
  (equal (simpadd0-initer-option initer? (gin-fix gin))
         (simpadd0-initer-option initer? gin)))

Theorem: simpadd0-desiniter-of-desiniter-fix-desiniter

(defthm simpadd0-desiniter-of-desiniter-fix-desiniter
  (equal (simpadd0-desiniter (desiniter-fix desiniter)
                             gin)
         (simpadd0-desiniter desiniter gin)))

Theorem: simpadd0-desiniter-of-gin-fix-gin

(defthm simpadd0-desiniter-of-gin-fix-gin
  (equal (simpadd0-desiniter desiniter (gin-fix gin))
         (simpadd0-desiniter desiniter gin)))

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

(defthm simpadd0-desiniter-list-of-desiniter-list-fix-desiniters
  (equal (simpadd0-desiniter-list (desiniter-list-fix desiniters)
                                  gin)
         (simpadd0-desiniter-list desiniters gin)))

Theorem: simpadd0-desiniter-list-of-gin-fix-gin

(defthm simpadd0-desiniter-list-of-gin-fix-gin
  (equal (simpadd0-desiniter-list desiniters (gin-fix gin))
         (simpadd0-desiniter-list desiniters gin)))

Theorem: simpadd0-designor-of-designor-fix-designor

(defthm simpadd0-designor-of-designor-fix-designor
  (equal (simpadd0-designor (designor-fix designor)
                            gin)
         (simpadd0-designor designor gin)))

Theorem: simpadd0-designor-of-gin-fix-gin

(defthm simpadd0-designor-of-gin-fix-gin
  (equal (simpadd0-designor designor (gin-fix gin))
         (simpadd0-designor designor gin)))

Theorem: simpadd0-designor-list-of-designor-list-fix-designors

(defthm simpadd0-designor-list-of-designor-list-fix-designors
  (equal (simpadd0-designor-list (designor-list-fix designors)
                                 gin)
         (simpadd0-designor-list designors gin)))

Theorem: simpadd0-designor-list-of-gin-fix-gin

(defthm simpadd0-designor-list-of-gin-fix-gin
  (equal (simpadd0-designor-list designors (gin-fix gin))
         (simpadd0-designor-list designors gin)))

Theorem: simpadd0-declor-of-declor-fix-declor

(defthm simpadd0-declor-of-declor-fix-declor
  (equal (simpadd0-declor (declor-fix declor)
                          fundefp gin)
         (simpadd0-declor declor fundefp gin)))

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

(defthm simpadd0-declor-of-bool-fix-fundefp
  (equal (simpadd0-declor declor (acl2::bool-fix fundefp)
                          gin)
         (simpadd0-declor declor fundefp gin)))

Theorem: simpadd0-declor-of-gin-fix-gin

(defthm simpadd0-declor-of-gin-fix-gin
  (equal (simpadd0-declor declor fundefp (gin-fix gin))
         (simpadd0-declor declor fundefp gin)))

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

(defthm simpadd0-declor-option-of-declor-option-fix-declor?
  (equal (simpadd0-declor-option (declor-option-fix declor?)
                                 gin)
         (simpadd0-declor-option declor? gin)))

Theorem: simpadd0-declor-option-of-gin-fix-gin

(defthm simpadd0-declor-option-of-gin-fix-gin
  (equal (simpadd0-declor-option declor? (gin-fix gin))
         (simpadd0-declor-option declor? gin)))

Theorem: simpadd0-dirdeclor-of-dirdeclor-fix-dirdeclor

(defthm simpadd0-dirdeclor-of-dirdeclor-fix-dirdeclor
  (equal (simpadd0-dirdeclor (dirdeclor-fix dirdeclor)
                             fundefp gin)
         (simpadd0-dirdeclor dirdeclor fundefp gin)))

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

(defthm simpadd0-dirdeclor-of-bool-fix-fundefp
  (equal (simpadd0-dirdeclor dirdeclor (acl2::bool-fix fundefp)
                             gin)
         (simpadd0-dirdeclor dirdeclor fundefp gin)))

Theorem: simpadd0-dirdeclor-of-gin-fix-gin

(defthm simpadd0-dirdeclor-of-gin-fix-gin
  (equal (simpadd0-dirdeclor dirdeclor fundefp (gin-fix gin))
         (simpadd0-dirdeclor dirdeclor fundefp gin)))

Theorem: simpadd0-absdeclor-of-absdeclor-fix-absdeclor

(defthm simpadd0-absdeclor-of-absdeclor-fix-absdeclor
  (equal (simpadd0-absdeclor (absdeclor-fix absdeclor)
                             gin)
         (simpadd0-absdeclor absdeclor gin)))

Theorem: simpadd0-absdeclor-of-gin-fix-gin

(defthm simpadd0-absdeclor-of-gin-fix-gin
  (equal (simpadd0-absdeclor absdeclor (gin-fix gin))
         (simpadd0-absdeclor absdeclor gin)))

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

(defthm simpadd0-absdeclor-option-of-absdeclor-option-fix-absdeclor?
 (equal (simpadd0-absdeclor-option (absdeclor-option-fix absdeclor?)
                                   gin)
        (simpadd0-absdeclor-option absdeclor? gin)))

Theorem: simpadd0-absdeclor-option-of-gin-fix-gin

(defthm simpadd0-absdeclor-option-of-gin-fix-gin
  (equal (simpadd0-absdeclor-option absdeclor? (gin-fix gin))
         (simpadd0-absdeclor-option absdeclor? gin)))

Theorem: simpadd0-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor

(defthm simpadd0-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor
  (equal (simpadd0-dirabsdeclor (dirabsdeclor-fix dirabsdeclor)
                                gin)
         (simpadd0-dirabsdeclor dirabsdeclor gin)))

Theorem: simpadd0-dirabsdeclor-of-gin-fix-gin

(defthm simpadd0-dirabsdeclor-of-gin-fix-gin
  (equal (simpadd0-dirabsdeclor dirabsdeclor (gin-fix gin))
         (simpadd0-dirabsdeclor dirabsdeclor gin)))

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

(defthm
 simpadd0-dirabsdeclor-option-of-dirabsdeclor-option-fix-dirabsdeclor?
 (equal (simpadd0-dirabsdeclor-option
             (dirabsdeclor-option-fix dirabsdeclor?)
             gin)
        (simpadd0-dirabsdeclor-option dirabsdeclor? gin)))

Theorem: simpadd0-dirabsdeclor-option-of-gin-fix-gin

(defthm simpadd0-dirabsdeclor-option-of-gin-fix-gin
  (equal (simpadd0-dirabsdeclor-option dirabsdeclor? (gin-fix gin))
         (simpadd0-dirabsdeclor-option dirabsdeclor? gin)))

Theorem: simpadd0-param-declon-of-param-declon-fix-paramdeclon

(defthm simpadd0-param-declon-of-param-declon-fix-paramdeclon
  (equal (simpadd0-param-declon (param-declon-fix paramdeclon)
                                gin)
         (simpadd0-param-declon paramdeclon gin)))

Theorem: simpadd0-param-declon-of-gin-fix-gin

(defthm simpadd0-param-declon-of-gin-fix-gin
  (equal (simpadd0-param-declon paramdeclon (gin-fix gin))
         (simpadd0-param-declon paramdeclon gin)))

Theorem: simpadd0-param-declon-list-of-param-declon-list-fix-paramdeclons

(defthm
   simpadd0-param-declon-list-of-param-declon-list-fix-paramdeclons
 (equal
    (simpadd0-param-declon-list (param-declon-list-fix paramdeclons)
                                gin)
    (simpadd0-param-declon-list paramdeclons gin)))

Theorem: simpadd0-param-declon-list-of-gin-fix-gin

(defthm simpadd0-param-declon-list-of-gin-fix-gin
  (equal (simpadd0-param-declon-list paramdeclons (gin-fix gin))
         (simpadd0-param-declon-list paramdeclons gin)))

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

(defthm simpadd0-param-declor-of-param-declor-fix-paramdeclor
  (equal (simpadd0-param-declor (param-declor-fix paramdeclor)
                                gin)
         (simpadd0-param-declor paramdeclor gin)))

Theorem: simpadd0-param-declor-of-gin-fix-gin

(defthm simpadd0-param-declor-of-gin-fix-gin
  (equal (simpadd0-param-declor paramdeclor (gin-fix gin))
         (simpadd0-param-declor paramdeclor gin)))

Theorem: simpadd0-tyname-of-tyname-fix-tyname

(defthm simpadd0-tyname-of-tyname-fix-tyname
  (equal (simpadd0-tyname (tyname-fix tyname)
                          gin)
         (simpadd0-tyname tyname gin)))

Theorem: simpadd0-tyname-of-gin-fix-gin

(defthm simpadd0-tyname-of-gin-fix-gin
  (equal (simpadd0-tyname tyname (gin-fix gin))
         (simpadd0-tyname tyname gin)))

Theorem: simpadd0-struni-spec-of-struni-spec-fix-struni-spec

(defthm simpadd0-struni-spec-of-struni-spec-fix-struni-spec
  (equal (simpadd0-struni-spec (struni-spec-fix struni-spec)
                               gin)
         (simpadd0-struni-spec struni-spec gin)))

Theorem: simpadd0-struni-spec-of-gin-fix-gin

(defthm simpadd0-struni-spec-of-gin-fix-gin
  (equal (simpadd0-struni-spec struni-spec (gin-fix gin))
         (simpadd0-struni-spec struni-spec gin)))

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

(defthm simpadd0-struct-declon-of-struct-declon-fix-structdeclon
  (equal (simpadd0-struct-declon (struct-declon-fix structdeclon)
                                 gin)
         (simpadd0-struct-declon structdeclon gin)))

Theorem: simpadd0-struct-declon-of-gin-fix-gin

(defthm simpadd0-struct-declon-of-gin-fix-gin
  (equal (simpadd0-struct-declon structdeclon (gin-fix gin))
         (simpadd0-struct-declon structdeclon gin)))

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

(defthm
 simpadd0-struct-declon-list-of-struct-declon-list-fix-structdeclons
 (equal (simpadd0-struct-declon-list
             (struct-declon-list-fix structdeclons)
             gin)
        (simpadd0-struct-declon-list structdeclons gin)))

Theorem: simpadd0-struct-declon-list-of-gin-fix-gin

(defthm simpadd0-struct-declon-list-of-gin-fix-gin
  (equal (simpadd0-struct-declon-list structdeclons (gin-fix gin))
         (simpadd0-struct-declon-list structdeclons gin)))

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

(defthm simpadd0-struct-declor-of-struct-declor-fix-structdeclor
  (equal (simpadd0-struct-declor (struct-declor-fix structdeclor)
                                 gin)
         (simpadd0-struct-declor structdeclor gin)))

Theorem: simpadd0-struct-declor-of-gin-fix-gin

(defthm simpadd0-struct-declor-of-gin-fix-gin
  (equal (simpadd0-struct-declor structdeclor (gin-fix gin))
         (simpadd0-struct-declor structdeclor gin)))

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

(defthm
 simpadd0-struct-declor-list-of-struct-declor-list-fix-structdeclors
 (equal (simpadd0-struct-declor-list
             (struct-declor-list-fix structdeclors)
             gin)
        (simpadd0-struct-declor-list structdeclors gin)))

Theorem: simpadd0-struct-declor-list-of-gin-fix-gin

(defthm simpadd0-struct-declor-list-of-gin-fix-gin
  (equal (simpadd0-struct-declor-list structdeclors (gin-fix gin))
         (simpadd0-struct-declor-list structdeclors gin)))

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

(defthm simpadd0-enum-spec-of-enum-spec-fix-enumspec
  (equal (simpadd0-enum-spec (enum-spec-fix enumspec)
                             gin)
         (simpadd0-enum-spec enumspec gin)))

Theorem: simpadd0-enum-spec-of-gin-fix-gin

(defthm simpadd0-enum-spec-of-gin-fix-gin
  (equal (simpadd0-enum-spec enumspec (gin-fix gin))
         (simpadd0-enum-spec enumspec gin)))

Theorem: simpadd0-enumer-of-enumer-fix-enumer

(defthm simpadd0-enumer-of-enumer-fix-enumer
  (equal (simpadd0-enumer (enumer-fix enumer)
                          gin)
         (simpadd0-enumer enumer gin)))

Theorem: simpadd0-enumer-of-gin-fix-gin

(defthm simpadd0-enumer-of-gin-fix-gin
  (equal (simpadd0-enumer enumer (gin-fix gin))
         (simpadd0-enumer enumer gin)))

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

(defthm simpadd0-enumer-list-of-enumer-list-fix-enumers
  (equal (simpadd0-enumer-list (enumer-list-fix enumers)
                               gin)
         (simpadd0-enumer-list enumers gin)))

Theorem: simpadd0-enumer-list-of-gin-fix-gin

(defthm simpadd0-enumer-list-of-gin-fix-gin
  (equal (simpadd0-enumer-list enumers (gin-fix gin))
         (simpadd0-enumer-list enumers gin)))

Theorem: simpadd0-statassert-of-statassert-fix-statassert

(defthm simpadd0-statassert-of-statassert-fix-statassert
  (equal (simpadd0-statassert (statassert-fix statassert)
                              gin)
         (simpadd0-statassert statassert gin)))

Theorem: simpadd0-statassert-of-gin-fix-gin

(defthm simpadd0-statassert-of-gin-fix-gin
  (equal (simpadd0-statassert statassert (gin-fix gin))
         (simpadd0-statassert statassert gin)))

Theorem: simpadd0-initdeclor-of-initdeclor-fix-initdeclor

(defthm simpadd0-initdeclor-of-initdeclor-fix-initdeclor
  (equal (simpadd0-initdeclor (initdeclor-fix initdeclor)
                              gin)
         (simpadd0-initdeclor initdeclor gin)))

Theorem: simpadd0-initdeclor-of-gin-fix-gin

(defthm simpadd0-initdeclor-of-gin-fix-gin
  (equal (simpadd0-initdeclor initdeclor (gin-fix gin))
         (simpadd0-initdeclor initdeclor gin)))

Theorem: simpadd0-initdeclor-list-of-initdeclor-list-fix-initdeclors

(defthm simpadd0-initdeclor-list-of-initdeclor-list-fix-initdeclors
  (equal (simpadd0-initdeclor-list (initdeclor-list-fix initdeclors)
                                   gin)
         (simpadd0-initdeclor-list initdeclors gin)))

Theorem: simpadd0-initdeclor-list-of-gin-fix-gin

(defthm simpadd0-initdeclor-list-of-gin-fix-gin
  (equal (simpadd0-initdeclor-list initdeclors (gin-fix gin))
         (simpadd0-initdeclor-list initdeclors gin)))

Theorem: simpadd0-decl-of-decl-fix-decl

(defthm simpadd0-decl-of-decl-fix-decl
  (equal (simpadd0-decl (decl-fix decl) gin)
         (simpadd0-decl decl gin)))

Theorem: simpadd0-decl-of-gin-fix-gin

(defthm simpadd0-decl-of-gin-fix-gin
  (equal (simpadd0-decl decl (gin-fix gin))
         (simpadd0-decl decl gin)))

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

(defthm simpadd0-decl-list-of-decl-list-fix-decls
  (equal (simpadd0-decl-list (c$::decl-list-fix decls)
                             gin)
         (simpadd0-decl-list decls gin)))

Theorem: simpadd0-decl-list-of-gin-fix-gin

(defthm simpadd0-decl-list-of-gin-fix-gin
  (equal (simpadd0-decl-list decls (gin-fix gin))
         (simpadd0-decl-list decls gin)))

Theorem: simpadd0-label-of-label-fix-label

(defthm simpadd0-label-of-label-fix-label
  (equal (simpadd0-label (label-fix label) gin)
         (simpadd0-label label gin)))

Theorem: simpadd0-label-of-gin-fix-gin

(defthm simpadd0-label-of-gin-fix-gin
  (equal (simpadd0-label label (gin-fix gin))
         (simpadd0-label label gin)))

Theorem: simpadd0-stmt-of-stmt-fix-stmt

(defthm simpadd0-stmt-of-stmt-fix-stmt
  (equal (simpadd0-stmt (stmt-fix stmt) gin)
         (simpadd0-stmt stmt gin)))

Theorem: simpadd0-stmt-of-gin-fix-gin

(defthm simpadd0-stmt-of-gin-fix-gin
  (equal (simpadd0-stmt stmt (gin-fix gin))
         (simpadd0-stmt stmt gin)))

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

(defthm simpadd0-comp-stmt-of-comp-stmt-fix-cstmt
  (equal (simpadd0-comp-stmt (c$::comp-stmt-fix cstmt)
                             gin)
         (simpadd0-comp-stmt cstmt gin)))

Theorem: simpadd0-comp-stmt-of-gin-fix-gin

(defthm simpadd0-comp-stmt-of-gin-fix-gin
  (equal (simpadd0-comp-stmt cstmt (gin-fix gin))
         (simpadd0-comp-stmt cstmt gin)))

Theorem: simpadd0-block-item-of-block-item-fix-item

(defthm simpadd0-block-item-of-block-item-fix-item
  (equal (simpadd0-block-item (block-item-fix item)
                              gin)
         (simpadd0-block-item item gin)))

Theorem: simpadd0-block-item-of-gin-fix-gin

(defthm simpadd0-block-item-of-gin-fix-gin
  (equal (simpadd0-block-item item (gin-fix gin))
         (simpadd0-block-item item gin)))

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

(defthm simpadd0-block-item-list-of-block-item-list-fix-items
  (equal (simpadd0-block-item-list (block-item-list-fix items)
                                   gin)
         (simpadd0-block-item-list items gin)))

Theorem: simpadd0-block-item-list-of-gin-fix-gin

(defthm simpadd0-block-item-list-of-gin-fix-gin
  (equal (simpadd0-block-item-list items (gin-fix gin))
         (simpadd0-block-item-list items gin)))

Theorem: simpadd0-expr-expr-equiv-congruence-on-expr

(defthm simpadd0-expr-expr-equiv-congruence-on-expr
  (implies (c$::expr-equiv expr expr-equiv)
           (equal (simpadd0-expr expr gin)
                  (simpadd0-expr expr-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-expr-gin-equiv-congruence-on-gin

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

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

(defthm simpadd0-expr-list-expr-list-equiv-congruence-on-exprs
  (implies (c$::expr-list-equiv exprs exprs-equiv)
           (equal (simpadd0-expr-list exprs gin)
                  (simpadd0-expr-list exprs-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-expr-list-gin-equiv-congruence-on-gin

(defthm simpadd0-expr-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-expr-list exprs gin)
                  (simpadd0-expr-list exprs gin-equiv)))
  :rule-classes :congruence)

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

(defthm simpadd0-expr-option-expr-option-equiv-congruence-on-expr?
  (implies (c$::expr-option-equiv expr? expr?-equiv)
           (equal (simpadd0-expr-option expr? gin)
                  (simpadd0-expr-option expr?-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-expr-option-gin-equiv-congruence-on-gin

(defthm simpadd0-expr-option-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-expr-option expr? gin)
                  (simpadd0-expr-option expr? gin-equiv)))
  :rule-classes :congruence)

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

(defthm simpadd0-const-expr-const-expr-equiv-congruence-on-cexpr
  (implies (c$::const-expr-equiv cexpr cexpr-equiv)
           (equal (simpadd0-const-expr cexpr gin)
                  (simpadd0-const-expr cexpr-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-const-expr-gin-equiv-congruence-on-gin

(defthm simpadd0-const-expr-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-const-expr cexpr gin)
                  (simpadd0-const-expr cexpr gin-equiv)))
  :rule-classes :congruence)

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

(defthm
 simpadd0-const-expr-option-const-expr-option-equiv-congruence-on-cexpr?
 (implies (c$::const-expr-option-equiv cexpr? cexpr?-equiv)
          (equal (simpadd0-const-expr-option cexpr? gin)
                 (simpadd0-const-expr-option cexpr?-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-const-expr-option-gin-equiv-congruence-on-gin

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

Theorem: simpadd0-genassoc-genassoc-equiv-congruence-on-genassoc

(defthm simpadd0-genassoc-genassoc-equiv-congruence-on-genassoc
  (implies (c$::genassoc-equiv genassoc genassoc-equiv)
           (equal (simpadd0-genassoc genassoc gin)
                  (simpadd0-genassoc genassoc-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-genassoc-gin-equiv-congruence-on-gin

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

Theorem: simpadd0-genassoc-list-genassoc-list-equiv-congruence-on-genassocs

(defthm
 simpadd0-genassoc-list-genassoc-list-equiv-congruence-on-genassocs
 (implies (c$::genassoc-list-equiv genassocs genassocs-equiv)
          (equal (simpadd0-genassoc-list genassocs gin)
                 (simpadd0-genassoc-list genassocs-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-genassoc-list-gin-equiv-congruence-on-gin

(defthm simpadd0-genassoc-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-genassoc-list genassocs gin)
                  (simpadd0-genassoc-list genassocs gin-equiv)))
  :rule-classes :congruence)

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

(defthm
 simpadd0-member-designor-member-designor-equiv-congruence-on-memdes
 (implies (c$::member-designor-equiv memdes memdes-equiv)
          (equal (simpadd0-member-designor memdes gin)
                 (simpadd0-member-designor memdes-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-member-designor-gin-equiv-congruence-on-gin

(defthm simpadd0-member-designor-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-member-designor memdes gin)
                  (simpadd0-member-designor memdes gin-equiv)))
  :rule-classes :congruence)

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

(defthm simpadd0-type-spec-type-spec-equiv-congruence-on-tyspec
  (implies (c$::type-spec-equiv tyspec tyspec-equiv)
           (equal (simpadd0-type-spec tyspec gin)
                  (simpadd0-type-spec tyspec-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-type-spec-gin-equiv-congruence-on-gin

(defthm simpadd0-type-spec-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-type-spec tyspec gin)
                  (simpadd0-type-spec tyspec gin-equiv)))
  :rule-classes :congruence)

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

(defthm simpadd0-spec/qual-spec/qual-equiv-congruence-on-specqual
  (implies (c$::spec/qual-equiv specqual specqual-equiv)
           (equal (simpadd0-spec/qual specqual gin)
                  (simpadd0-spec/qual specqual-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-spec/qual-gin-equiv-congruence-on-gin

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

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

(defthm
 simpadd0-spec/qual-list-spec/qual-list-equiv-congruence-on-specquals
 (implies (c$::spec/qual-list-equiv specquals specquals-equiv)
          (equal (simpadd0-spec/qual-list specquals gin)
                 (simpadd0-spec/qual-list specquals-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-spec/qual-list-gin-equiv-congruence-on-gin

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

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

(defthm simpadd0-align-spec-align-spec-equiv-congruence-on-alignspec
  (implies (c$::align-spec-equiv alignspec alignspec-equiv)
           (equal (simpadd0-align-spec alignspec gin)
                  (simpadd0-align-spec alignspec-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-align-spec-gin-equiv-congruence-on-gin

(defthm simpadd0-align-spec-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-align-spec alignspec gin)
                  (simpadd0-align-spec alignspec gin-equiv)))
  :rule-classes :congruence)

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

(defthm simpadd0-decl-spec-decl-spec-equiv-congruence-on-declspec
  (implies (c$::decl-spec-equiv declspec declspec-equiv)
           (equal (simpadd0-decl-spec declspec gin)
                  (simpadd0-decl-spec declspec-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-decl-spec-gin-equiv-congruence-on-gin

(defthm simpadd0-decl-spec-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-decl-spec declspec gin)
                  (simpadd0-decl-spec declspec gin-equiv)))
  :rule-classes :congruence)

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

(defthm
 simpadd0-decl-spec-list-decl-spec-list-equiv-congruence-on-declspecs
 (implies (c$::decl-spec-list-equiv declspecs declspecs-equiv)
          (equal (simpadd0-decl-spec-list declspecs gin)
                 (simpadd0-decl-spec-list declspecs-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-decl-spec-list-gin-equiv-congruence-on-gin

(defthm simpadd0-decl-spec-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-decl-spec-list declspecs gin)
                  (simpadd0-decl-spec-list declspecs gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-initer-initer-equiv-congruence-on-initer

(defthm simpadd0-initer-initer-equiv-congruence-on-initer
  (implies (c$::initer-equiv initer initer-equiv)
           (equal (simpadd0-initer initer gin)
                  (simpadd0-initer initer-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-initer-gin-equiv-congruence-on-gin

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

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

(defthm
   simpadd0-initer-option-initer-option-equiv-congruence-on-initer?
  (implies (c$::initer-option-equiv initer? initer?-equiv)
           (equal (simpadd0-initer-option initer? gin)
                  (simpadd0-initer-option initer?-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-initer-option-gin-equiv-congruence-on-gin

(defthm simpadd0-initer-option-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-initer-option initer? gin)
                  (simpadd0-initer-option initer? gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-desiniter-desiniter-equiv-congruence-on-desiniter

(defthm simpadd0-desiniter-desiniter-equiv-congruence-on-desiniter
  (implies (c$::desiniter-equiv desiniter desiniter-equiv)
           (equal (simpadd0-desiniter desiniter gin)
                  (simpadd0-desiniter desiniter-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-desiniter-gin-equiv-congruence-on-gin

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

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

(defthm
 simpadd0-desiniter-list-desiniter-list-equiv-congruence-on-desiniters
 (implies (c$::desiniter-list-equiv desiniters desiniters-equiv)
          (equal (simpadd0-desiniter-list desiniters gin)
                 (simpadd0-desiniter-list desiniters-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-desiniter-list-gin-equiv-congruence-on-gin

(defthm simpadd0-desiniter-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-desiniter-list desiniters gin)
                  (simpadd0-desiniter-list desiniters gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-designor-designor-equiv-congruence-on-designor

(defthm simpadd0-designor-designor-equiv-congruence-on-designor
  (implies (c$::designor-equiv designor designor-equiv)
           (equal (simpadd0-designor designor gin)
                  (simpadd0-designor designor-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-designor-gin-equiv-congruence-on-gin

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

Theorem: simpadd0-designor-list-designor-list-equiv-congruence-on-designors

(defthm
 simpadd0-designor-list-designor-list-equiv-congruence-on-designors
 (implies (c$::designor-list-equiv designors designors-equiv)
          (equal (simpadd0-designor-list designors gin)
                 (simpadd0-designor-list designors-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-designor-list-gin-equiv-congruence-on-gin

(defthm simpadd0-designor-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-designor-list designors gin)
                  (simpadd0-designor-list designors gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-declor-declor-equiv-congruence-on-declor

(defthm simpadd0-declor-declor-equiv-congruence-on-declor
  (implies (c$::declor-equiv declor declor-equiv)
           (equal (simpadd0-declor declor fundefp gin)
                  (simpadd0-declor declor-equiv fundefp gin)))
  :rule-classes :congruence)

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

(defthm simpadd0-declor-iff-congruence-on-fundefp
  (implies (iff fundefp fundefp-equiv)
           (equal (simpadd0-declor declor fundefp gin)
                  (simpadd0-declor declor fundefp-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-declor-gin-equiv-congruence-on-gin

(defthm simpadd0-declor-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-declor declor fundefp gin)
                  (simpadd0-declor declor fundefp gin-equiv)))
  :rule-classes :congruence)

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

(defthm
   simpadd0-declor-option-declor-option-equiv-congruence-on-declor?
  (implies (c$::declor-option-equiv declor? declor?-equiv)
           (equal (simpadd0-declor-option declor? gin)
                  (simpadd0-declor-option declor?-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-declor-option-gin-equiv-congruence-on-gin

(defthm simpadd0-declor-option-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-declor-option declor? gin)
                  (simpadd0-declor-option declor? gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor

(defthm simpadd0-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor
  (implies (c$::dirdeclor-equiv dirdeclor dirdeclor-equiv)
           (equal (simpadd0-dirdeclor dirdeclor fundefp gin)
                  (simpadd0-dirdeclor dirdeclor-equiv fundefp gin)))
  :rule-classes :congruence)

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

(defthm simpadd0-dirdeclor-iff-congruence-on-fundefp
  (implies (iff fundefp fundefp-equiv)
           (equal (simpadd0-dirdeclor dirdeclor fundefp gin)
                  (simpadd0-dirdeclor dirdeclor fundefp-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-dirdeclor-gin-equiv-congruence-on-gin

(defthm simpadd0-dirdeclor-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-dirdeclor dirdeclor fundefp gin)
                  (simpadd0-dirdeclor dirdeclor fundefp gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-absdeclor-absdeclor-equiv-congruence-on-absdeclor

(defthm simpadd0-absdeclor-absdeclor-equiv-congruence-on-absdeclor
  (implies (c$::absdeclor-equiv absdeclor absdeclor-equiv)
           (equal (simpadd0-absdeclor absdeclor gin)
                  (simpadd0-absdeclor absdeclor-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-absdeclor-gin-equiv-congruence-on-gin

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

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

(defthm
 simpadd0-absdeclor-option-absdeclor-option-equiv-congruence-on-absdeclor?
 (implies (c$::absdeclor-option-equiv absdeclor? absdeclor?-equiv)
          (equal (simpadd0-absdeclor-option absdeclor? gin)
                 (simpadd0-absdeclor-option absdeclor?-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-absdeclor-option-gin-equiv-congruence-on-gin

(defthm simpadd0-absdeclor-option-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-absdeclor-option absdeclor? gin)
                  (simpadd0-absdeclor-option absdeclor? gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor

(defthm
 simpadd0-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor
 (implies (c$::dirabsdeclor-equiv dirabsdeclor dirabsdeclor-equiv)
          (equal (simpadd0-dirabsdeclor dirabsdeclor gin)
                 (simpadd0-dirabsdeclor dirabsdeclor-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-dirabsdeclor-gin-equiv-congruence-on-gin

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

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

(defthm
 simpadd0-dirabsdeclor-option-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor?
 (implies
   (c$::dirabsdeclor-option-equiv dirabsdeclor? dirabsdeclor?-equiv)
   (equal (simpadd0-dirabsdeclor-option dirabsdeclor? gin)
          (simpadd0-dirabsdeclor-option dirabsdeclor?-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-dirabsdeclor-option-gin-equiv-congruence-on-gin

(defthm simpadd0-dirabsdeclor-option-gin-equiv-congruence-on-gin
 (implies
     (gin-equiv gin gin-equiv)
     (equal (simpadd0-dirabsdeclor-option dirabsdeclor? gin)
            (simpadd0-dirabsdeclor-option dirabsdeclor? gin-equiv)))
 :rule-classes :congruence)

Theorem: simpadd0-param-declon-param-declon-equiv-congruence-on-paramdeclon

(defthm
 simpadd0-param-declon-param-declon-equiv-congruence-on-paramdeclon
 (implies (c$::param-declon-equiv paramdeclon paramdeclon-equiv)
          (equal (simpadd0-param-declon paramdeclon gin)
                 (simpadd0-param-declon paramdeclon-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-param-declon-gin-equiv-congruence-on-gin

(defthm simpadd0-param-declon-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-param-declon paramdeclon gin)
                  (simpadd0-param-declon paramdeclon gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-param-declon-list-param-declon-list-equiv-congruence-on-paramdeclons

(defthm
 simpadd0-param-declon-list-param-declon-list-equiv-congruence-on-paramdeclons
 (implies
      (c$::param-declon-list-equiv paramdeclons paramdeclons-equiv)
      (equal (simpadd0-param-declon-list paramdeclons gin)
             (simpadd0-param-declon-list paramdeclons-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-param-declon-list-gin-equiv-congruence-on-gin

(defthm simpadd0-param-declon-list-gin-equiv-congruence-on-gin
  (implies
       (gin-equiv gin gin-equiv)
       (equal (simpadd0-param-declon-list paramdeclons gin)
              (simpadd0-param-declon-list paramdeclons gin-equiv)))
  :rule-classes :congruence)

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

(defthm
 simpadd0-param-declor-param-declor-equiv-congruence-on-paramdeclor
 (implies (c$::param-declor-equiv paramdeclor paramdeclor-equiv)
          (equal (simpadd0-param-declor paramdeclor gin)
                 (simpadd0-param-declor paramdeclor-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-param-declor-gin-equiv-congruence-on-gin

(defthm simpadd0-param-declor-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-param-declor paramdeclor gin)
                  (simpadd0-param-declor paramdeclor gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-tyname-tyname-equiv-congruence-on-tyname

(defthm simpadd0-tyname-tyname-equiv-congruence-on-tyname
  (implies (c$::tyname-equiv tyname tyname-equiv)
           (equal (simpadd0-tyname tyname gin)
                  (simpadd0-tyname tyname-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-tyname-gin-equiv-congruence-on-gin

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

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

(defthm
   simpadd0-struni-spec-struni-spec-equiv-congruence-on-struni-spec
  (implies (c$::struni-spec-equiv struni-spec struni-spec-equiv)
           (equal (simpadd0-struni-spec struni-spec gin)
                  (simpadd0-struni-spec struni-spec-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-struni-spec-gin-equiv-congruence-on-gin

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

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

(defthm
 simpadd0-struct-declon-struct-declon-equiv-congruence-on-structdeclon
 (implies (c$::struct-declon-equiv structdeclon structdeclon-equiv)
          (equal (simpadd0-struct-declon structdeclon gin)
                 (simpadd0-struct-declon structdeclon-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-struct-declon-gin-equiv-congruence-on-gin

(defthm simpadd0-struct-declon-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-struct-declon structdeclon gin)
                  (simpadd0-struct-declon structdeclon gin-equiv)))
  :rule-classes :congruence)

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

(defthm
 simpadd0-struct-declon-list-struct-declon-list-equiv-congruence-on-structdeclons
 (implies
    (c$::struct-declon-list-equiv structdeclons structdeclons-equiv)
    (equal (simpadd0-struct-declon-list structdeclons gin)
           (simpadd0-struct-declon-list structdeclons-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-struct-declon-list-gin-equiv-congruence-on-gin

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

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

(defthm
 simpadd0-struct-declor-struct-declor-equiv-congruence-on-structdeclor
 (implies (c$::struct-declor-equiv structdeclor structdeclor-equiv)
          (equal (simpadd0-struct-declor structdeclor gin)
                 (simpadd0-struct-declor structdeclor-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-struct-declor-gin-equiv-congruence-on-gin

(defthm simpadd0-struct-declor-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-struct-declor structdeclor gin)
                  (simpadd0-struct-declor structdeclor gin-equiv)))
  :rule-classes :congruence)

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

(defthm
 simpadd0-struct-declor-list-struct-declor-list-equiv-congruence-on-structdeclors
 (implies
    (c$::struct-declor-list-equiv structdeclors structdeclors-equiv)
    (equal (simpadd0-struct-declor-list structdeclors gin)
           (simpadd0-struct-declor-list structdeclors-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-struct-declor-list-gin-equiv-congruence-on-gin

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

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

(defthm simpadd0-enum-spec-enum-spec-equiv-congruence-on-enumspec
  (implies (c$::enum-spec-equiv enumspec enumspec-equiv)
           (equal (simpadd0-enum-spec enumspec gin)
                  (simpadd0-enum-spec enumspec-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-enum-spec-gin-equiv-congruence-on-gin

(defthm simpadd0-enum-spec-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-enum-spec enumspec gin)
                  (simpadd0-enum-spec enumspec gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-enumer-enumer-equiv-congruence-on-enumer

(defthm simpadd0-enumer-enumer-equiv-congruence-on-enumer
  (implies (c$::enumer-equiv enumer enumer-equiv)
           (equal (simpadd0-enumer enumer gin)
                  (simpadd0-enumer enumer-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-enumer-gin-equiv-congruence-on-gin

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

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

(defthm simpadd0-enumer-list-enumer-list-equiv-congruence-on-enumers
  (implies (c$::enumer-list-equiv enumers enumers-equiv)
           (equal (simpadd0-enumer-list enumers gin)
                  (simpadd0-enumer-list enumers-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-enumer-list-gin-equiv-congruence-on-gin

(defthm simpadd0-enumer-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-enumer-list enumers gin)
                  (simpadd0-enumer-list enumers gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-statassert-statassert-equiv-congruence-on-statassert

(defthm
      simpadd0-statassert-statassert-equiv-congruence-on-statassert
  (implies (c$::statassert-equiv statassert statassert-equiv)
           (equal (simpadd0-statassert statassert gin)
                  (simpadd0-statassert statassert-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-statassert-gin-equiv-congruence-on-gin

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

Theorem: simpadd0-initdeclor-initdeclor-equiv-congruence-on-initdeclor

(defthm
      simpadd0-initdeclor-initdeclor-equiv-congruence-on-initdeclor
  (implies (c$::initdeclor-equiv initdeclor initdeclor-equiv)
           (equal (simpadd0-initdeclor initdeclor gin)
                  (simpadd0-initdeclor initdeclor-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-initdeclor-gin-equiv-congruence-on-gin

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

Theorem: simpadd0-initdeclor-list-initdeclor-list-equiv-congruence-on-initdeclors

(defthm
 simpadd0-initdeclor-list-initdeclor-list-equiv-congruence-on-initdeclors
 (implies (c$::initdeclor-list-equiv initdeclors initdeclors-equiv)
          (equal (simpadd0-initdeclor-list initdeclors gin)
                 (simpadd0-initdeclor-list initdeclors-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-initdeclor-list-gin-equiv-congruence-on-gin

(defthm simpadd0-initdeclor-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-initdeclor-list initdeclors gin)
                  (simpadd0-initdeclor-list initdeclors gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-decl-decl-equiv-congruence-on-decl

(defthm simpadd0-decl-decl-equiv-congruence-on-decl
  (implies (c$::decl-equiv decl decl-equiv)
           (equal (simpadd0-decl decl gin)
                  (simpadd0-decl decl-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-decl-gin-equiv-congruence-on-gin

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

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

(defthm simpadd0-decl-list-decl-list-equiv-congruence-on-decls
  (implies (c$::decl-list-equiv decls decls-equiv)
           (equal (simpadd0-decl-list decls gin)
                  (simpadd0-decl-list decls-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-decl-list-gin-equiv-congruence-on-gin

(defthm simpadd0-decl-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-decl-list decls gin)
                  (simpadd0-decl-list decls gin-equiv)))
  :rule-classes :congruence)

Theorem: simpadd0-label-label-equiv-congruence-on-label

(defthm simpadd0-label-label-equiv-congruence-on-label
  (implies (c$::label-equiv label label-equiv)
           (equal (simpadd0-label label gin)
                  (simpadd0-label label-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-label-gin-equiv-congruence-on-gin

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

Theorem: simpadd0-stmt-stmt-equiv-congruence-on-stmt

(defthm simpadd0-stmt-stmt-equiv-congruence-on-stmt
  (implies (c$::stmt-equiv stmt stmt-equiv)
           (equal (simpadd0-stmt stmt gin)
                  (simpadd0-stmt stmt-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-stmt-gin-equiv-congruence-on-gin

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

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

(defthm simpadd0-comp-stmt-comp-stmt-equiv-congruence-on-cstmt
  (implies (c$::comp-stmt-equiv cstmt cstmt-equiv)
           (equal (simpadd0-comp-stmt cstmt gin)
                  (simpadd0-comp-stmt cstmt-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-comp-stmt-gin-equiv-congruence-on-gin

(defthm simpadd0-comp-stmt-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-comp-stmt cstmt gin)
                  (simpadd0-comp-stmt cstmt gin-equiv)))
  :rule-classes :congruence)

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

(defthm simpadd0-block-item-block-item-equiv-congruence-on-item
  (implies (c$::block-item-equiv item item-equiv)
           (equal (simpadd0-block-item item gin)
                  (simpadd0-block-item item-equiv gin)))
  :rule-classes :congruence)

Theorem: simpadd0-block-item-gin-equiv-congruence-on-gin

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

Theorem: simpadd0-block-item-list-block-item-list-equiv-congruence-on-items

(defthm
 simpadd0-block-item-list-block-item-list-equiv-congruence-on-items
 (implies (c$::block-item-list-equiv items items-equiv)
          (equal (simpadd0-block-item-list items gin)
                 (simpadd0-block-item-list items-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-block-item-list-gin-equiv-congruence-on-gin

(defthm simpadd0-block-item-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-block-item-list items gin)
                  (simpadd0-block-item-list items gin-equiv)))
  :rule-classes :congruence)

Theorem: expr-unambp-of-simpadd0-expr

(defthm expr-unambp-of-simpadd0-expr
  (b* (((mv ?new-expr ?gout)
        (simpadd0-expr expr gin)))
    (expr-unambp new-expr)))

Theorem: expr-list-unambp-of-simpadd0-expr-list

(defthm expr-list-unambp-of-simpadd0-expr-list
  (b* (((mv ?new-exprs ?gout)
        (simpadd0-expr-list exprs gin)))
    (expr-list-unambp new-exprs)))

Theorem: expr-option-unambp-of-simpadd0-expr-option

(defthm expr-option-unambp-of-simpadd0-expr-option
  (b* (((mv ?new-expr? ?gout)
        (simpadd0-expr-option expr? gin)))
    (expr-option-unambp new-expr?)))

Theorem: const-expr-unambp-of-simpadd0-const-expr

(defthm const-expr-unambp-of-simpadd0-const-expr
  (b* (((mv ?new-cexpr ?gout)
        (simpadd0-const-expr cexpr gin)))
    (const-expr-unambp new-cexpr)))

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

(defthm const-expr-option-unambp-of-simpadd0-const-expr-option
  (b* (((mv ?new-cexpr? ?gout)
        (simpadd0-const-expr-option cexpr? gin)))
    (const-expr-option-unambp new-cexpr?)))

Theorem: genassoc-unambp-of-simpadd0-genassoc

(defthm genassoc-unambp-of-simpadd0-genassoc
  (b* (((mv ?new-genassoc ?gout)
        (simpadd0-genassoc genassoc gin)))
    (genassoc-unambp new-genassoc)))

Theorem: genassoc-list-unambp-of-simpadd0-genassoc-list

(defthm genassoc-list-unambp-of-simpadd0-genassoc-list
  (b* (((mv ?new-genassocs ?gout)
        (simpadd0-genassoc-list genassocs gin)))
    (genassoc-list-unambp new-genassocs)))

Theorem: member-designor-unambp-of-simpadd0-member-designor

(defthm member-designor-unambp-of-simpadd0-member-designor
  (b* (((mv ?new-memdes ?gout)
        (simpadd0-member-designor memdes gin)))
    (member-designor-unambp new-memdes)))

Theorem: type-spec-unambp-of-simpadd0-type-spec

(defthm type-spec-unambp-of-simpadd0-type-spec
  (b* (((mv ?new-tyspec ?gout)
        (simpadd0-type-spec tyspec gin)))
    (type-spec-unambp new-tyspec)))

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

(defthm spec/qual-unambp-of-simpadd0-spec/qual
  (b* (((mv ?new-specqual ?gout)
        (simpadd0-spec/qual specqual gin)))
    (spec/qual-unambp new-specqual)))

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

(defthm spec/qual-list-unambp-of-simpadd0-spec/qual-list
  (b* (((mv ?new-specquals ?gout)
        (simpadd0-spec/qual-list specquals gin)))
    (spec/qual-list-unambp new-specquals)))

Theorem: align-spec-unambp-of-simpadd0-align-spec

(defthm align-spec-unambp-of-simpadd0-align-spec
  (b* (((mv ?new-alignspec ?gout)
        (simpadd0-align-spec alignspec gin)))
    (align-spec-unambp new-alignspec)))

Theorem: decl-spec-unambp-of-simpadd0-decl-spec

(defthm decl-spec-unambp-of-simpadd0-decl-spec
  (b* (((mv ?new-declspec ?gout)
        (simpadd0-decl-spec declspec gin)))
    (decl-spec-unambp new-declspec)))

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

(defthm decl-spec-list-unambp-of-simpadd0-decl-spec-list
  (b* (((mv ?new-declspecs ?gout)
        (simpadd0-decl-spec-list declspecs gin)))
    (decl-spec-list-unambp new-declspecs)))

Theorem: initer-unambp-of-simpadd0-initer

(defthm initer-unambp-of-simpadd0-initer
  (b* (((mv ?new-initer ?gout)
        (simpadd0-initer initer gin)))
    (initer-unambp new-initer)))

Theorem: initer-option-unambp-of-simpadd0-initer-option

(defthm initer-option-unambp-of-simpadd0-initer-option
  (b* (((mv ?new-initer? ?gout)
        (simpadd0-initer-option initer? gin)))
    (initer-option-unambp new-initer?)))

Theorem: desiniter-unambp-of-simpadd0-desiniter

(defthm desiniter-unambp-of-simpadd0-desiniter
  (b* (((mv ?new-desiniter ?gout)
        (simpadd0-desiniter desiniter gin)))
    (desiniter-unambp new-desiniter)))

Theorem: desiniter-list-unambp-of-simpadd0-desiniter-list

(defthm desiniter-list-unambp-of-simpadd0-desiniter-list
  (b* (((mv ?new-desiniters ?gout)
        (simpadd0-desiniter-list desiniters gin)))
    (desiniter-list-unambp new-desiniters)))

Theorem: designor-unambp-of-simpadd0-designor

(defthm designor-unambp-of-simpadd0-designor
  (b* (((mv ?new-designor ?gout)
        (simpadd0-designor designor gin)))
    (designor-unambp new-designor)))

Theorem: designor-list-unambp-of-simpadd0-designor-list

(defthm designor-list-unambp-of-simpadd0-designor-list
  (b* (((mv ?new-designors ?gout)
        (simpadd0-designor-list designors gin)))
    (designor-list-unambp new-designors)))

Theorem: declor-unambp-of-simpadd0-declor

(defthm declor-unambp-of-simpadd0-declor
  (b* (((mv ?new-declor ?new-fundefp ?gout)
        (simpadd0-declor declor fundefp gin)))
    (declor-unambp new-declor)))

Theorem: declor-option-unambp-of-simpadd0-declor-option

(defthm declor-option-unambp-of-simpadd0-declor-option
  (b* (((mv ?new-declor? ?gout)
        (simpadd0-declor-option declor? gin)))
    (declor-option-unambp new-declor?)))

Theorem: dirdeclor-unambp-of-simpadd0-dirdeclor

(defthm dirdeclor-unambp-of-simpadd0-dirdeclor
  (b* (((mv ?new-dirdeclor ?new-fundefp ?gout)
        (simpadd0-dirdeclor dirdeclor fundefp gin)))
    (dirdeclor-unambp new-dirdeclor)))

Theorem: absdeclor-unambp-of-simpadd0-absdeclor

(defthm absdeclor-unambp-of-simpadd0-absdeclor
  (b* (((mv ?new-absdeclor ?gout)
        (simpadd0-absdeclor absdeclor gin)))
    (absdeclor-unambp new-absdeclor)))

Theorem: absdeclor-option-unambp-of-simpadd0-absdeclor-option

(defthm absdeclor-option-unambp-of-simpadd0-absdeclor-option
  (b* (((mv ?new-absdeclor? ?gout)
        (simpadd0-absdeclor-option absdeclor? gin)))
    (absdeclor-option-unambp new-absdeclor?)))

Theorem: dirabsdeclor-unambp-of-simpadd0-dirabsdeclor

(defthm dirabsdeclor-unambp-of-simpadd0-dirabsdeclor
  (b* (((mv ?new-dirabsdeclor ?gout)
        (simpadd0-dirabsdeclor dirabsdeclor gin)))
    (dirabsdeclor-unambp new-dirabsdeclor)))

Theorem: dirabsdeclor-option-unambp-of-simpadd0-dirabsdeclor-option

(defthm dirabsdeclor-option-unambp-of-simpadd0-dirabsdeclor-option
  (b* (((mv ?new-dirabsdeclor? ?gout)
        (simpadd0-dirabsdeclor-option dirabsdeclor? gin)))
    (dirabsdeclor-option-unambp new-dirabsdeclor?)))

Theorem: param-declon-unambp-of-simpadd0-param-declon

(defthm param-declon-unambp-of-simpadd0-param-declon
  (b* (((mv ?new-paramdeclon ?gout)
        (simpadd0-param-declon paramdeclon gin)))
    (param-declon-unambp new-paramdeclon)))

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

(defthm param-declon-list-unambp-of-simpadd0-param-declon-list
  (b* (((mv ?new-paramdeclons ?gout)
        (simpadd0-param-declon-list paramdeclons gin)))
    (param-declon-list-unambp new-paramdeclons)))

Theorem: param-declor-unambp-of-simpadd0-param-declor

(defthm param-declor-unambp-of-simpadd0-param-declor
  (b* (((mv ?new-paramdeclor ?gout)
        (simpadd0-param-declor paramdeclor gin)))
    (param-declor-unambp new-paramdeclor)))

Theorem: tyname-unambp-of-simpadd0-tyname

(defthm tyname-unambp-of-simpadd0-tyname
  (b* (((mv ?new-tyname ?gout)
        (simpadd0-tyname tyname gin)))
    (tyname-unambp new-tyname)))

Theorem: struni-spec-unambp-of-simpadd0-struni-spec

(defthm struni-spec-unambp-of-simpadd0-struni-spec
  (b* (((mv ?new-struni-spec ?gout)
        (simpadd0-struni-spec struni-spec gin)))
    (struni-spec-unambp new-struni-spec)))

Theorem: struct-declon-unambp-of-simpadd0-struct-declon

(defthm struct-declon-unambp-of-simpadd0-struct-declon
  (b* (((mv ?new-structdeclon ?gout)
        (simpadd0-struct-declon structdeclon gin)))
    (struct-declon-unambp new-structdeclon)))

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

(defthm struct-declon-list-unambp-of-simpadd0-struct-declon-list
  (b* (((mv ?new-structdeclons ?gout)
        (simpadd0-struct-declon-list structdeclons gin)))
    (struct-declon-list-unambp new-structdeclons)))

Theorem: struct-declor-unambp-of-simpadd0-struct-declor

(defthm struct-declor-unambp-of-simpadd0-struct-declor
  (b* (((mv ?new-structdeclor ?gout)
        (simpadd0-struct-declor structdeclor gin)))
    (struct-declor-unambp new-structdeclor)))

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

(defthm struct-declor-list-unambp-of-simpadd0-struct-declor-list
  (b* (((mv ?new-structdeclors ?gout)
        (simpadd0-struct-declor-list structdeclors gin)))
    (struct-declor-list-unambp new-structdeclors)))

Theorem: enum-spec-unambp-of-simpadd0-enum-spec

(defthm enum-spec-unambp-of-simpadd0-enum-spec
  (b* (((mv ?new-enumspec ?gout)
        (simpadd0-enum-spec enumspec gin)))
    (enum-spec-unambp new-enumspec)))

Theorem: enumer-unambp-of-simpadd0-enumer

(defthm enumer-unambp-of-simpadd0-enumer
  (b* (((mv ?new-enumer ?gout)
        (simpadd0-enumer enumer gin)))
    (enumer-unambp new-enumer)))

Theorem: enumer-list-unambp-of-simpadd0-enumer-list

(defthm enumer-list-unambp-of-simpadd0-enumer-list
  (b* (((mv ?new-enumers ?gout)
        (simpadd0-enumer-list enumers gin)))
    (enumer-list-unambp new-enumers)))

Theorem: statassert-unambp-of-simpadd0-statassert

(defthm statassert-unambp-of-simpadd0-statassert
  (b* (((mv ?new-statassert ?gout)
        (simpadd0-statassert statassert gin)))
    (statassert-unambp new-statassert)))

Theorem: initdeclor-unambp-of-simpadd0-initdeclor

(defthm initdeclor-unambp-of-simpadd0-initdeclor
  (b* (((mv ?new-initdeclor ?gout)
        (simpadd0-initdeclor initdeclor gin)))
    (initdeclor-unambp new-initdeclor)))

Theorem: initdeclor-list-unambp-of-simpadd0-initdeclor-list

(defthm initdeclor-list-unambp-of-simpadd0-initdeclor-list
  (b* (((mv ?new-initdeclors ?gout)
        (simpadd0-initdeclor-list initdeclors gin)))
    (initdeclor-list-unambp new-initdeclors)))

Theorem: decl-unambp-of-simpadd0-decl

(defthm decl-unambp-of-simpadd0-decl
  (b* (((mv ?new-decl ?gout)
        (simpadd0-decl decl gin)))
    (decl-unambp new-decl)))

Theorem: decl-list-unambp-of-simpadd0-decl-list

(defthm decl-list-unambp-of-simpadd0-decl-list
  (b* (((mv ?new-decls ?gout)
        (simpadd0-decl-list decls gin)))
    (decl-list-unambp new-decls)))

Theorem: label-unambp-of-simpadd0-label

(defthm label-unambp-of-simpadd0-label
  (b* (((mv ?new-label ?gout)
        (simpadd0-label label gin)))
    (label-unambp new-label)))

Theorem: stmt-unambp-of-simpadd0-stmt

(defthm stmt-unambp-of-simpadd0-stmt
  (b* (((mv ?new-stmt ?gout)
        (simpadd0-stmt stmt gin)))
    (stmt-unambp new-stmt)))

Theorem: comp-stmt-unambp-of-simpadd0-block

(defthm comp-stmt-unambp-of-simpadd0-block
  (b* (((mv ?new-cstmt ?gout)
        (simpadd0-comp-stmt cstmt gin)))
    (comp-stmt-unambp new-cstmt)))

Theorem: block-item-unambp-of-simpadd0-block-item

(defthm block-item-unambp-of-simpadd0-block-item
  (b* (((mv ?new-item ?gout)
        (simpadd0-block-item item gin)))
    (block-item-unambp new-item)))

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

(defthm block-item-list-unambp-of-simpadd0-block-item-list
  (b* (((mv ?new-items ?gout)
        (simpadd0-block-item-list items gin)))
    (block-item-list-unambp new-items)))

Theorem: expr-annop-of-simpadd0-expr

(defthm expr-annop-of-simpadd0-expr
  (implies (and (expr-unambp expr)
                (expr-annop expr))
           (b* (((mv ?new-expr ?gout)
                 (simpadd0-expr expr gin)))
             (expr-annop new-expr))))

Theorem: expr-list-annop-of-simpadd0-expr-list

(defthm expr-list-annop-of-simpadd0-expr-list
  (implies (and (expr-list-unambp exprs)
                (expr-list-annop exprs))
           (b* (((mv ?new-exprs ?gout)
                 (simpadd0-expr-list exprs gin)))
             (expr-list-annop new-exprs))))

Theorem: expr-option-annop-of-simpadd0-expr-option

(defthm expr-option-annop-of-simpadd0-expr-option
  (implies (and (expr-option-unambp expr?)
                (expr-option-annop expr?))
           (b* (((mv ?new-expr? ?gout)
                 (simpadd0-expr-option expr? gin)))
             (expr-option-annop new-expr?))))

Theorem: const-expr-annop-of-simpadd0-const-expr

(defthm const-expr-annop-of-simpadd0-const-expr
  (implies (and (const-expr-unambp cexpr)
                (const-expr-annop cexpr))
           (b* (((mv ?new-cexpr ?gout)
                 (simpadd0-const-expr cexpr gin)))
             (const-expr-annop new-cexpr))))

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

(defthm const-expr-option-annop-of-simpadd0-const-expr-option
  (implies (and (const-expr-option-unambp cexpr?)
                (const-expr-option-annop cexpr?))
           (b* (((mv ?new-cexpr? ?gout)
                 (simpadd0-const-expr-option cexpr? gin)))
             (const-expr-option-annop new-cexpr?))))

Theorem: genassoc-annop-of-simpadd0-genassoc

(defthm genassoc-annop-of-simpadd0-genassoc
  (implies (and (genassoc-unambp genassoc)
                (genassoc-annop genassoc))
           (b* (((mv ?new-genassoc ?gout)
                 (simpadd0-genassoc genassoc gin)))
             (genassoc-annop new-genassoc))))

Theorem: genassoc-list-annop-of-simpadd0-genassoc-list

(defthm genassoc-list-annop-of-simpadd0-genassoc-list
  (implies (and (genassoc-list-unambp genassocs)
                (genassoc-list-annop genassocs))
           (b* (((mv ?new-genassocs ?gout)
                 (simpadd0-genassoc-list genassocs gin)))
             (genassoc-list-annop new-genassocs))))

Theorem: member-designor-annop-of-simpadd0-member-designor

(defthm member-designor-annop-of-simpadd0-member-designor
  (implies (and (member-designor-unambp memdes)
                (member-designor-annop memdes))
           (b* (((mv ?new-memdes ?gout)
                 (simpadd0-member-designor memdes gin)))
             (member-designor-annop new-memdes))))

Theorem: type-spec-annop-of-simpadd0-type-spec

(defthm type-spec-annop-of-simpadd0-type-spec
  (implies (and (type-spec-unambp tyspec)
                (type-spec-annop tyspec))
           (b* (((mv ?new-tyspec ?gout)
                 (simpadd0-type-spec tyspec gin)))
             (type-spec-annop new-tyspec))))

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

(defthm spec/qual-annop-of-simpadd0-spec/qual
  (implies (and (spec/qual-unambp specqual)
                (spec/qual-annop specqual))
           (b* (((mv ?new-specqual ?gout)
                 (simpadd0-spec/qual specqual gin)))
             (spec/qual-annop new-specqual))))

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

(defthm spec/qual-list-annop-of-simpadd0-spec/qual-list
  (implies (and (spec/qual-list-unambp specquals)
                (spec/qual-list-annop specquals))
           (b* (((mv ?new-specquals ?gout)
                 (simpadd0-spec/qual-list specquals gin)))
             (spec/qual-list-annop new-specquals))))

Theorem: align-spec-annop-of-simpadd0-align-spec

(defthm align-spec-annop-of-simpadd0-align-spec
  (implies (and (align-spec-unambp alignspec)
                (align-spec-annop alignspec))
           (b* (((mv ?new-alignspec ?gout)
                 (simpadd0-align-spec alignspec gin)))
             (align-spec-annop new-alignspec))))

Theorem: decl-spec-annop-of-simpadd0-decl-spec

(defthm decl-spec-annop-of-simpadd0-decl-spec
  (implies (and (decl-spec-unambp declspec)
                (decl-spec-annop declspec))
           (b* (((mv ?new-declspec ?gout)
                 (simpadd0-decl-spec declspec gin)))
             (decl-spec-annop new-declspec))))

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

(defthm decl-spec-list-annop-of-simpadd0-decl-spec-list
  (implies (and (decl-spec-list-unambp declspecs)
                (decl-spec-list-annop declspecs))
           (b* (((mv ?new-declspecs ?gout)
                 (simpadd0-decl-spec-list declspecs gin)))
             (decl-spec-list-annop new-declspecs))))

Theorem: initer-annop-of-simpadd0-initer

(defthm initer-annop-of-simpadd0-initer
  (implies (and (initer-unambp initer)
                (initer-annop initer))
           (b* (((mv ?new-initer ?gout)
                 (simpadd0-initer initer gin)))
             (initer-annop new-initer))))

Theorem: initer-option-annop-of-simpadd0-initer-option

(defthm initer-option-annop-of-simpadd0-initer-option
  (implies (and (initer-option-unambp initer?)
                (initer-option-annop initer?))
           (b* (((mv ?new-initer? ?gout)
                 (simpadd0-initer-option initer? gin)))
             (initer-option-annop new-initer?))))

Theorem: desiniter-annop-of-simpadd0-desiniter

(defthm desiniter-annop-of-simpadd0-desiniter
  (implies (and (desiniter-unambp desiniter)
                (desiniter-annop desiniter))
           (b* (((mv ?new-desiniter ?gout)
                 (simpadd0-desiniter desiniter gin)))
             (desiniter-annop new-desiniter))))

Theorem: desiniter-list-annop-of-simpadd0-desiniter-list

(defthm desiniter-list-annop-of-simpadd0-desiniter-list
  (implies (and (desiniter-list-unambp desiniters)
                (desiniter-list-annop desiniters))
           (b* (((mv ?new-desiniters ?gout)
                 (simpadd0-desiniter-list desiniters gin)))
             (desiniter-list-annop new-desiniters))))

Theorem: designor-annop-of-simpadd0-designor

(defthm designor-annop-of-simpadd0-designor
  (implies (and (designor-unambp designor)
                (designor-annop designor))
           (b* (((mv ?new-designor ?gout)
                 (simpadd0-designor designor gin)))
             (designor-annop new-designor))))

Theorem: designor-list-annop-of-simpadd0-designor-list

(defthm designor-list-annop-of-simpadd0-designor-list
  (implies (and (designor-list-unambp designors)
                (designor-list-annop designors))
           (b* (((mv ?new-designors ?gout)
                 (simpadd0-designor-list designors gin)))
             (designor-list-annop new-designors))))

Theorem: declor-annop-of-simpadd0-declor

(defthm declor-annop-of-simpadd0-declor
  (implies (and (declor-unambp declor)
                (declor-annop declor))
           (b* (((mv ?new-declor ?new-fundefp ?gout)
                 (simpadd0-declor declor fundefp gin)))
             (declor-annop new-declor))))

Theorem: declor-option-annop-of-simpadd0-declor-option

(defthm declor-option-annop-of-simpadd0-declor-option
  (implies (and (declor-option-unambp declor?)
                (declor-option-annop declor?))
           (b* (((mv ?new-declor? ?gout)
                 (simpadd0-declor-option declor? gin)))
             (declor-option-annop new-declor?))))

Theorem: dirdeclor-annop-of-simpadd0-dirdeclor

(defthm dirdeclor-annop-of-simpadd0-dirdeclor
  (implies (and (dirdeclor-unambp dirdeclor)
                (dirdeclor-annop dirdeclor))
           (b* (((mv ?new-dirdeclor ?new-fundefp ?gout)
                 (simpadd0-dirdeclor dirdeclor fundefp gin)))
             (dirdeclor-annop new-dirdeclor))))

Theorem: absdeclor-annop-of-simpadd0-absdeclor

(defthm absdeclor-annop-of-simpadd0-absdeclor
  (implies (and (absdeclor-unambp absdeclor)
                (absdeclor-annop absdeclor))
           (b* (((mv ?new-absdeclor ?gout)
                 (simpadd0-absdeclor absdeclor gin)))
             (absdeclor-annop new-absdeclor))))

Theorem: absdeclor-option-annop-of-simpadd0-absdeclor-option

(defthm absdeclor-option-annop-of-simpadd0-absdeclor-option
  (implies (and (absdeclor-option-unambp absdeclor?)
                (absdeclor-option-annop absdeclor?))
           (b* (((mv ?new-absdeclor? ?gout)
                 (simpadd0-absdeclor-option absdeclor? gin)))
             (absdeclor-option-annop new-absdeclor?))))

Theorem: dirabsdeclor-annop-of-simpadd0-dirabsdeclor

(defthm dirabsdeclor-annop-of-simpadd0-dirabsdeclor
  (implies (and (dirabsdeclor-unambp dirabsdeclor)
                (dirabsdeclor-annop dirabsdeclor))
           (b* (((mv ?new-dirabsdeclor ?gout)
                 (simpadd0-dirabsdeclor dirabsdeclor gin)))
             (dirabsdeclor-annop new-dirabsdeclor))))

Theorem: dirabsdeclor-option-annop-of-simpadd0-dirabsdeclor-option

(defthm dirabsdeclor-option-annop-of-simpadd0-dirabsdeclor-option
  (implies (and (dirabsdeclor-option-unambp dirabsdeclor?)
                (dirabsdeclor-option-annop dirabsdeclor?))
           (b* (((mv ?new-dirabsdeclor? ?gout)
                 (simpadd0-dirabsdeclor-option dirabsdeclor? gin)))
             (dirabsdeclor-option-annop new-dirabsdeclor?))))

Theorem: param-declon-annop-of-simpadd0-param-declon

(defthm param-declon-annop-of-simpadd0-param-declon
  (implies (and (param-declon-unambp paramdeclon)
                (param-declon-annop paramdeclon))
           (b* (((mv ?new-paramdeclon ?gout)
                 (simpadd0-param-declon paramdeclon gin)))
             (param-declon-annop new-paramdeclon))))

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

(defthm param-declon-list-annop-of-simpadd0-param-declon-list
  (implies (and (param-declon-list-unambp paramdeclons)
                (param-declon-list-annop paramdeclons))
           (b* (((mv ?new-paramdeclons ?gout)
                 (simpadd0-param-declon-list paramdeclons gin)))
             (param-declon-list-annop new-paramdeclons))))

Theorem: param-declor-annop-of-simpadd0-param-declor

(defthm param-declor-annop-of-simpadd0-param-declor
  (implies (and (param-declor-unambp paramdeclor)
                (param-declor-annop paramdeclor))
           (b* (((mv ?new-paramdeclor ?gout)
                 (simpadd0-param-declor paramdeclor gin)))
             (param-declor-annop new-paramdeclor))))

Theorem: tyname-annop-of-simpadd0-tyname

(defthm tyname-annop-of-simpadd0-tyname
  (implies (and (tyname-unambp tyname)
                (tyname-annop tyname))
           (b* (((mv ?new-tyname ?gout)
                 (simpadd0-tyname tyname gin)))
             (tyname-annop new-tyname))))

Theorem: struni-spec-annop-of-simpadd0-struni-spec

(defthm struni-spec-annop-of-simpadd0-struni-spec
  (implies (and (struni-spec-unambp struni-spec)
                (struni-spec-annop struni-spec))
           (b* (((mv ?new-struni-spec ?gout)
                 (simpadd0-struni-spec struni-spec gin)))
             (struni-spec-annop new-struni-spec))))

Theorem: struct-declon-annop-of-simpadd0-struct-declon

(defthm struct-declon-annop-of-simpadd0-struct-declon
  (implies (and (struct-declon-unambp structdeclon)
                (struct-declon-annop structdeclon))
           (b* (((mv ?new-structdeclon ?gout)
                 (simpadd0-struct-declon structdeclon gin)))
             (struct-declon-annop new-structdeclon))))

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

(defthm struct-declon-list-annop-of-simpadd0-struct-declon-list
  (implies (and (struct-declon-list-unambp structdeclons)
                (struct-declon-list-annop structdeclons))
           (b* (((mv ?new-structdeclons ?gout)
                 (simpadd0-struct-declon-list structdeclons gin)))
             (struct-declon-list-annop new-structdeclons))))

Theorem: struct-declor-annop-of-simpadd0-struct-declor

(defthm struct-declor-annop-of-simpadd0-struct-declor
  (implies (and (struct-declor-unambp structdeclor)
                (struct-declor-annop structdeclor))
           (b* (((mv ?new-structdeclor ?gout)
                 (simpadd0-struct-declor structdeclor gin)))
             (struct-declor-annop new-structdeclor))))

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

(defthm struct-declor-list-annop-of-simpadd0-struct-declor-list
  (implies (and (struct-declor-list-unambp structdeclors)
                (struct-declor-list-annop structdeclors))
           (b* (((mv ?new-structdeclors ?gout)
                 (simpadd0-struct-declor-list structdeclors gin)))
             (struct-declor-list-annop new-structdeclors))))

Theorem: enum-spec-annop-of-simpadd0-enum-spec

(defthm enum-spec-annop-of-simpadd0-enum-spec
  (implies (and (enum-spec-unambp enumspec)
                (enum-spec-annop enumspec))
           (b* (((mv ?new-enumspec ?gout)
                 (simpadd0-enum-spec enumspec gin)))
             (enum-spec-annop new-enumspec))))

Theorem: enumer-annop-of-simpadd0-enumer

(defthm enumer-annop-of-simpadd0-enumer
  (implies (and (enumer-unambp enumer)
                (enumer-annop enumer))
           (b* (((mv ?new-enumer ?gout)
                 (simpadd0-enumer enumer gin)))
             (enumer-annop new-enumer))))

Theorem: enumer-list-annop-of-simpadd0-enumer-list

(defthm enumer-list-annop-of-simpadd0-enumer-list
  (implies (and (enumer-list-unambp enumers)
                (enumer-list-annop enumers))
           (b* (((mv ?new-enumers ?gout)
                 (simpadd0-enumer-list enumers gin)))
             (enumer-list-annop new-enumers))))

Theorem: statassert-annop-of-simpadd0-statassert

(defthm statassert-annop-of-simpadd0-statassert
  (implies (and (statassert-unambp statassert)
                (statassert-annop statassert))
           (b* (((mv ?new-statassert ?gout)
                 (simpadd0-statassert statassert gin)))
             (statassert-annop new-statassert))))

Theorem: initdeclor-annop-of-simpadd0-initdeclor

(defthm initdeclor-annop-of-simpadd0-initdeclor
  (implies (and (initdeclor-unambp initdeclor)
                (initdeclor-annop initdeclor))
           (b* (((mv ?new-initdeclor ?gout)
                 (simpadd0-initdeclor initdeclor gin)))
             (initdeclor-annop new-initdeclor))))

Theorem: initdeclor-list-annop-of-simpadd0-initdeclor-list

(defthm initdeclor-list-annop-of-simpadd0-initdeclor-list
  (implies (and (initdeclor-list-unambp initdeclors)
                (initdeclor-list-annop initdeclors))
           (b* (((mv ?new-initdeclors ?gout)
                 (simpadd0-initdeclor-list initdeclors gin)))
             (initdeclor-list-annop new-initdeclors))))

Theorem: decl-annop-of-simpadd0-decl

(defthm decl-annop-of-simpadd0-decl
  (implies (and (decl-unambp decl)
                (decl-annop decl))
           (b* (((mv ?new-decl ?gout)
                 (simpadd0-decl decl gin)))
             (decl-annop new-decl))))

Theorem: decl-list-annop-of-simpadd0-decl-list

(defthm decl-list-annop-of-simpadd0-decl-list
  (implies (and (decl-list-unambp decls)
                (decl-list-annop decls))
           (b* (((mv ?new-decls ?gout)
                 (simpadd0-decl-list decls gin)))
             (decl-list-annop new-decls))))

Theorem: label-annop-of-simpadd0-label

(defthm label-annop-of-simpadd0-label
  (implies (and (label-unambp label)
                (label-annop label))
           (b* (((mv ?new-label ?gout)
                 (simpadd0-label label gin)))
             (label-annop new-label))))

Theorem: stmt-annop-of-simpadd0-stmt

(defthm stmt-annop-of-simpadd0-stmt
  (implies (and (stmt-unambp stmt)
                (stmt-annop stmt))
           (b* (((mv ?new-stmt ?gout)
                 (simpadd0-stmt stmt gin)))
             (stmt-annop new-stmt))))

Theorem: comp-stmt-annop-of-simpadd0-comp-stmt

(defthm comp-stmt-annop-of-simpadd0-comp-stmt
  (implies (and (comp-stmt-unambp cstmt)
                (comp-stmt-annop cstmt))
           (b* (((mv ?new-cstmt ?gout)
                 (simpadd0-comp-stmt cstmt gin)))
             (comp-stmt-annop new-cstmt))))

Theorem: block-item-annop-of-simpadd0-block-item

(defthm block-item-annop-of-simpadd0-block-item
  (implies (and (block-item-unambp item)
                (block-item-annop item))
           (b* (((mv ?new-item ?gout)
                 (simpadd0-block-item item gin)))
             (block-item-annop new-item))))

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

(defthm block-item-list-annop-of-simpadd0-block-item-list
  (implies (and (block-item-list-unambp items)
                (block-item-list-annop items))
           (b* (((mv ?new-items ?gout)
                 (simpadd0-block-item-list items gin)))
             (block-item-list-annop new-items))))

Theorem: expr-aidentp-of-simpadd0-expr

(defthm expr-aidentp-of-simpadd0-expr
  (implies (and (expr-unambp expr)
                (expr-aidentp expr gcc))
           (b* (((mv ?new-expr ?gout)
                 (simpadd0-expr expr gin)))
             (expr-aidentp new-expr gcc))))

Theorem: expr-list-aidentp-of-simpadd0-expr-list

(defthm expr-list-aidentp-of-simpadd0-expr-list
  (implies (and (expr-list-unambp exprs)
                (expr-list-aidentp exprs gcc))
           (b* (((mv ?new-exprs ?gout)
                 (simpadd0-expr-list exprs gin)))
             (expr-list-aidentp new-exprs gcc))))

Theorem: expr-option-aidentp-of-simpadd0-expr-option

(defthm expr-option-aidentp-of-simpadd0-expr-option
  (implies (and (expr-option-unambp expr?)
                (expr-option-aidentp expr? gcc))
           (b* (((mv ?new-expr? ?gout)
                 (simpadd0-expr-option expr? gin)))
             (expr-option-aidentp new-expr? gcc))))

Theorem: const-expr-aidentp-of-simpadd0-const-expr

(defthm const-expr-aidentp-of-simpadd0-const-expr
  (implies (and (const-expr-unambp cexpr)
                (const-expr-aidentp cexpr gcc))
           (b* (((mv ?new-cexpr ?gout)
                 (simpadd0-const-expr cexpr gin)))
             (const-expr-aidentp new-cexpr gcc))))

Theorem: const-expr-option-aidentp-of-simpadd0-const-expr-option

(defthm const-expr-option-aidentp-of-simpadd0-const-expr-option
  (implies (and (const-expr-option-unambp cexpr?)
                (const-expr-option-aidentp cexpr? gcc))
           (b* (((mv ?new-cexpr? ?gout)
                 (simpadd0-const-expr-option cexpr? gin)))
             (const-expr-option-aidentp new-cexpr? gcc))))

Theorem: genassoc-aidentp-of-simpadd0-genassoc

(defthm genassoc-aidentp-of-simpadd0-genassoc
  (implies (and (genassoc-unambp genassoc)
                (genassoc-aidentp genassoc gcc))
           (b* (((mv ?new-genassoc ?gout)
                 (simpadd0-genassoc genassoc gin)))
             (genassoc-aidentp new-genassoc gcc))))

Theorem: genassoc-list-aidentp-of-simpadd0-genassoc-list

(defthm genassoc-list-aidentp-of-simpadd0-genassoc-list
  (implies (and (genassoc-list-unambp genassocs)
                (genassoc-list-aidentp genassocs gcc))
           (b* (((mv ?new-genassocs ?gout)
                 (simpadd0-genassoc-list genassocs gin)))
             (genassoc-list-aidentp new-genassocs gcc))))

Theorem: member-designor-aidentp-of-simpadd0-member-designor

(defthm member-designor-aidentp-of-simpadd0-member-designor
  (implies (and (member-designor-unambp memdes)
                (member-designor-aidentp memdes gcc))
           (b* (((mv ?new-memdes ?gout)
                 (simpadd0-member-designor memdes gin)))
             (member-designor-aidentp new-memdes gcc))))

Theorem: type-spec-aidentp-of-simpadd0-type-spec

(defthm type-spec-aidentp-of-simpadd0-type-spec
  (implies (and (type-spec-unambp tyspec)
                (type-spec-aidentp tyspec gcc))
           (b* (((mv ?new-tyspec ?gout)
                 (simpadd0-type-spec tyspec gin)))
             (type-spec-aidentp new-tyspec gcc))))

Theorem: spec/qual-aidentp-of-simpadd0-spec/qual

(defthm spec/qual-aidentp-of-simpadd0-spec/qual
  (implies (and (spec/qual-unambp specqual)
                (spec/qual-aidentp specqual gcc))
           (b* (((mv ?new-specqual ?gout)
                 (simpadd0-spec/qual specqual gin)))
             (spec/qual-aidentp new-specqual gcc))))

Theorem: spec/qual-list-aidentp-of-simpadd0-spec/qual-list

(defthm spec/qual-list-aidentp-of-simpadd0-spec/qual-list
  (implies (and (spec/qual-list-unambp specquals)
                (spec/qual-list-aidentp specquals gcc))
           (b* (((mv ?new-specquals ?gout)
                 (simpadd0-spec/qual-list specquals gin)))
             (spec/qual-list-aidentp new-specquals gcc))))

Theorem: align-spec-aidentp-of-simpadd0-align-spec

(defthm align-spec-aidentp-of-simpadd0-align-spec
  (implies (and (align-spec-unambp alignspec)
                (align-spec-aidentp alignspec gcc))
           (b* (((mv ?new-alignspec ?gout)
                 (simpadd0-align-spec alignspec gin)))
             (align-spec-aidentp new-alignspec gcc))))

Theorem: decl-spec-aidentp-of-simpadd0-decl-spec

(defthm decl-spec-aidentp-of-simpadd0-decl-spec
  (implies (and (decl-spec-unambp declspec)
                (decl-spec-aidentp declspec gcc))
           (b* (((mv ?new-declspec ?gout)
                 (simpadd0-decl-spec declspec gin)))
             (decl-spec-aidentp new-declspec gcc))))

Theorem: decl-spec-list-aidentp-of-simpadd0-decl-spec-list

(defthm decl-spec-list-aidentp-of-simpadd0-decl-spec-list
  (implies (and (decl-spec-list-unambp declspecs)
                (decl-spec-list-aidentp declspecs gcc))
           (b* (((mv ?new-declspecs ?gout)
                 (simpadd0-decl-spec-list declspecs gin)))
             (decl-spec-list-aidentp new-declspecs gcc))))

Theorem: initer-aidentp-of-simpadd0-initer

(defthm initer-aidentp-of-simpadd0-initer
  (implies (and (initer-unambp initer)
                (initer-aidentp initer gcc))
           (b* (((mv ?new-initer ?gout)
                 (simpadd0-initer initer gin)))
             (initer-aidentp new-initer gcc))))

Theorem: initer-option-aidentp-of-simpadd0-initer-option

(defthm initer-option-aidentp-of-simpadd0-initer-option
  (implies (and (initer-option-unambp initer?)
                (initer-option-aidentp initer? gcc))
           (b* (((mv ?new-initer? ?gout)
                 (simpadd0-initer-option initer? gin)))
             (initer-option-aidentp new-initer? gcc))))

Theorem: desiniter-aidentp-of-simpadd0-desiniter

(defthm desiniter-aidentp-of-simpadd0-desiniter
  (implies (and (desiniter-unambp desiniter)
                (desiniter-aidentp desiniter gcc))
           (b* (((mv ?new-desiniter ?gout)
                 (simpadd0-desiniter desiniter gin)))
             (desiniter-aidentp new-desiniter gcc))))

Theorem: desiniter-list-aidentp-of-simpadd0-desiniter-list

(defthm desiniter-list-aidentp-of-simpadd0-desiniter-list
  (implies (and (desiniter-list-unambp desiniters)
                (desiniter-list-aidentp desiniters gcc))
           (b* (((mv ?new-desiniters ?gout)
                 (simpadd0-desiniter-list desiniters gin)))
             (desiniter-list-aidentp new-desiniters gcc))))

Theorem: designor-aidentp-of-simpadd0-designor

(defthm designor-aidentp-of-simpadd0-designor
  (implies (and (designor-unambp designor)
                (designor-aidentp designor gcc))
           (b* (((mv ?new-designor ?gout)
                 (simpadd0-designor designor gin)))
             (designor-aidentp new-designor gcc))))

Theorem: designor-list-aidentp-of-simpadd0-designor-list

(defthm designor-list-aidentp-of-simpadd0-designor-list
  (implies (and (designor-list-unambp designors)
                (designor-list-aidentp designors gcc))
           (b* (((mv ?new-designors ?gout)
                 (simpadd0-designor-list designors gin)))
             (designor-list-aidentp new-designors gcc))))

Theorem: declor-aidentp-of-simpadd0-declor

(defthm declor-aidentp-of-simpadd0-declor
  (implies (and (declor-unambp declor)
                (declor-aidentp declor gcc))
           (b* (((mv ?new-declor ?new-fundefp ?gout)
                 (simpadd0-declor declor fundefp gin)))
             (declor-aidentp new-declor gcc))))

Theorem: declor-option-aidentp-of-simpadd0-declor-option

(defthm declor-option-aidentp-of-simpadd0-declor-option
  (implies (and (declor-option-unambp declor?)
                (declor-option-aidentp declor? gcc))
           (b* (((mv ?new-declor? ?gout)
                 (simpadd0-declor-option declor? gin)))
             (declor-option-aidentp new-declor? gcc))))

Theorem: dirdeclor-aidentp-of-simpadd0-dirdeclor

(defthm dirdeclor-aidentp-of-simpadd0-dirdeclor
  (implies (and (dirdeclor-unambp dirdeclor)
                (dirdeclor-aidentp dirdeclor gcc))
           (b* (((mv ?new-dirdeclor ?new-fundefp ?gout)
                 (simpadd0-dirdeclor dirdeclor fundefp gin)))
             (dirdeclor-aidentp new-dirdeclor gcc))))

Theorem: absdeclor-aidentp-of-simpadd0-absdeclor

(defthm absdeclor-aidentp-of-simpadd0-absdeclor
  (implies (and (absdeclor-unambp absdeclor)
                (absdeclor-aidentp absdeclor gcc))
           (b* (((mv ?new-absdeclor ?gout)
                 (simpadd0-absdeclor absdeclor gin)))
             (absdeclor-aidentp new-absdeclor gcc))))

Theorem: absdeclor-option-aidentp-of-simpadd0-absdeclor-option

(defthm absdeclor-option-aidentp-of-simpadd0-absdeclor-option
  (implies (and (absdeclor-option-unambp absdeclor?)
                (absdeclor-option-aidentp absdeclor? gcc))
           (b* (((mv ?new-absdeclor? ?gout)
                 (simpadd0-absdeclor-option absdeclor? gin)))
             (absdeclor-option-aidentp new-absdeclor? gcc))))

Theorem: dirabsdeclor-aidentp-of-simpadd0-dirabsdeclor

(defthm dirabsdeclor-aidentp-of-simpadd0-dirabsdeclor
  (implies (and (dirabsdeclor-unambp dirabsdeclor)
                (dirabsdeclor-aidentp dirabsdeclor gcc))
           (b* (((mv ?new-dirabsdeclor ?gout)
                 (simpadd0-dirabsdeclor dirabsdeclor gin)))
             (dirabsdeclor-aidentp new-dirabsdeclor gcc))))

Theorem: dirabsdeclor-option-aidentp-of-simpadd0-dirabsdeclor-option

(defthm dirabsdeclor-option-aidentp-of-simpadd0-dirabsdeclor-option
  (implies (and (dirabsdeclor-option-unambp dirabsdeclor?)
                (dirabsdeclor-option-aidentp dirabsdeclor? gcc))
           (b* (((mv ?new-dirabsdeclor? ?gout)
                 (simpadd0-dirabsdeclor-option dirabsdeclor? gin)))
             (dirabsdeclor-option-aidentp new-dirabsdeclor? gcc))))

Theorem: param-declon-aidentp-of-simpadd0-param-declon

(defthm param-declon-aidentp-of-simpadd0-param-declon
  (implies (and (param-declon-unambp paramdeclon)
                (param-declon-aidentp paramdeclon gcc))
           (b* (((mv ?new-paramdeclon ?gout)
                 (simpadd0-param-declon paramdeclon gin)))
             (param-declon-aidentp new-paramdeclon gcc))))

Theorem: param-declon-list-aidentp-of-simpadd0-param-declon-list

(defthm param-declon-list-aidentp-of-simpadd0-param-declon-list
  (implies (and (param-declon-list-unambp paramdeclons)
                (param-declon-list-aidentp paramdeclons gcc))
           (b* (((mv ?new-paramdeclons ?gout)
                 (simpadd0-param-declon-list paramdeclons gin)))
             (param-declon-list-aidentp new-paramdeclons gcc))))

Theorem: param-declor-aidentp-of-simpadd0-param-declor

(defthm param-declor-aidentp-of-simpadd0-param-declor
  (implies (and (param-declor-unambp paramdeclor)
                (param-declor-aidentp paramdeclor gcc))
           (b* (((mv ?new-paramdeclor ?gout)
                 (simpadd0-param-declor paramdeclor gin)))
             (param-declor-aidentp new-paramdeclor gcc))))

Theorem: tyname-aidentp-of-simpadd0-tyname

(defthm tyname-aidentp-of-simpadd0-tyname
  (implies (and (tyname-unambp tyname)
                (tyname-aidentp tyname gcc))
           (b* (((mv ?new-tyname ?gout)
                 (simpadd0-tyname tyname gin)))
             (tyname-aidentp new-tyname gcc))))

Theorem: struni-spec-aidentp-of-simpadd0-struni-spec

(defthm struni-spec-aidentp-of-simpadd0-struni-spec
  (implies (and (struni-spec-unambp struni-spec)
                (struni-spec-aidentp struni-spec gcc))
           (b* (((mv ?new-struni-spec ?gout)
                 (simpadd0-struni-spec struni-spec gin)))
             (struni-spec-aidentp new-struni-spec gcc))))

Theorem: struct-declon-aidentp-of-simpadd0-struct-declon

(defthm struct-declon-aidentp-of-simpadd0-struct-declon
  (implies (and (struct-declon-unambp structdeclon)
                (struct-declon-aidentp structdeclon gcc))
           (b* (((mv ?new-structdeclon ?gout)
                 (simpadd0-struct-declon structdeclon gin)))
             (struct-declon-aidentp new-structdeclon gcc))))

Theorem: struct-declon-list-aidentp-of-simpadd0-struct-declon-list

(defthm struct-declon-list-aidentp-of-simpadd0-struct-declon-list
  (implies (and (struct-declon-list-unambp structdeclons)
                (struct-declon-list-aidentp structdeclons gcc))
           (b* (((mv ?new-structdeclons ?gout)
                 (simpadd0-struct-declon-list structdeclons gin)))
             (struct-declon-list-aidentp new-structdeclons gcc))))

Theorem: struct-declor-aidentp-of-simpadd0-struct-declor

(defthm struct-declor-aidentp-of-simpadd0-struct-declor
  (implies (and (struct-declor-unambp structdeclor)
                (struct-declor-aidentp structdeclor gcc))
           (b* (((mv ?new-structdeclor ?gout)
                 (simpadd0-struct-declor structdeclor gin)))
             (struct-declor-aidentp new-structdeclor gcc))))

Theorem: struct-declor-list-aidentp-of-simpadd0-struct-declor-list

(defthm struct-declor-list-aidentp-of-simpadd0-struct-declor-list
  (implies (and (struct-declor-list-unambp structdeclors)
                (struct-declor-list-aidentp structdeclors gcc))
           (b* (((mv ?new-structdeclors ?gout)
                 (simpadd0-struct-declor-list structdeclors gin)))
             (struct-declor-list-aidentp new-structdeclors gcc))))

Theorem: enum-spec-aidentp-of-simpadd0-enum-spec

(defthm enum-spec-aidentp-of-simpadd0-enum-spec
  (implies (and (enum-spec-unambp enumspec)
                (enum-spec-aidentp enumspec gcc))
           (b* (((mv ?new-enumspec ?gout)
                 (simpadd0-enum-spec enumspec gin)))
             (enum-spec-aidentp new-enumspec gcc))))

Theorem: enumer-aidentp-of-simpadd0-enumer

(defthm enumer-aidentp-of-simpadd0-enumer
  (implies (and (enumer-unambp enumer)
                (enumer-aidentp enumer gcc))
           (b* (((mv ?new-enumer ?gout)
                 (simpadd0-enumer enumer gin)))
             (enumer-aidentp new-enumer gcc))))

Theorem: enumer-list-aidentp-of-simpadd0-enumer-list

(defthm enumer-list-aidentp-of-simpadd0-enumer-list
  (implies (and (enumer-list-unambp enumers)
                (enumer-list-aidentp enumers gcc))
           (b* (((mv ?new-enumers ?gout)
                 (simpadd0-enumer-list enumers gin)))
             (enumer-list-aidentp new-enumers gcc))))

Theorem: statassert-aidentp-of-simpadd0-statassert

(defthm statassert-aidentp-of-simpadd0-statassert
  (implies (and (statassert-unambp statassert)
                (statassert-aidentp statassert gcc))
           (b* (((mv ?new-statassert ?gout)
                 (simpadd0-statassert statassert gin)))
             (statassert-aidentp new-statassert gcc))))

Theorem: initdeclor-aidentp-of-simpadd0-initdeclor

(defthm initdeclor-aidentp-of-simpadd0-initdeclor
  (implies (and (initdeclor-unambp initdeclor)
                (initdeclor-aidentp initdeclor gcc))
           (b* (((mv ?new-initdeclor ?gout)
                 (simpadd0-initdeclor initdeclor gin)))
             (initdeclor-aidentp new-initdeclor gcc))))

Theorem: initdeclor-list-aidentp-of-simpadd0-initdeclor-list

(defthm initdeclor-list-aidentp-of-simpadd0-initdeclor-list
  (implies (and (initdeclor-list-unambp initdeclors)
                (initdeclor-list-aidentp initdeclors gcc))
           (b* (((mv ?new-initdeclors ?gout)
                 (simpadd0-initdeclor-list initdeclors gin)))
             (initdeclor-list-aidentp new-initdeclors gcc))))

Theorem: decl-aidentp-of-simpadd0-decl

(defthm decl-aidentp-of-simpadd0-decl
  (implies (and (decl-unambp decl)
                (decl-aidentp decl gcc))
           (b* (((mv ?new-decl ?gout)
                 (simpadd0-decl decl gin)))
             (decl-aidentp new-decl gcc))))

Theorem: decl-list-aidentp-of-simpadd0-decl-list

(defthm decl-list-aidentp-of-simpadd0-decl-list
  (implies (and (decl-list-unambp decls)
                (decl-list-aidentp decls gcc))
           (b* (((mv ?new-decls ?gout)
                 (simpadd0-decl-list decls gin)))
             (decl-list-aidentp new-decls gcc))))

Theorem: label-aidentp-of-simpadd0-label

(defthm label-aidentp-of-simpadd0-label
  (implies (and (label-unambp label)
                (label-aidentp label gcc))
           (b* (((mv ?new-label ?gout)
                 (simpadd0-label label gin)))
             (label-aidentp new-label gcc))))

Theorem: stmt-aidentp-of-simpadd0-stmt

(defthm stmt-aidentp-of-simpadd0-stmt
  (implies (and (stmt-unambp stmt)
                (stmt-aidentp stmt gcc))
           (b* (((mv ?new-stmt ?gout)
                 (simpadd0-stmt stmt gin)))
             (stmt-aidentp new-stmt gcc))))

Theorem: comp-stmt-aidentp-of-simpadd0-comp-stmt

(defthm comp-stmt-aidentp-of-simpadd0-comp-stmt
  (implies (and (comp-stmt-unambp cstmt)
                (comp-stmt-aidentp cstmt gcc))
           (b* (((mv ?new-cstmt ?gout)
                 (simpadd0-comp-stmt cstmt gin)))
             (comp-stmt-aidentp new-cstmt gcc))))

Theorem: block-item-aidentp-of-simpadd0-block-item

(defthm block-item-aidentp-of-simpadd0-block-item
  (implies (and (block-item-unambp item)
                (block-item-aidentp item gcc))
           (b* (((mv ?new-item ?gout)
                 (simpadd0-block-item item gin)))
             (block-item-aidentp new-item gcc))))

Theorem: block-item-list-aidentp-of-simpadd0-block-item-list

(defthm block-item-list-aidentp-of-simpadd0-block-item-list
  (implies (and (block-item-list-unambp items)
                (block-item-list-aidentp items gcc))
           (b* (((mv ?new-items ?gout)
                 (simpadd0-block-item-list items gin)))
             (block-item-list-aidentp new-items gcc))))

Subtopics

Simpadd0-dirdeclor: Transform a direct declarator.
Simpadd0-declor: Transform a declarator.
Simpadd0-initdeclor: Transform an initializer declarator.
Simpadd0-initdeclor-list: Transform a list of initializer declarators.
Simpadd0-decl: Transform a declaration.
Simpadd0-comp-stmt: Transform a compound-statement.
Simpadd0-param-declor: Transform a parameter declarator.
Simpadd0-param-declon-list: Transform a list of parameter declarations.
Simpadd0-param-declon: Transform a parameter declaration.
Simpadd0-expr-option: Transform an optional expression.
Simpadd0-struct-declor-list: Transform a list of structure declarators.
Simpadd0-struct-declon-list: Transform a list of structure declarations.
Simpadd0-dirabsdeclor-option: Transform an optional direct abstract declarator.
Simpadd0-desiniter-list: Transform a list of initializers with optional designations.
Simpadd0-struni-spec: Transform a structure or union specifier.
Simpadd0-struct-declor: Transform a structure declarator.
Simpadd0-struct-declon: Transform a structure declaration.
Simpadd0-statassert: Transform an static assertion declaration.
Simpadd0-spec/qual-list: Transform a list of type specifiers and qualifiers.
Simpadd0-spec/qual: Transform a type specifier or qualifier.
Simpadd0-genassoc-list: Transform a list of generic associations.
Simpadd0-dirabsdeclor: Transform a direct abstract declarator.
Simpadd0-desiniter: Transform an initializer with optional designations.
Simpadd0-designor-list: Transform a list of designators.
Simpadd0-decl-spec-list: Transform a list of declaration specifiers.
Simpadd0-const-expr-option: Transform an optional constant expression.
Simpadd0-align-spec: Transform an alignment specifier.
Simpadd0-absdeclor-option: Transform an optional abstract declarator.
Simpadd0-type-spec: Transform a type specifier.
Simpadd0-tyname: Transform a type name.
Simpadd0-member-designor: Transform a member designator.
Simpadd0-initer-option: Transform an optional initializer.
Simpadd0-initer: Transform an initializer.
Simpadd0-genassoc: Transform a generic association.
Simpadd0-expr-list: Transform a list of expressions.
Simpadd0-enumer-list: Transform a list of enumerators.
Simpadd0-enumer: Transform an enumerator.
Simpadd0-enum-spec: Transform an enumeration specifier.
Simpadd0-designor: Transform a designator.
Simpadd0-declor-option: Transform an optional declarator.
Simpadd0-decl-spec: Transform a declaration specifier.
Simpadd0-decl-list: Transform a list of declarations.
Simpadd0-const-expr: Transform a constant expression.
Simpadd0-block-item-list: Transform a list of block items.
Simpadd0-block-item: Transform a block item.
Simpadd0-absdeclor: Transform an abstract declarator.
Simpadd0-stmt: Transform a statement.
Simpadd0-label: Transform a label.
Simpadd0-expr: Transform an expression.