Transform expressions, declarations, statements, and related entities.
Function:
(defun simpadd0-expr (expr) (declare (xargs :guard (exprp expr))) (declare (xargs :guard (expr-unambp expr))) (let ((__function__ 'simpadd0-expr)) (declare (ignorable __function__)) (expr-case expr :ident (expr-fix expr) :const (expr-fix expr) :string (expr-fix expr) :paren (expr-paren (simpadd0-expr expr.unwrap)) :gensel (make-expr-gensel :control (simpadd0-expr expr.control) :assocs (simpadd0-genassoc-list expr.assocs)) :arrsub (make-expr-arrsub :arg1 (simpadd0-expr expr.arg1) :arg2 (simpadd0-expr expr.arg2)) :funcall (make-expr-funcall :fun (simpadd0-expr expr.fun) :args (simpadd0-expr-list expr.args)) :member (make-expr-member :arg (simpadd0-expr expr.arg) :name expr.name) :memberp (make-expr-memberp :arg (simpadd0-expr expr.arg) :name expr.name) :complit (make-expr-complit :type (simpadd0-tyname expr.type) :elems (simpadd0-desiniter-list expr.elems) :final-comma expr.final-comma) :unary (make-expr-unary :op expr.op :arg (simpadd0-expr expr.arg)) :sizeof (expr-sizeof (simpadd0-tyname expr.type)) :sizeof-ambig (prog2$ (impossible) (irr-expr)) :alignof (make-expr-alignof :type (simpadd0-tyname expr.type) :uscores expr.uscores) :cast (make-expr-cast :type (simpadd0-tyname expr.type) :arg (simpadd0-expr expr.arg)) :binary (b* ((arg1 (simpadd0-expr expr.arg1)) (arg2 (simpadd0-expr expr.arg2))) (if (c$::expr-zerop arg2) arg1 (make-expr-binary :op expr.op :arg1 arg1 :arg2 arg2))) :cond (make-expr-cond :test (simpadd0-expr expr.test) :then (simpadd0-expr expr.then) :else (simpadd0-expr expr.else)) :comma (make-expr-comma :first (simpadd0-expr expr.first) :next (simpadd0-expr expr.next)) :cast/call-ambig (prog2$ (impossible) (irr-expr)) :cast/mul-ambig (prog2$ (impossible) (irr-expr)) :cast/add-ambig (prog2$ (impossible) (irr-expr)) :cast/sub-ambig (prog2$ (impossible) (irr-expr)) :cast/and-ambig (prog2$ (impossible) (irr-expr)) :stmt (expr-stmt (simpadd0-block-item-list expr.items)) :tycompat (make-expr-tycompat :type1 (simpadd0-tyname expr.type1) :type2 (simpadd0-tyname expr.type2)) :offsetof (make-expr-offsetof :type (simpadd0-tyname expr.type) :member (simpadd0-member-designor expr.member)))))
Function:
(defun simpadd0-expr-list (exprs) (declare (xargs :guard (expr-listp exprs))) (declare (xargs :guard (expr-list-unambp exprs))) (let ((__function__ 'simpadd0-expr-list)) (declare (ignorable __function__)) (cond ((endp exprs) nil) (t (cons (simpadd0-expr (car exprs)) (simpadd0-expr-list (cdr exprs)))))))
Function:
(defun simpadd0-expr-option (expr?) (declare (xargs :guard (expr-optionp expr?))) (declare (xargs :guard (expr-option-unambp expr?))) (let ((__function__ 'simpadd0-expr-option)) (declare (ignorable __function__)) (expr-option-case expr? :some (simpadd0-expr expr?.val) :none nil)))
Function:
(defun simpadd0-const-expr (cexpr) (declare (xargs :guard (const-exprp cexpr))) (declare (xargs :guard (const-expr-unambp cexpr))) (let ((__function__ 'simpadd0-const-expr)) (declare (ignorable __function__)) (const-expr (simpadd0-expr (const-expr->unwrap cexpr)))))
Function:
(defun simpadd0-const-expr-option (cexpr?) (declare (xargs :guard (const-expr-optionp cexpr?))) (declare (xargs :guard (const-expr-option-unambp cexpr?))) (let ((__function__ 'simpadd0-const-expr-option)) (declare (ignorable __function__)) (const-expr-option-case cexpr? :some (simpadd0-const-expr cexpr?.val) :none nil)))
Function:
(defun simpadd0-genassoc (genassoc) (declare (xargs :guard (genassocp genassoc))) (declare (xargs :guard (genassoc-unambp genassoc))) (let ((__function__ 'simpadd0-genassoc)) (declare (ignorable __function__)) (genassoc-case genassoc :type (make-genassoc-type :type (simpadd0-tyname genassoc.type) :expr (simpadd0-expr genassoc.expr)) :default (genassoc-default (simpadd0-expr genassoc.expr)))))
Function:
(defun simpadd0-genassoc-list (genassocs) (declare (xargs :guard (genassoc-listp genassocs))) (declare (xargs :guard (genassoc-list-unambp genassocs))) (let ((__function__ 'simpadd0-genassoc-list)) (declare (ignorable __function__)) (cond ((endp genassocs) nil) (t (cons (simpadd0-genassoc (car genassocs)) (simpadd0-genassoc-list (cdr genassocs)))))))
Function:
(defun simpadd0-member-designor (memdes) (declare (xargs :guard (member-designorp memdes))) (declare (xargs :guard (member-designor-unambp memdes))) (let ((__function__ 'simpadd0-member-designor)) (declare (ignorable __function__)) (member-designor-case memdes :ident (member-designor-fix memdes) :dot (make-member-designor-dot :member (simpadd0-member-designor memdes.member) :name memdes.name) :sub (make-member-designor-sub :member (simpadd0-member-designor memdes.member) :index (simpadd0-expr memdes.index)))))
Function:
(defun simpadd0-type-spec (tyspec) (declare (xargs :guard (type-specp tyspec))) (declare (xargs :guard (type-spec-unambp tyspec))) (let ((__function__ 'simpadd0-type-spec)) (declare (ignorable __function__)) (type-spec-case tyspec :void (type-spec-fix tyspec) :char (type-spec-fix tyspec) :short (type-spec-fix tyspec) :int (type-spec-fix tyspec) :long (type-spec-fix tyspec) :float (type-spec-fix tyspec) :double (type-spec-fix tyspec) :signed (type-spec-fix tyspec) :unsigned (type-spec-fix tyspec) :bool (type-spec-fix tyspec) :complex (type-spec-fix tyspec) :atomic (type-spec-atomic (simpadd0-tyname tyspec.type)) :struct (type-spec-struct (simpadd0-strunispec tyspec.unwrap)) :union (type-spec-union (simpadd0-strunispec tyspec.unwrap)) :enum (type-spec-enum (simpadd0-enumspec tyspec.unwrap)) :typedef (type-spec-fix tyspec) :int128 (type-spec-fix tyspec) :float128 (type-spec-fix tyspec) :builtin-va-list (type-spec-fix tyspec) :typeof-expr (make-type-spec-typeof-expr :expr (simpadd0-expr tyspec.expr) :uscores tyspec.uscores) :typeof-type (make-type-spec-typeof-type :type (simpadd0-tyname tyspec.type) :uscores tyspec.uscores) :typeof-ambig (prog2$ (impossible) (irr-type-spec)))))
Function:
(defun simpadd0-spec/qual (specqual) (declare (xargs :guard (spec/qual-p specqual))) (declare (xargs :guard (spec/qual-unambp specqual))) (let ((__function__ 'simpadd0-spec/qual)) (declare (ignorable __function__)) (spec/qual-case specqual :tyspec (spec/qual-tyspec (simpadd0-type-spec specqual.unwrap)) :tyqual (spec/qual-fix specqual) :align (spec/qual-align (simpadd0-align-spec specqual.unwrap)) :attrib (spec/qual-fix specqual))))
Function:
(defun simpadd0-spec/qual-list (specquals) (declare (xargs :guard (spec/qual-listp specquals))) (declare (xargs :guard (spec/qual-list-unambp specquals))) (let ((__function__ 'simpadd0-spec/qual-list)) (declare (ignorable __function__)) (cond ((endp specquals) nil) (t (cons (simpadd0-spec/qual (car specquals)) (simpadd0-spec/qual-list (cdr specquals)))))))
Function:
(defun simpadd0-align-spec (alignspec) (declare (xargs :guard (align-specp alignspec))) (declare (xargs :guard (align-spec-unambp alignspec))) (let ((__function__ 'simpadd0-align-spec)) (declare (ignorable __function__)) (align-spec-case alignspec :alignas-type (align-spec-alignas-type (simpadd0-tyname alignspec.type)) :alignas-expr (align-spec-alignas-expr (simpadd0-const-expr alignspec.arg)) :alignas-ambig (prog2$ (impossible) (irr-align-spec)))))
Function:
(defun simpadd0-declspec (declspec) (declare (xargs :guard (declspecp declspec))) (declare (xargs :guard (declspec-unambp declspec))) (let ((__function__ 'simpadd0-declspec)) (declare (ignorable __function__)) (declspec-case declspec :stocla (declspec-fix declspec) :tyspec (declspec-tyspec (simpadd0-type-spec declspec.unwrap)) :tyqual (declspec-fix declspec) :funspec (declspec-fix declspec) :align (declspec-align (simpadd0-align-spec declspec.unwrap)) :attrib (declspec-fix declspec))))
Function:
(defun simpadd0-declspec-list (declspecs) (declare (xargs :guard (declspec-listp declspecs))) (declare (xargs :guard (declspec-list-unambp declspecs))) (let ((__function__ 'simpadd0-declspec-list)) (declare (ignorable __function__)) (cond ((endp declspecs) nil) (t (cons (simpadd0-declspec (car declspecs)) (simpadd0-declspec-list (cdr declspecs)))))))
Function:
(defun simpadd0-initer (initer) (declare (xargs :guard (initerp initer))) (declare (xargs :guard (initer-unambp initer))) (let ((__function__ 'simpadd0-initer)) (declare (ignorable __function__)) (initer-case initer :single (initer-single (simpadd0-expr initer.expr)) :list (make-initer-list :elems (simpadd0-desiniter-list initer.elems) :final-comma initer.final-comma))))
Function:
(defun simpadd0-initer-option (initer?) (declare (xargs :guard (initer-optionp initer?))) (declare (xargs :guard (initer-option-unambp initer?))) (let ((__function__ 'simpadd0-initer-option)) (declare (ignorable __function__)) (initer-option-case initer? :some (simpadd0-initer initer?.val) :none nil)))
Function:
(defun simpadd0-desiniter (desiniter) (declare (xargs :guard (desiniterp desiniter))) (declare (xargs :guard (desiniter-unambp desiniter))) (let ((__function__ 'simpadd0-desiniter)) (declare (ignorable __function__)) (b* (((desiniter desiniter) desiniter)) (make-desiniter :design (simpadd0-designor-list desiniter.design) :init (simpadd0-initer desiniter.init)))))
Function:
(defun simpadd0-desiniter-list (desiniters) (declare (xargs :guard (desiniter-listp desiniters))) (declare (xargs :guard (desiniter-list-unambp desiniters))) (let ((__function__ 'simpadd0-desiniter-list)) (declare (ignorable __function__)) (cond ((endp desiniters) nil) (t (cons (simpadd0-desiniter (car desiniters)) (simpadd0-desiniter-list (cdr desiniters)))))))
Function:
(defun simpadd0-designor (designor) (declare (xargs :guard (designorp designor))) (declare (xargs :guard (designor-unambp designor))) (let ((__function__ 'simpadd0-designor)) (declare (ignorable __function__)) (designor-case designor :sub (designor-sub (simpadd0-const-expr designor.index)) :dot (designor-fix designor))))
Function:
(defun simpadd0-designor-list (designors) (declare (xargs :guard (designor-listp designors))) (declare (xargs :guard (designor-list-unambp designors))) (let ((__function__ 'simpadd0-designor-list)) (declare (ignorable __function__)) (cond ((endp designors) nil) (t (cons (simpadd0-designor (car designors)) (simpadd0-designor-list (cdr designors)))))))
Function:
(defun simpadd0-declor (declor) (declare (xargs :guard (declorp declor))) (declare (xargs :guard (declor-unambp declor))) (let ((__function__ 'simpadd0-declor)) (declare (ignorable __function__)) (b* (((declor declor) declor)) (make-declor :pointers declor.pointers :decl (simpadd0-dirdeclor declor.decl)))))
Function:
(defun simpadd0-declor-option (declor?) (declare (xargs :guard (declor-optionp declor?))) (declare (xargs :guard (declor-option-unambp declor?))) (let ((__function__ 'simpadd0-declor-option)) (declare (ignorable __function__)) (declor-option-case declor? :some (simpadd0-declor declor?.val) :none nil)))
Function:
(defun simpadd0-dirdeclor (dirdeclor) (declare (xargs :guard (dirdeclorp dirdeclor))) (declare (xargs :guard (dirdeclor-unambp dirdeclor))) (let ((__function__ 'simpadd0-dirdeclor)) (declare (ignorable __function__)) (dirdeclor-case dirdeclor :ident (dirdeclor-fix dirdeclor) :paren (dirdeclor-paren (simpadd0-declor dirdeclor.unwrap)) :array (make-dirdeclor-array :decl (simpadd0-dirdeclor dirdeclor.decl) :tyquals dirdeclor.tyquals :expr? (simpadd0-expr-option dirdeclor.expr?)) :array-static1 (make-dirdeclor-array-static1 :decl (simpadd0-dirdeclor dirdeclor.decl) :tyquals dirdeclor.tyquals :expr (simpadd0-expr dirdeclor.expr)) :array-static2 (make-dirdeclor-array-static2 :decl (simpadd0-dirdeclor dirdeclor.decl) :tyquals dirdeclor.tyquals :expr (simpadd0-expr dirdeclor.expr)) :array-star (make-dirdeclor-array-star :decl (simpadd0-dirdeclor dirdeclor.decl) :tyquals dirdeclor.tyquals) :function-params (make-dirdeclor-function-params :decl (simpadd0-dirdeclor dirdeclor.decl) :params (simpadd0-paramdecl-list dirdeclor.params) :ellipsis dirdeclor.ellipsis) :function-names (make-dirdeclor-function-names :decl (simpadd0-dirdeclor dirdeclor.decl) :names dirdeclor.names))))
Function:
(defun simpadd0-absdeclor (absdeclor) (declare (xargs :guard (absdeclorp absdeclor))) (declare (xargs :guard (absdeclor-unambp absdeclor))) (let ((__function__ 'simpadd0-absdeclor)) (declare (ignorable __function__)) (b* (((absdeclor absdeclor) absdeclor)) (make-absdeclor :pointers absdeclor.pointers :decl? (simpadd0-dirabsdeclor-option absdeclor.decl?)))))
Function:
(defun simpadd0-absdeclor-option (absdeclor?) (declare (xargs :guard (absdeclor-optionp absdeclor?))) (declare (xargs :guard (absdeclor-option-unambp absdeclor?))) (let ((__function__ 'simpadd0-absdeclor-option)) (declare (ignorable __function__)) (absdeclor-option-case absdeclor? :some (simpadd0-absdeclor absdeclor?.val) :none nil)))
Function:
(defun simpadd0-dirabsdeclor (dirabsdeclor) (declare (xargs :guard (dirabsdeclorp dirabsdeclor))) (declare (xargs :guard (dirabsdeclor-unambp dirabsdeclor))) (let ((__function__ 'simpadd0-dirabsdeclor)) (declare (ignorable __function__)) (dirabsdeclor-case dirabsdeclor :dummy-base (prog2$ (raise "Misusage error: ~x0." (dirabsdeclor-fix dirabsdeclor)) (irr-dirabsdeclor)) :paren (dirabsdeclor-paren (simpadd0-absdeclor dirabsdeclor.unwrap)) :array (make-dirabsdeclor-array :decl? (simpadd0-dirabsdeclor-option dirabsdeclor.decl?) :tyquals dirabsdeclor.tyquals :expr? (simpadd0-expr-option dirabsdeclor.expr?)) :array-static1 (make-dirabsdeclor-array-static1 :decl? (simpadd0-dirabsdeclor-option dirabsdeclor.decl?) :tyquals dirabsdeclor.tyquals :expr (simpadd0-expr dirabsdeclor.expr)) :array-static2 (make-dirabsdeclor-array-static2 :decl? (simpadd0-dirabsdeclor-option dirabsdeclor.decl?) :tyquals dirabsdeclor.tyquals :expr (simpadd0-expr dirabsdeclor.expr)) :array-star (dirabsdeclor-array-star (simpadd0-dirabsdeclor-option dirabsdeclor.decl?)) :function (make-dirabsdeclor-function :decl? (simpadd0-dirabsdeclor-option dirabsdeclor.decl?) :params (simpadd0-paramdecl-list dirabsdeclor.params) :ellipsis dirabsdeclor.ellipsis))))
Function:
(defun simpadd0-dirabsdeclor-option (dirabsdeclor?) (declare (xargs :guard (dirabsdeclor-optionp dirabsdeclor?))) (declare (xargs :guard (dirabsdeclor-option-unambp dirabsdeclor?))) (let ((__function__ 'simpadd0-dirabsdeclor-option)) (declare (ignorable __function__)) (dirabsdeclor-option-case dirabsdeclor? :some (simpadd0-dirabsdeclor dirabsdeclor?.val) :none nil)))
Function:
(defun simpadd0-paramdecl (paramdecl) (declare (xargs :guard (paramdeclp paramdecl))) (declare (xargs :guard (paramdecl-unambp paramdecl))) (let ((__function__ 'simpadd0-paramdecl)) (declare (ignorable __function__)) (b* (((paramdecl paramdecl) paramdecl)) (make-paramdecl :spec (simpadd0-declspec-list paramdecl.spec) :decl (simpadd0-paramdeclor paramdecl.decl)))))
Function:
(defun simpadd0-paramdecl-list (paramdecls) (declare (xargs :guard (paramdecl-listp paramdecls))) (declare (xargs :guard (paramdecl-list-unambp paramdecls))) (let ((__function__ 'simpadd0-paramdecl-list)) (declare (ignorable __function__)) (cond ((endp paramdecls) nil) (t (cons (simpadd0-paramdecl (car paramdecls)) (simpadd0-paramdecl-list (cdr paramdecls)))))))
Function:
(defun simpadd0-paramdeclor (paramdeclor) (declare (xargs :guard (paramdeclorp paramdeclor))) (declare (xargs :guard (paramdeclor-unambp paramdeclor))) (let ((__function__ 'simpadd0-paramdeclor)) (declare (ignorable __function__)) (paramdeclor-case paramdeclor :declor (paramdeclor-declor (simpadd0-declor paramdeclor.unwrap)) :absdeclor (paramdeclor-absdeclor (simpadd0-absdeclor paramdeclor.unwrap)) :none (paramdeclor-none) :ambig (prog2$ (impossible) (irr-paramdeclor)))))
Function:
(defun simpadd0-tyname (tyname) (declare (xargs :guard (tynamep tyname))) (declare (xargs :guard (tyname-unambp tyname))) (let ((__function__ 'simpadd0-tyname)) (declare (ignorable __function__)) (b* (((tyname tyname) tyname)) (make-tyname :specqual (simpadd0-spec/qual-list tyname.specqual) :decl? (simpadd0-absdeclor-option tyname.decl?)))))
Function:
(defun simpadd0-strunispec (strunispec) (declare (xargs :guard (strunispecp strunispec))) (declare (xargs :guard (strunispec-unambp strunispec))) (let ((__function__ 'simpadd0-strunispec)) (declare (ignorable __function__)) (b* (((strunispec strunispec) strunispec)) (make-strunispec :name strunispec.name :members (simpadd0-structdecl-list strunispec.members)))))
Function:
(defun simpadd0-structdecl (structdecl) (declare (xargs :guard (structdeclp structdecl))) (declare (xargs :guard (structdecl-unambp structdecl))) (let ((__function__ 'simpadd0-structdecl)) (declare (ignorable __function__)) (structdecl-case structdecl :member (make-structdecl-member :extension structdecl.extension :specqual (simpadd0-spec/qual-list structdecl.specqual) :declor (simpadd0-structdeclor-list structdecl.declor) :attrib structdecl.attrib) :statassert (structdecl-statassert (simpadd0-statassert structdecl.unwrap)))))
Function:
(defun simpadd0-structdecl-list (structdecls) (declare (xargs :guard (structdecl-listp structdecls))) (declare (xargs :guard (structdecl-list-unambp structdecls))) (let ((__function__ 'simpadd0-structdecl-list)) (declare (ignorable __function__)) (cond ((endp structdecls) nil) (t (cons (simpadd0-structdecl (car structdecls)) (simpadd0-structdecl-list (cdr structdecls)))))))
Function:
(defun simpadd0-structdeclor (structdeclor) (declare (xargs :guard (structdeclorp structdeclor))) (declare (xargs :guard (structdeclor-unambp structdeclor))) (let ((__function__ 'simpadd0-structdeclor)) (declare (ignorable __function__)) (b* (((structdeclor structdeclor) structdeclor)) (make-structdeclor :declor? (simpadd0-declor-option structdeclor.declor?) :expr? (simpadd0-const-expr-option structdeclor.expr?)))))
Function:
(defun simpadd0-structdeclor-list (structdeclors) (declare (xargs :guard (structdeclor-listp structdeclors))) (declare (xargs :guard (structdeclor-list-unambp structdeclors))) (let ((__function__ 'simpadd0-structdeclor-list)) (declare (ignorable __function__)) (cond ((endp structdeclors) nil) (t (cons (simpadd0-structdeclor (car structdeclors)) (simpadd0-structdeclor-list (cdr structdeclors)))))))
Function:
(defun simpadd0-enumspec (enumspec) (declare (xargs :guard (enumspecp enumspec))) (declare (xargs :guard (enumspec-unambp enumspec))) (let ((__function__ 'simpadd0-enumspec)) (declare (ignorable __function__)) (b* (((enumspec enumspec) enumspec)) (make-enumspec :name enumspec.name :list (simpadd0-enumer-list enumspec.list) :final-comma enumspec.final-comma))))
Function:
(defun simpadd0-enumer (enumer) (declare (xargs :guard (enumerp enumer))) (declare (xargs :guard (enumer-unambp enumer))) (let ((__function__ 'simpadd0-enumer)) (declare (ignorable __function__)) (b* (((enumer enumer) enumer)) (make-enumer :name enumer.name :value (simpadd0-const-expr-option enumer.value)))))
Function:
(defun simpadd0-enumer-list (enumers) (declare (xargs :guard (enumer-listp enumers))) (declare (xargs :guard (enumer-list-unambp enumers))) (let ((__function__ 'simpadd0-enumer-list)) (declare (ignorable __function__)) (cond ((endp enumers) nil) (t (cons (simpadd0-enumer (car enumers)) (simpadd0-enumer-list (cdr enumers)))))))
Function:
(defun simpadd0-statassert (statassert) (declare (xargs :guard (statassertp statassert))) (declare (xargs :guard (statassert-unambp statassert))) (let ((__function__ 'simpadd0-statassert)) (declare (ignorable __function__)) (b* (((statassert statassert) statassert)) (make-statassert :test (simpadd0-const-expr statassert.test) :message statassert.message))))
Function:
(defun simpadd0-initdeclor (initdeclor) (declare (xargs :guard (initdeclorp initdeclor))) (declare (xargs :guard (initdeclor-unambp initdeclor))) (let ((__function__ 'simpadd0-initdeclor)) (declare (ignorable __function__)) (b* (((initdeclor initdeclor) initdeclor)) (make-initdeclor :declor (simpadd0-declor initdeclor.declor) :asm? initdeclor.asm? :init? (simpadd0-initer-option initdeclor.init?)))))
Function:
(defun simpadd0-initdeclor-list (initdeclors) (declare (xargs :guard (initdeclor-listp initdeclors))) (declare (xargs :guard (initdeclor-list-unambp initdeclors))) (let ((__function__ 'simpadd0-initdeclor-list)) (declare (ignorable __function__)) (cond ((endp initdeclors) nil) (t (cons (simpadd0-initdeclor (car initdeclors)) (simpadd0-initdeclor-list (cdr initdeclors)))))))
Function:
(defun simpadd0-decl (decl) (declare (xargs :guard (declp decl))) (declare (xargs :guard (decl-unambp decl))) (let ((__function__ 'simpadd0-decl)) (declare (ignorable __function__)) (decl-case decl :decl (make-decl-decl :extension decl.extension :specs (simpadd0-declspec-list decl.specs) :init (simpadd0-initdeclor-list decl.init) :attrib decl.attrib) :statassert (decl-statassert (simpadd0-statassert decl.unwrap)))))
Function:
(defun simpadd0-decl-list (decls) (declare (xargs :guard (decl-listp decls))) (declare (xargs :guard (decl-list-unambp decls))) (let ((__function__ 'simpadd0-decl-list)) (declare (ignorable __function__)) (cond ((endp decls) nil) (t (cons (simpadd0-decl (car decls)) (simpadd0-decl-list (cdr decls)))))))
Function:
(defun simpadd0-label (label) (declare (xargs :guard (labelp label))) (declare (xargs :guard (label-unambp label))) (let ((__function__ 'simpadd0-label)) (declare (ignorable __function__)) (label-case label :name (label-fix label) :casexpr (make-label-casexpr :expr (simpadd0-const-expr label.expr) :range? (simpadd0-const-expr-option label.range?)) :default (label-fix label))))
Function:
(defun simpadd0-stmt (stmt) (declare (xargs :guard (stmtp stmt))) (declare (xargs :guard (stmt-unambp stmt))) (let ((__function__ 'simpadd0-stmt)) (declare (ignorable __function__)) (stmt-case stmt :labeled (make-stmt-labeled :label (simpadd0-label stmt.label) :stmt (simpadd0-stmt stmt.stmt)) :compound (stmt-compound (simpadd0-block-item-list stmt.items)) :expr (stmt-expr (simpadd0-expr-option stmt.expr?)) :if (make-stmt-if :test (simpadd0-expr stmt.test) :then (simpadd0-stmt stmt.then)) :ifelse (make-stmt-ifelse :test (simpadd0-expr stmt.test) :then (simpadd0-stmt stmt.then) :else (simpadd0-stmt stmt.else)) :switch (make-stmt-switch :target (simpadd0-expr stmt.target) :body (simpadd0-stmt stmt.body)) :while (make-stmt-while :test (simpadd0-expr stmt.test) :body (simpadd0-stmt stmt.body)) :dowhile (make-stmt-dowhile :body (simpadd0-stmt stmt.body) :test (simpadd0-expr stmt.test)) :for-expr (make-stmt-for-expr :init (simpadd0-expr-option stmt.init) :test (simpadd0-expr-option stmt.test) :next (simpadd0-expr-option stmt.next) :body (simpadd0-stmt stmt.body)) :for-decl (make-stmt-for-decl :init (simpadd0-decl stmt.init) :test (simpadd0-expr-option stmt.test) :next (simpadd0-expr-option stmt.next) :body (simpadd0-stmt stmt.body)) :for-ambig (prog2$ (impossible) (irr-stmt)) :goto (stmt-fix stmt) :continue (stmt-fix stmt) :break (stmt-fix stmt) :return (stmt-return (simpadd0-expr-option stmt.expr?)) :asm (stmt-fix stmt))))
Function:
(defun simpadd0-block-item (item) (declare (xargs :guard (block-itemp item))) (declare (xargs :guard (block-item-unambp item))) (let ((__function__ 'simpadd0-block-item)) (declare (ignorable __function__)) (block-item-case item :decl (block-item-decl (simpadd0-decl item.unwrap)) :stmt (block-item-stmt (simpadd0-stmt item.unwrap)) :ambig (prog2$ (impossible) (irr-block-item)))))
Function:
(defun simpadd0-block-item-list (items) (declare (xargs :guard (block-item-listp items))) (declare (xargs :guard (block-item-list-unambp items))) (let ((__function__ 'simpadd0-block-item-list)) (declare (ignorable __function__)) (cond ((endp items) nil) (t (cons (simpadd0-block-item (car items)) (simpadd0-block-item-list (cdr items)))))))
Theorem:
(defthm return-type-of-simpadd0-expr.new-expr (b* ((?new-expr (simpadd0-expr expr))) (exprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-expr-list.new-exprs (b* ((?new-exprs (simpadd0-expr-list exprs))) (expr-listp new-exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-expr-option.new-expr? (b* ((?new-expr? (simpadd0-expr-option expr?))) (expr-optionp new-expr?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-const-expr.new-cexpr (b* ((?new-cexpr (simpadd0-const-expr cexpr))) (const-exprp new-cexpr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-const-expr-option.new-cexpr? (b* ((?new-cexpr? (simpadd0-const-expr-option cexpr?))) (const-expr-optionp new-cexpr?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-genassoc.new-genassoc (b* ((?new-genassoc (simpadd0-genassoc genassoc))) (genassocp new-genassoc)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-genassoc-list.new-genassocs (b* ((?new-genassocs (simpadd0-genassoc-list genassocs))) (genassoc-listp new-genassocs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-member-designor.new-memdes (b* ((?new-memdes (simpadd0-member-designor memdes))) (member-designorp new-memdes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-type-spec.new-tyspec (b* ((?new-tyspec (simpadd0-type-spec tyspec))) (type-specp new-tyspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-spec/qual.new-specqual (b* ((?new-specqual (simpadd0-spec/qual specqual))) (spec/qual-p new-specqual)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-spec/qual-list.new-specquals (b* ((?new-specquals (simpadd0-spec/qual-list specquals))) (spec/qual-listp new-specquals)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-align-spec.new-alignspec (b* ((?new-alignspec (simpadd0-align-spec alignspec))) (align-specp new-alignspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-declspec.new-declspec (b* ((?new-declspec (simpadd0-declspec declspec))) (declspecp new-declspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-declspec-list.new-declspecs (b* ((?new-declspecs (simpadd0-declspec-list declspecs))) (declspec-listp new-declspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-initer.new-initer (b* ((?new-initer (simpadd0-initer initer))) (initerp new-initer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-initer-option.new-initer? (b* ((?new-initer? (simpadd0-initer-option initer?))) (initer-optionp new-initer?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-desiniter.new-desiniter (b* ((?new-desiniter (simpadd0-desiniter desiniter))) (desiniterp new-desiniter)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-desiniter-list.new-desiniters (b* ((?new-desiniters (simpadd0-desiniter-list desiniters))) (desiniter-listp new-desiniters)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-designor.new-designor (b* ((?new-designor (simpadd0-designor designor))) (designorp new-designor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-designor-list.new-designors (b* ((?new-designors (simpadd0-designor-list designors))) (designor-listp new-designors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-declor.new-declor (b* ((?new-declor (simpadd0-declor declor))) (declorp new-declor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-declor-option.new-declor? (b* ((?new-declor? (simpadd0-declor-option declor?))) (declor-optionp new-declor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-dirdeclor.new-dirdeclor (b* ((?new-dirdeclor (simpadd0-dirdeclor dirdeclor))) (dirdeclorp new-dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-absdeclor.new-absdeclor (b* ((?new-absdeclor (simpadd0-absdeclor absdeclor))) (absdeclorp new-absdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-absdeclor-option.new-absdeclor? (b* ((?new-absdeclor? (simpadd0-absdeclor-option absdeclor?))) (absdeclor-optionp new-absdeclor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-dirabsdeclor.new-dirabsdeclor (b* ((?new-dirabsdeclor (simpadd0-dirabsdeclor dirabsdeclor))) (dirabsdeclorp new-dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-dirabsdeclor-option.new-dirabsdeclor? (b* ((?new-dirabsdeclor? (simpadd0-dirabsdeclor-option dirabsdeclor?))) (dirabsdeclor-optionp new-dirabsdeclor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-paramdecl.new-paramdecl (b* ((?new-paramdecl (simpadd0-paramdecl paramdecl))) (paramdeclp new-paramdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-paramdecl-list.new-paramdecls (b* ((?new-paramdecls (simpadd0-paramdecl-list paramdecls))) (paramdecl-listp new-paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-paramdeclor.new-paramdeclor (b* ((?new-paramdeclor (simpadd0-paramdeclor paramdeclor))) (paramdeclorp new-paramdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-tyname.new-tyname (b* ((?new-tyname (simpadd0-tyname tyname))) (tynamep new-tyname)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-strunispec.new-strunispec (b* ((?new-strunispec (simpadd0-strunispec strunispec))) (strunispecp new-strunispec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-structdecl.new-structdecl (b* ((?new-structdecl (simpadd0-structdecl structdecl))) (structdeclp new-structdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-structdecl-list.new-structdecls (b* ((?new-structdecls (simpadd0-structdecl-list structdecls))) (structdecl-listp new-structdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-structdeclor.new-structdeclor (b* ((?new-structdeclor (simpadd0-structdeclor structdeclor))) (structdeclorp new-structdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-structdeclor-list.new-structdeclors (b* ((?new-structdeclors (simpadd0-structdeclor-list structdeclors))) (structdeclor-listp new-structdeclors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-enumspec.new-enumspec (b* ((?new-enumspec (simpadd0-enumspec enumspec))) (enumspecp new-enumspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-enumer.new-enumer (b* ((?new-enumer (simpadd0-enumer enumer))) (enumerp new-enumer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-enumer-list.new-enumers (b* ((?new-enumers (simpadd0-enumer-list enumers))) (enumer-listp new-enumers)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-statassert.new-statassert (b* ((?new-statassert (simpadd0-statassert statassert))) (statassertp new-statassert)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-initdeclor.new-initdeclor (b* ((?new-initdeclor (simpadd0-initdeclor initdeclor))) (initdeclorp new-initdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-initdeclor-list.new-initdeclors (b* ((?new-initdeclors (simpadd0-initdeclor-list initdeclors))) (initdeclor-listp new-initdeclors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-decl.new-decl (b* ((?new-decl (simpadd0-decl decl))) (declp new-decl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-decl-list.new-decls (b* ((?new-decls (simpadd0-decl-list decls))) (decl-listp new-decls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-label.new-label (b* ((?new-label (simpadd0-label label))) (labelp new-label)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-stmt.new-stmt (b* ((?new-stmt (simpadd0-stmt stmt))) (stmtp new-stmt)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-block-item.new-item (b* ((?new-item (simpadd0-block-item item))) (block-itemp new-item)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-simpadd0-block-item-list.new-items (b* ((?new-items (simpadd0-block-item-list items))) (block-item-listp new-items)) :rule-classes :rewrite)
Theorem:
(defthm simpadd0-expr-of-expr-fix-expr (equal (simpadd0-expr (expr-fix expr)) (simpadd0-expr expr)))
Theorem:
(defthm simpadd0-expr-list-of-expr-list-fix-exprs (equal (simpadd0-expr-list (expr-list-fix exprs)) (simpadd0-expr-list exprs)))
Theorem:
(defthm simpadd0-expr-option-of-expr-option-fix-expr? (equal (simpadd0-expr-option (expr-option-fix expr?)) (simpadd0-expr-option expr?)))
Theorem:
(defthm simpadd0-const-expr-of-const-expr-fix-cexpr (equal (simpadd0-const-expr (c$::const-expr-fix cexpr)) (simpadd0-const-expr cexpr)))
Theorem:
(defthm simpadd0-const-expr-option-of-const-expr-option-fix-cexpr? (equal (simpadd0-const-expr-option (const-expr-option-fix cexpr?)) (simpadd0-const-expr-option cexpr?)))
Theorem:
(defthm simpadd0-genassoc-of-genassoc-fix-genassoc (equal (simpadd0-genassoc (genassoc-fix genassoc)) (simpadd0-genassoc genassoc)))
Theorem:
(defthm simpadd0-genassoc-list-of-genassoc-list-fix-genassocs (equal (simpadd0-genassoc-list (genassoc-list-fix genassocs)) (simpadd0-genassoc-list genassocs)))
Theorem:
(defthm simpadd0-member-designor-of-member-designor-fix-memdes (equal (simpadd0-member-designor (member-designor-fix memdes)) (simpadd0-member-designor memdes)))
Theorem:
(defthm simpadd0-type-spec-of-type-spec-fix-tyspec (equal (simpadd0-type-spec (type-spec-fix tyspec)) (simpadd0-type-spec tyspec)))
Theorem:
(defthm simpadd0-spec/qual-of-spec/qual-fix-specqual (equal (simpadd0-spec/qual (spec/qual-fix specqual)) (simpadd0-spec/qual specqual)))
Theorem:
(defthm simpadd0-spec/qual-list-of-spec/qual-list-fix-specquals (equal (simpadd0-spec/qual-list (spec/qual-list-fix specquals)) (simpadd0-spec/qual-list specquals)))
Theorem:
(defthm simpadd0-align-spec-of-align-spec-fix-alignspec (equal (simpadd0-align-spec (align-spec-fix alignspec)) (simpadd0-align-spec alignspec)))
Theorem:
(defthm simpadd0-declspec-of-declspec-fix-declspec (equal (simpadd0-declspec (declspec-fix declspec)) (simpadd0-declspec declspec)))
Theorem:
(defthm simpadd0-declspec-list-of-declspec-list-fix-declspecs (equal (simpadd0-declspec-list (declspec-list-fix declspecs)) (simpadd0-declspec-list declspecs)))
Theorem:
(defthm simpadd0-initer-of-initer-fix-initer (equal (simpadd0-initer (initer-fix initer)) (simpadd0-initer initer)))
Theorem:
(defthm simpadd0-initer-option-of-initer-option-fix-initer? (equal (simpadd0-initer-option (initer-option-fix initer?)) (simpadd0-initer-option initer?)))
Theorem:
(defthm simpadd0-desiniter-of-desiniter-fix-desiniter (equal (simpadd0-desiniter (desiniter-fix desiniter)) (simpadd0-desiniter desiniter)))
Theorem:
(defthm simpadd0-desiniter-list-of-desiniter-list-fix-desiniters (equal (simpadd0-desiniter-list (desiniter-list-fix desiniters)) (simpadd0-desiniter-list desiniters)))
Theorem:
(defthm simpadd0-designor-of-designor-fix-designor (equal (simpadd0-designor (designor-fix designor)) (simpadd0-designor designor)))
Theorem:
(defthm simpadd0-designor-list-of-designor-list-fix-designors (equal (simpadd0-designor-list (designor-list-fix designors)) (simpadd0-designor-list designors)))
Theorem:
(defthm simpadd0-declor-of-declor-fix-declor (equal (simpadd0-declor (declor-fix declor)) (simpadd0-declor declor)))
Theorem:
(defthm simpadd0-declor-option-of-declor-option-fix-declor? (equal (simpadd0-declor-option (declor-option-fix declor?)) (simpadd0-declor-option declor?)))
Theorem:
(defthm simpadd0-dirdeclor-of-dirdeclor-fix-dirdeclor (equal (simpadd0-dirdeclor (dirdeclor-fix dirdeclor)) (simpadd0-dirdeclor dirdeclor)))
Theorem:
(defthm simpadd0-absdeclor-of-absdeclor-fix-absdeclor (equal (simpadd0-absdeclor (absdeclor-fix absdeclor)) (simpadd0-absdeclor absdeclor)))
Theorem:
(defthm simpadd0-absdeclor-option-of-absdeclor-option-fix-absdeclor? (equal (simpadd0-absdeclor-option (absdeclor-option-fix absdeclor?)) (simpadd0-absdeclor-option absdeclor?)))
Theorem:
(defthm simpadd0-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor (equal (simpadd0-dirabsdeclor (dirabsdeclor-fix dirabsdeclor)) (simpadd0-dirabsdeclor dirabsdeclor)))
Theorem:
(defthm simpadd0-dirabsdeclor-option-of-dirabsdeclor-option-fix-dirabsdeclor? (equal (simpadd0-dirabsdeclor-option (dirabsdeclor-option-fix dirabsdeclor?)) (simpadd0-dirabsdeclor-option dirabsdeclor?)))
Theorem:
(defthm simpadd0-paramdecl-of-paramdecl-fix-paramdecl (equal (simpadd0-paramdecl (paramdecl-fix paramdecl)) (simpadd0-paramdecl paramdecl)))
Theorem:
(defthm simpadd0-paramdecl-list-of-paramdecl-list-fix-paramdecls (equal (simpadd0-paramdecl-list (paramdecl-list-fix paramdecls)) (simpadd0-paramdecl-list paramdecls)))
Theorem:
(defthm simpadd0-paramdeclor-of-paramdeclor-fix-paramdeclor (equal (simpadd0-paramdeclor (paramdeclor-fix paramdeclor)) (simpadd0-paramdeclor paramdeclor)))
Theorem:
(defthm simpadd0-tyname-of-tyname-fix-tyname (equal (simpadd0-tyname (tyname-fix tyname)) (simpadd0-tyname tyname)))
Theorem:
(defthm simpadd0-strunispec-of-strunispec-fix-strunispec (equal (simpadd0-strunispec (strunispec-fix strunispec)) (simpadd0-strunispec strunispec)))
Theorem:
(defthm simpadd0-structdecl-of-structdecl-fix-structdecl (equal (simpadd0-structdecl (structdecl-fix structdecl)) (simpadd0-structdecl structdecl)))
Theorem:
(defthm simpadd0-structdecl-list-of-structdecl-list-fix-structdecls (equal (simpadd0-structdecl-list (structdecl-list-fix structdecls)) (simpadd0-structdecl-list structdecls)))
Theorem:
(defthm simpadd0-structdeclor-of-structdeclor-fix-structdeclor (equal (simpadd0-structdeclor (structdeclor-fix structdeclor)) (simpadd0-structdeclor structdeclor)))
Theorem:
(defthm simpadd0-structdeclor-list-of-structdeclor-list-fix-structdeclors (equal (simpadd0-structdeclor-list (structdeclor-list-fix structdeclors)) (simpadd0-structdeclor-list structdeclors)))
Theorem:
(defthm simpadd0-enumspec-of-enumspec-fix-enumspec (equal (simpadd0-enumspec (enumspec-fix enumspec)) (simpadd0-enumspec enumspec)))
Theorem:
(defthm simpadd0-enumer-of-enumer-fix-enumer (equal (simpadd0-enumer (enumer-fix enumer)) (simpadd0-enumer enumer)))
Theorem:
(defthm simpadd0-enumer-list-of-enumer-list-fix-enumers (equal (simpadd0-enumer-list (enumer-list-fix enumers)) (simpadd0-enumer-list enumers)))
Theorem:
(defthm simpadd0-statassert-of-statassert-fix-statassert (equal (simpadd0-statassert (statassert-fix statassert)) (simpadd0-statassert statassert)))
Theorem:
(defthm simpadd0-initdeclor-of-initdeclor-fix-initdeclor (equal (simpadd0-initdeclor (initdeclor-fix initdeclor)) (simpadd0-initdeclor initdeclor)))
Theorem:
(defthm simpadd0-initdeclor-list-of-initdeclor-list-fix-initdeclors (equal (simpadd0-initdeclor-list (initdeclor-list-fix initdeclors)) (simpadd0-initdeclor-list initdeclors)))
Theorem:
(defthm simpadd0-decl-of-decl-fix-decl (equal (simpadd0-decl (decl-fix decl)) (simpadd0-decl decl)))
Theorem:
(defthm simpadd0-decl-list-of-decl-list-fix-decls (equal (simpadd0-decl-list (c$::decl-list-fix decls)) (simpadd0-decl-list decls)))
Theorem:
(defthm simpadd0-label-of-label-fix-label (equal (simpadd0-label (label-fix label)) (simpadd0-label label)))
Theorem:
(defthm simpadd0-stmt-of-stmt-fix-stmt (equal (simpadd0-stmt (stmt-fix stmt)) (simpadd0-stmt stmt)))
Theorem:
(defthm simpadd0-block-item-of-block-item-fix-item (equal (simpadd0-block-item (block-item-fix item)) (simpadd0-block-item item)))
Theorem:
(defthm simpadd0-block-item-list-of-block-item-list-fix-items (equal (simpadd0-block-item-list (block-item-list-fix items)) (simpadd0-block-item-list items)))
Theorem:
(defthm simpadd0-expr-expr-equiv-congruence-on-expr (implies (c$::expr-equiv expr expr-equiv) (equal (simpadd0-expr expr) (simpadd0-expr expr-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-expr-list-expr-list-equiv-congruence-on-exprs (implies (c$::expr-list-equiv exprs exprs-equiv) (equal (simpadd0-expr-list exprs) (simpadd0-expr-list exprs-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-expr-option-expr-option-equiv-congruence-on-expr? (implies (c$::expr-option-equiv expr? expr?-equiv) (equal (simpadd0-expr-option expr?) (simpadd0-expr-option expr?-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-const-expr-const-expr-equiv-congruence-on-cexpr (implies (c$::const-expr-equiv cexpr cexpr-equiv) (equal (simpadd0-const-expr cexpr) (simpadd0-const-expr cexpr-equiv))) :rule-classes :congruence)
Theorem:
(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?) (simpadd0-const-expr-option cexpr?-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-genassoc-genassoc-equiv-congruence-on-genassoc (implies (c$::genassoc-equiv genassoc genassoc-equiv) (equal (simpadd0-genassoc genassoc) (simpadd0-genassoc genassoc-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-genassoc-list-genassoc-list-equiv-congruence-on-genassocs (implies (c$::genassoc-list-equiv genassocs genassocs-equiv) (equal (simpadd0-genassoc-list genassocs) (simpadd0-genassoc-list genassocs-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-member-designor-member-designor-equiv-congruence-on-memdes (implies (c$::member-designor-equiv memdes memdes-equiv) (equal (simpadd0-member-designor memdes) (simpadd0-member-designor memdes-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-type-spec-type-spec-equiv-congruence-on-tyspec (implies (c$::type-spec-equiv tyspec tyspec-equiv) (equal (simpadd0-type-spec tyspec) (simpadd0-type-spec tyspec-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-spec/qual-spec/qual-equiv-congruence-on-specqual (implies (c$::spec/qual-equiv specqual specqual-equiv) (equal (simpadd0-spec/qual specqual) (simpadd0-spec/qual specqual-equiv))) :rule-classes :congruence)
Theorem:
(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) (simpadd0-spec/qual-list specquals-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-align-spec-align-spec-equiv-congruence-on-alignspec (implies (c$::align-spec-equiv alignspec alignspec-equiv) (equal (simpadd0-align-spec alignspec) (simpadd0-align-spec alignspec-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-declspec-declspec-equiv-congruence-on-declspec (implies (c$::declspec-equiv declspec declspec-equiv) (equal (simpadd0-declspec declspec) (simpadd0-declspec declspec-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-declspec-list-declspec-list-equiv-congruence-on-declspecs (implies (c$::declspec-list-equiv declspecs declspecs-equiv) (equal (simpadd0-declspec-list declspecs) (simpadd0-declspec-list declspecs-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-initer-initer-equiv-congruence-on-initer (implies (c$::initer-equiv initer initer-equiv) (equal (simpadd0-initer initer) (simpadd0-initer initer-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-initer-option-initer-option-equiv-congruence-on-initer? (implies (c$::initer-option-equiv initer? initer?-equiv) (equal (simpadd0-initer-option initer?) (simpadd0-initer-option initer?-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-desiniter-desiniter-equiv-congruence-on-desiniter (implies (c$::desiniter-equiv desiniter desiniter-equiv) (equal (simpadd0-desiniter desiniter) (simpadd0-desiniter desiniter-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-desiniter-list-desiniter-list-equiv-congruence-on-desiniters (implies (c$::desiniter-list-equiv desiniters desiniters-equiv) (equal (simpadd0-desiniter-list desiniters) (simpadd0-desiniter-list desiniters-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-designor-designor-equiv-congruence-on-designor (implies (c$::designor-equiv designor designor-equiv) (equal (simpadd0-designor designor) (simpadd0-designor designor-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-designor-list-designor-list-equiv-congruence-on-designors (implies (c$::designor-list-equiv designors designors-equiv) (equal (simpadd0-designor-list designors) (simpadd0-designor-list designors-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-declor-declor-equiv-congruence-on-declor (implies (c$::declor-equiv declor declor-equiv) (equal (simpadd0-declor declor) (simpadd0-declor declor-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-declor-option-declor-option-equiv-congruence-on-declor? (implies (c$::declor-option-equiv declor? declor?-equiv) (equal (simpadd0-declor-option declor?) (simpadd0-declor-option declor?-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor (implies (c$::dirdeclor-equiv dirdeclor dirdeclor-equiv) (equal (simpadd0-dirdeclor dirdeclor) (simpadd0-dirdeclor dirdeclor-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-absdeclor-absdeclor-equiv-congruence-on-absdeclor (implies (c$::absdeclor-equiv absdeclor absdeclor-equiv) (equal (simpadd0-absdeclor absdeclor) (simpadd0-absdeclor absdeclor-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-absdeclor-option-absdeclor-option-equiv-congruence-on-absdeclor? (implies (c$::absdeclor-option-equiv absdeclor? absdeclor?-equiv) (equal (simpadd0-absdeclor-option absdeclor?) (simpadd0-absdeclor-option absdeclor?-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor (implies (c$::dirabsdeclor-equiv dirabsdeclor dirabsdeclor-equiv) (equal (simpadd0-dirabsdeclor dirabsdeclor) (simpadd0-dirabsdeclor dirabsdeclor-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-dirabsdeclor-option-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor? (implies (c$::dirabsdeclor-option-equiv dirabsdeclor? dirabsdeclor?-equiv) (equal (simpadd0-dirabsdeclor-option dirabsdeclor?) (simpadd0-dirabsdeclor-option dirabsdeclor?-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-paramdecl-paramdecl-equiv-congruence-on-paramdecl (implies (c$::paramdecl-equiv paramdecl paramdecl-equiv) (equal (simpadd0-paramdecl paramdecl) (simpadd0-paramdecl paramdecl-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-paramdecl-list-paramdecl-list-equiv-congruence-on-paramdecls (implies (c$::paramdecl-list-equiv paramdecls paramdecls-equiv) (equal (simpadd0-paramdecl-list paramdecls) (simpadd0-paramdecl-list paramdecls-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-paramdeclor-paramdeclor-equiv-congruence-on-paramdeclor (implies (c$::paramdeclor-equiv paramdeclor paramdeclor-equiv) (equal (simpadd0-paramdeclor paramdeclor) (simpadd0-paramdeclor paramdeclor-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-tyname-tyname-equiv-congruence-on-tyname (implies (c$::tyname-equiv tyname tyname-equiv) (equal (simpadd0-tyname tyname) (simpadd0-tyname tyname-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-strunispec-strunispec-equiv-congruence-on-strunispec (implies (c$::strunispec-equiv strunispec strunispec-equiv) (equal (simpadd0-strunispec strunispec) (simpadd0-strunispec strunispec-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-structdecl-structdecl-equiv-congruence-on-structdecl (implies (c$::structdecl-equiv structdecl structdecl-equiv) (equal (simpadd0-structdecl structdecl) (simpadd0-structdecl structdecl-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-structdecl-list-structdecl-list-equiv-congruence-on-structdecls (implies (c$::structdecl-list-equiv structdecls structdecls-equiv) (equal (simpadd0-structdecl-list structdecls) (simpadd0-structdecl-list structdecls-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-structdeclor-structdeclor-equiv-congruence-on-structdeclor (implies (c$::structdeclor-equiv structdeclor structdeclor-equiv) (equal (simpadd0-structdeclor structdeclor) (simpadd0-structdeclor structdeclor-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-structdeclor-list-structdeclor-list-equiv-congruence-on-structdeclors (implies (c$::structdeclor-list-equiv structdeclors structdeclors-equiv) (equal (simpadd0-structdeclor-list structdeclors) (simpadd0-structdeclor-list structdeclors-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-enumspec-enumspec-equiv-congruence-on-enumspec (implies (c$::enumspec-equiv enumspec enumspec-equiv) (equal (simpadd0-enumspec enumspec) (simpadd0-enumspec enumspec-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-enumer-enumer-equiv-congruence-on-enumer (implies (c$::enumer-equiv enumer enumer-equiv) (equal (simpadd0-enumer enumer) (simpadd0-enumer enumer-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-enumer-list-enumer-list-equiv-congruence-on-enumers (implies (c$::enumer-list-equiv enumers enumers-equiv) (equal (simpadd0-enumer-list enumers) (simpadd0-enumer-list enumers-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-statassert-statassert-equiv-congruence-on-statassert (implies (c$::statassert-equiv statassert statassert-equiv) (equal (simpadd0-statassert statassert) (simpadd0-statassert statassert-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-initdeclor-initdeclor-equiv-congruence-on-initdeclor (implies (c$::initdeclor-equiv initdeclor initdeclor-equiv) (equal (simpadd0-initdeclor initdeclor) (simpadd0-initdeclor initdeclor-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-initdeclor-list-initdeclor-list-equiv-congruence-on-initdeclors (implies (c$::initdeclor-list-equiv initdeclors initdeclors-equiv) (equal (simpadd0-initdeclor-list initdeclors) (simpadd0-initdeclor-list initdeclors-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-decl-decl-equiv-congruence-on-decl (implies (c$::decl-equiv decl decl-equiv) (equal (simpadd0-decl decl) (simpadd0-decl decl-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-decl-list-decl-list-equiv-congruence-on-decls (implies (c$::decl-list-equiv decls decls-equiv) (equal (simpadd0-decl-list decls) (simpadd0-decl-list decls-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-label-label-equiv-congruence-on-label (implies (c$::label-equiv label label-equiv) (equal (simpadd0-label label) (simpadd0-label label-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-stmt-stmt-equiv-congruence-on-stmt (implies (c$::stmt-equiv stmt stmt-equiv) (equal (simpadd0-stmt stmt) (simpadd0-stmt stmt-equiv))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-block-item-block-item-equiv-congruence-on-item (implies (c$::block-item-equiv item item-equiv) (equal (simpadd0-block-item item) (simpadd0-block-item item-equiv))) :rule-classes :congruence)
Theorem:
(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) (simpadd0-block-item-list items-equiv))) :rule-classes :congruence)
Theorem:
(defthm expr-unambp-of-simpadd0-expr (b* ((?new-expr (simpadd0-expr expr))) (expr-unambp new-expr)))
Theorem:
(defthm expr-list-unambp-of-simpadd0-expr-list (b* ((?new-exprs (simpadd0-expr-list exprs))) (expr-list-unambp new-exprs)))
Theorem:
(defthm expr-option-unambp-of-simpadd0-expr-option (b* ((?new-expr? (simpadd0-expr-option expr?))) (expr-option-unambp new-expr?)))
Theorem:
(defthm const-expr-unambp-of-simpadd0-const-expr (b* ((?new-cexpr (simpadd0-const-expr cexpr))) (const-expr-unambp new-cexpr)))
Theorem:
(defthm const-expr-option-unambp-of-simpadd0-const-expr-option (b* ((?new-cexpr? (simpadd0-const-expr-option cexpr?))) (const-expr-option-unambp new-cexpr?)))
Theorem:
(defthm genassoc-unambp-of-simpadd0-genassoc (b* ((?new-genassoc (simpadd0-genassoc genassoc))) (genassoc-unambp new-genassoc)))
Theorem:
(defthm genassoc-list-unambp-of-simpadd0-genassoc-list (b* ((?new-genassocs (simpadd0-genassoc-list genassocs))) (genassoc-list-unambp new-genassocs)))
Theorem:
(defthm member-designor-unambp-of-simpadd0-member-designor (b* ((?new-memdes (simpadd0-member-designor memdes))) (member-designor-unambp new-memdes)))
Theorem:
(defthm type-spec-unambp-of-simpadd0-type-spec (b* ((?new-tyspec (simpadd0-type-spec tyspec))) (type-spec-unambp new-tyspec)))
Theorem:
(defthm spec/qual-unambp-of-simpadd0-spec/qual (b* ((?new-specqual (simpadd0-spec/qual specqual))) (spec/qual-unambp new-specqual)))
Theorem:
(defthm spec/qual-list-unambp-of-simpadd0-spec/qual-list (b* ((?new-specquals (simpadd0-spec/qual-list specquals))) (spec/qual-list-unambp new-specquals)))
Theorem:
(defthm align-spec-unambp-of-simpadd0-align-spec (b* ((?new-alignspec (simpadd0-align-spec alignspec))) (align-spec-unambp new-alignspec)))
Theorem:
(defthm declspec-unambp-of-simpadd0-declspec (b* ((?new-declspec (simpadd0-declspec declspec))) (declspec-unambp new-declspec)))
Theorem:
(defthm declspec-list-unambp-of-simpadd0-declspec-list (b* ((?new-declspecs (simpadd0-declspec-list declspecs))) (declspec-list-unambp new-declspecs)))
Theorem:
(defthm initer-unambp-of-simpadd0-initer (b* ((?new-initer (simpadd0-initer initer))) (initer-unambp new-initer)))
Theorem:
(defthm initer-option-unambp-of-simpadd0-initer-option (b* ((?new-initer? (simpadd0-initer-option initer?))) (initer-option-unambp new-initer?)))
Theorem:
(defthm desiniter-unambp-of-simpadd0-desiniter (b* ((?new-desiniter (simpadd0-desiniter desiniter))) (desiniter-unambp new-desiniter)))
Theorem:
(defthm desiniter-list-unambp-of-simpadd0-desiniter-list (b* ((?new-desiniters (simpadd0-desiniter-list desiniters))) (desiniter-list-unambp new-desiniters)))
Theorem:
(defthm designor-unambp-of-simpadd0-designor (b* ((?new-designor (simpadd0-designor designor))) (designor-unambp new-designor)))
Theorem:
(defthm designor-list-unambp-of-simpadd0-designor-list (b* ((?new-designors (simpadd0-designor-list designors))) (designor-list-unambp new-designors)))
Theorem:
(defthm declor-unambp-of-simpadd0-declor (b* ((?new-declor (simpadd0-declor declor))) (declor-unambp new-declor)))
Theorem:
(defthm declor-option-unambp-of-simpadd0-declor-option (b* ((?new-declor? (simpadd0-declor-option declor?))) (declor-option-unambp new-declor?)))
Theorem:
(defthm dirdeclor-unambp-of-simpadd0-dirdeclor (b* ((?new-dirdeclor (simpadd0-dirdeclor dirdeclor))) (dirdeclor-unambp new-dirdeclor)))
Theorem:
(defthm absdeclor-unambp-of-simpadd0-absdeclor (b* ((?new-absdeclor (simpadd0-absdeclor absdeclor))) (absdeclor-unambp new-absdeclor)))
Theorem:
(defthm absdeclor-option-unambp-of-simpadd0-absdeclor-option (b* ((?new-absdeclor? (simpadd0-absdeclor-option absdeclor?))) (absdeclor-option-unambp new-absdeclor?)))
Theorem:
(defthm dirabsdeclor-unambp-of-simpadd0-dirabsdeclor (b* ((?new-dirabsdeclor (simpadd0-dirabsdeclor dirabsdeclor))) (dirabsdeclor-unambp new-dirabsdeclor)))
Theorem:
(defthm dirabsdeclor-option-unambp-of-simpadd0-dirabsdeclor-option (b* ((?new-dirabsdeclor? (simpadd0-dirabsdeclor-option dirabsdeclor?))) (dirabsdeclor-option-unambp new-dirabsdeclor?)))
Theorem:
(defthm paramdecl-unambp-of-simpadd0-paramdecl (b* ((?new-paramdecl (simpadd0-paramdecl paramdecl))) (paramdecl-unambp new-paramdecl)))
Theorem:
(defthm paramdecl-list-unambp-of-simpadd0-paramdecl-list (b* ((?new-paramdecls (simpadd0-paramdecl-list paramdecls))) (paramdecl-list-unambp new-paramdecls)))
Theorem:
(defthm paramdeclor-unambp-of-simpadd0-paramdeclor (b* ((?new-paramdeclor (simpadd0-paramdeclor paramdeclor))) (paramdeclor-unambp new-paramdeclor)))
Theorem:
(defthm tyname-unambp-of-simpadd0-tyname (b* ((?new-tyname (simpadd0-tyname tyname))) (tyname-unambp new-tyname)))
Theorem:
(defthm strunispec-unambp-of-simpadd0-strunispec (b* ((?new-strunispec (simpadd0-strunispec strunispec))) (strunispec-unambp new-strunispec)))
Theorem:
(defthm structdecl-unambp-of-simpadd0-structdecl (b* ((?new-structdecl (simpadd0-structdecl structdecl))) (structdecl-unambp new-structdecl)))
Theorem:
(defthm structdecl-list-unambp-of-simpadd0-structdecl-list (b* ((?new-structdecls (simpadd0-structdecl-list structdecls))) (structdecl-list-unambp new-structdecls)))
Theorem:
(defthm structdeclor-unambp-of-simpadd0-structdeclor (b* ((?new-structdeclor (simpadd0-structdeclor structdeclor))) (structdeclor-unambp new-structdeclor)))
Theorem:
(defthm structdeclor-list-unambp-of-simpadd0-structdeclor-list (b* ((?new-structdeclors (simpadd0-structdeclor-list structdeclors))) (structdeclor-list-unambp new-structdeclors)))
Theorem:
(defthm enumspec-unambp-of-simpadd0-enumspec (b* ((?new-enumspec (simpadd0-enumspec enumspec))) (enumspec-unambp new-enumspec)))
Theorem:
(defthm enumer-unambp-of-simpadd0-enumer (b* ((?new-enumer (simpadd0-enumer enumer))) (enumer-unambp new-enumer)))
Theorem:
(defthm enumer-list-unambp-of-simpadd0-enumer-list (b* ((?new-enumers (simpadd0-enumer-list enumers))) (enumer-list-unambp new-enumers)))
Theorem:
(defthm statassert-unambp-of-simpadd0-statassert (b* ((?new-statassert (simpadd0-statassert statassert))) (statassert-unambp new-statassert)))
Theorem:
(defthm initdeclor-unambp-of-simpadd0-initdeclor (b* ((?new-initdeclor (simpadd0-initdeclor initdeclor))) (initdeclor-unambp new-initdeclor)))
Theorem:
(defthm initdeclor-list-unambp-of-simpadd0-initdeclor-list (b* ((?new-initdeclors (simpadd0-initdeclor-list initdeclors))) (initdeclor-list-unambp new-initdeclors)))
Theorem:
(defthm decl-unambp-of-simpadd0-decl (b* ((?new-decl (simpadd0-decl decl))) (decl-unambp new-decl)))
Theorem:
(defthm decl-list-unambp-of-simpadd0-decl-list (b* ((?new-decls (simpadd0-decl-list decls))) (decl-list-unambp new-decls)))
Theorem:
(defthm label-unambp-of-simpadd0-label (b* ((?new-label (simpadd0-label label))) (label-unambp new-label)))
Theorem:
(defthm stmt-unambp-of-simpadd0-stmt (b* ((?new-stmt (simpadd0-stmt stmt))) (stmt-unambp new-stmt)))
Theorem:
(defthm block-item-unambp-of-simpadd0-block-item (b* ((?new-item (simpadd0-block-item item))) (block-item-unambp new-item)))
Theorem:
(defthm block-item-list-unambp-of-simpadd0-block-item-list (b* ((?new-items (simpadd0-block-item-list items))) (block-item-list-unambp new-items)))