Disambiguate expressions, declarations, and related artifacts.
In general, to disambiguate a construct, first we recursively disambiguate its sub-constructs, then we either join them into an updated construct, or perform a disambiguation of the construct itself if needed.
In general, the disambiguation of a construct may involve the extension of the disambiguation table. For instance, the mere occurrence of an enumeration specifier in the type name that is part of a cast expression extends the disambiguation table with enumeration constants.
Function:
(defun dimb-expr (expr table) (declare (xargs :guard (and (exprp expr) (dimb-tablep table)))) (let ((__function__ 'dimb-expr)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-dimb-table))) (expr-case expr :ident (b* ((kind (dimb-lookup-ident expr.unwrap table)) ((unless kind) (reterr (msg "The identifier ~x0 is used as an expression ~ but is not in scope." expr.unwrap)))) (dimb-kind-case kind :typedef (reterr (msg "The identifier ~x0 denotes a typedef ~ but it is used as an expression." expr.unwrap)) :objfun (retok (expr-fix expr) (dimb-table-fix table)) :enumconst (retok (expr-const (const-enum expr.unwrap)) (dimb-table-fix table)))) :const (retok (expr-fix expr) (dimb-table-fix table)) :string (retok (expr-fix expr) (dimb-table-fix table)) :paren (b* (((erp new-expr table) (dimb-expr expr.unwrap table))) (retok (expr-paren new-expr) table)) :gensel (b* (((erp new-control table) (dimb-expr expr.control table)) ((erp new-assocs table) (dimb-genassoc-list expr.assocs table))) (retok (make-expr-gensel :control new-control :assocs new-assocs) table)) :arrsub (b* (((erp new-arg1 table) (dimb-expr expr.arg1 table)) ((erp new-arg2 table) (dimb-expr expr.arg2 table))) (retok (make-expr-arrsub :arg1 new-arg1 :arg2 new-arg2) table)) :funcall (b* (((erp new-fun table) (dimb-expr expr.fun table)) ((erp new-args table) (dimb-expr-list expr.args table))) (retok (make-expr-funcall :fun new-fun :args new-args) table)) :member (b* (((erp new-arg table) (dimb-expr expr.arg table))) (retok (make-expr-member :arg new-arg :name expr.name) table)) :memberp (b* (((erp new-arg table) (dimb-expr expr.arg table))) (retok (make-expr-memberp :arg new-arg :name expr.name) (dimb-table-fix table))) :complit (b* (((erp new-type table) (dimb-tyname expr.type table)) ((erp new-elems table) (dimb-desiniter-list expr.elems table))) (retok (make-expr-complit :type new-type :elems new-elems :final-comma expr.final-comma) table)) :unary (b* (((erp new-arg table) (dimb-expr expr.arg table))) (retok (make-expr-unary :op expr.op :arg new-arg) table)) :sizeof (b* (((erp new-tyname table) (dimb-tyname expr.type table))) (retok (expr-sizeof new-tyname) table)) :sizeof-ambig (b* (((erp expr-or-tyname table) (dimb-amb-expr/tyname expr.expr/tyname table))) (expr/tyname-case expr-or-tyname :expr (retok (make-expr-unary :op (unop-sizeof) :arg expr-or-tyname.unwrap) table) :tyname (retok (expr-sizeof expr-or-tyname.unwrap) table))) :alignof (b* (((erp new-tyname table) (dimb-tyname expr.type table))) (retok (make-expr-alignof :type new-tyname :uscores expr.uscores) table)) :cast (b* (((erp new-type table) (dimb-tyname expr.type table)) ((erp new-arg table) (dimb-expr expr.arg table))) (retok (make-expr-cast :type new-type :arg new-arg) table)) :binary (b* (((erp new-arg1 table) (dimb-expr expr.arg1 table)) ((erp new-arg2 table) (dimb-expr expr.arg2 table))) (retok (make-expr-binary :op expr.op :arg1 new-arg1 :arg2 new-arg2) table)) :cond (b* (((erp new-test table) (dimb-expr expr.test table)) ((erp new-then table) (dimb-expr expr.then table)) ((erp new-else table) (dimb-expr expr.else table))) (retok (make-expr-cond :test new-test :then new-then :else new-else) table)) :comma (b* (((erp new-first table) (dimb-expr expr.first table)) ((erp new-next table) (dimb-expr expr.next table))) (retok (make-expr-comma :first new-first :next new-next) table)) :cast/call-ambig (b* (((erp expr/tyname table) (dimb-amb-expr/tyname expr.type/fun table)) ((erp new-arg/rest table) (dimb-expr expr.arg/rest table))) (expr/tyname-case expr/tyname :tyname (retok (dimb-cast/call-to-cast (expr/tyname-tyname->unwrap expr/tyname) expr.inc/dec new-arg/rest) table) :expr (retok (dimb-cast/call-to-call (expr/tyname-expr->unwrap expr/tyname) expr.inc/dec new-arg/rest) table))) :cast/mul-ambig (b* (((erp expr/tyname table) (dimb-amb-expr/tyname expr.type/arg1 table)) ((erp new-arg/arg2 table) (dimb-expr expr.arg/arg2 table))) (expr/tyname-case expr/tyname :tyname (retok (dimb-cast/mul-to-cast (expr/tyname-tyname->unwrap expr/tyname) expr.inc/dec new-arg/arg2) table) :expr (retok (dimb-cast/mul-to-mul (expr/tyname-expr->unwrap expr/tyname) expr.inc/dec new-arg/arg2) table))) :cast/add-ambig (b* (((erp expr/tyname table) (dimb-amb-expr/tyname expr.type/arg1 table)) ((erp new-arg/arg2 table) (dimb-expr expr.arg/arg2 table))) (expr/tyname-case expr/tyname :tyname (retok (dimb-cast/addsub-to-cast (expr/tyname-tyname->unwrap expr/tyname) expr.inc/dec new-arg/arg2 (unop-plus)) table) :expr (retok (dimb-cast/addsub-to-addsub (expr/tyname-expr->unwrap expr/tyname) expr.inc/dec new-arg/arg2 (binop-add)) table))) :cast/sub-ambig (b* (((erp expr/tyname table) (dimb-amb-expr/tyname expr.type/arg1 table)) ((erp new-arg/arg2 table) (dimb-expr expr.arg/arg2 table))) (expr/tyname-case expr/tyname :tyname (retok (dimb-cast/addsub-to-cast (expr/tyname-tyname->unwrap expr/tyname) expr.inc/dec new-arg/arg2 (unop-minus)) table) :expr (retok (dimb-cast/addsub-to-addsub (expr/tyname-expr->unwrap expr/tyname) expr.inc/dec new-arg/arg2 (binop-sub)) table))) :cast/and-ambig (b* (((erp expr/tyname table) (dimb-amb-expr/tyname expr.type/arg1 table)) ((erp new-arg/arg2 table) (dimb-expr expr.arg/arg2 table))) (expr/tyname-case expr/tyname :tyname (retok (dimb-cast/and-to-cast (expr/tyname-tyname->unwrap expr/tyname) expr.inc/dec new-arg/arg2) table) :expr (retok (dimb-cast/and-to-and (expr/tyname-expr->unwrap expr/tyname) expr.inc/dec new-arg/arg2) table)))))))
Function:
(defun dimb-expr-list (exprs table) (declare (xargs :guard (and (expr-listp exprs) (dimb-tablep table)))) (let ((__function__ 'dimb-expr-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp exprs)) (retok nil (dimb-table-fix table))) ((erp new-expr table) (dimb-expr (car exprs) table)) ((erp new-exprs table) (dimb-expr-list (cdr exprs) table))) (retok (cons new-expr new-exprs) table))))
Function:
(defun dimb-expr-option (expr? table) (declare (xargs :guard (and (expr-optionp expr?) (dimb-tablep table)))) (let ((__function__ 'dimb-expr-option)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table))) (expr-option-case expr? :some (dimb-expr expr?.val table) :none (retok nil (dimb-table-fix table))))))
Function:
(defun dimb-const-expr (cexpr table) (declare (xargs :guard (and (const-exprp cexpr) (dimb-tablep table)))) (let ((__function__ 'dimb-const-expr)) (declare (ignorable __function__)) (b* (((reterr) (irr-const-expr) (irr-dimb-table)) ((erp new-expr table) (dimb-expr (const-expr->unwrap cexpr) table))) (retok (const-expr new-expr) table))))
Function:
(defun dimb-const-expr-option (cexpr? table) (declare (xargs :guard (and (const-expr-optionp cexpr?) (dimb-tablep table)))) (let ((__function__ 'dimb-const-expr-option)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table))) (const-expr-option-case cexpr? :some (dimb-const-expr cexpr?.val table) :none (retok nil (dimb-table-fix table))))))
Function:
(defun dimb-genassoc (assoc table) (declare (xargs :guard (and (genassocp assoc) (dimb-tablep table)))) (let ((__function__ 'dimb-genassoc)) (declare (ignorable __function__)) (b* (((reterr) (irr-genassoc) (irr-dimb-table))) (genassoc-case assoc :type (b* (((erp new-tyname table) (dimb-tyname assoc.type table)) ((erp new-expr table) (dimb-expr assoc.expr table))) (retok (make-genassoc-type :type new-tyname :expr new-expr) table)) :default (b* (((erp new-expr table) (dimb-expr assoc.expr table))) (retok (genassoc-default new-expr) table))))))
Function:
(defun dimb-genassoc-list (assocs table) (declare (xargs :guard (and (genassoc-listp assocs) (dimb-tablep table)))) (let ((__function__ 'dimb-genassoc-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp assocs)) (retok nil (dimb-table-fix table))) ((erp new-assoc table) (dimb-genassoc (car assocs) table)) ((erp new-assocs table) (dimb-genassoc-list (cdr assocs) table))) (retok (cons new-assoc new-assocs) table))))
Function:
(defun dimb-type-spec (tyspec table) (declare (xargs :guard (and (type-specp tyspec) (dimb-tablep table)))) (let ((__function__ 'dimb-type-spec)) (declare (ignorable __function__)) (b* (((reterr) (irr-type-spec) (irr-dimb-table))) (type-spec-case tyspec :void (retok (type-spec-void) (dimb-table-fix table)) :char (retok (type-spec-char) (dimb-table-fix table)) :short (retok (type-spec-short) (dimb-table-fix table)) :int (retok (type-spec-int) (dimb-table-fix table)) :long (retok (type-spec-long) (dimb-table-fix table)) :float (retok (type-spec-float) (dimb-table-fix table)) :double (retok (type-spec-double) (dimb-table-fix table)) :signed (retok (type-spec-signed tyspec.uscores) (dimb-table-fix table)) :unsigned (retok (type-spec-unsigned) (dimb-table-fix table)) :bool (retok (type-spec-bool) (dimb-table-fix table)) :complex (retok (type-spec-complex) (dimb-table-fix table)) :atomic (b* (((erp new-type table) (dimb-tyname tyspec.type table))) (retok (type-spec-atomic new-type) table)) :struct (b* (((erp new-strunispec table) (dimb-strunispec tyspec.unwrap table))) (retok (type-spec-struct new-strunispec) table)) :union (b* (((erp new-strunispec table) (dimb-strunispec tyspec.unwrap table))) (retok (type-spec-union new-strunispec) table)) :enum (b* (((erp new-enumspec table) (dimb-enumspec tyspec.unwrap table))) (retok (type-spec-enum new-enumspec) table)) :typedef (b* ((kind (dimb-lookup-ident tyspec.name table)) ((unless kind) (reterr (msg "The identifier ~x0 is used as a type specifier ~ but it is not in scope." tyspec.name)))) (dimb-kind-case kind :typedef (retok (type-spec-typedef tyspec.name) (dimb-table-fix table)) :objfun (reterr (msg "The identifier ~x0 denotes ~ an object or function ~ but it is used as a typedef name." tyspec.name)) :enumconst (reterr (msg "The identifier ~x0 denotes ~ an enumeration constant ~ but it is used as a typedef name." tyspec.name)))) :int128 (retok (type-spec-int128) (dimb-table-fix table)) :float128 (retok (type-spec-float128) (dimb-table-fix table)) :builtin-va-list (retok (type-spec-builtin-va-list) (dimb-table-fix table)) :typeof-expr (b* (((erp new-expr table) (dimb-expr tyspec.expr table))) (retok (make-type-spec-typeof-expr :expr new-expr :uscores tyspec.uscores) table)) :typeof-type (b* (((erp new-tyname table) (dimb-tyname tyspec.type table))) (retok (make-type-spec-typeof-type :type new-tyname :uscores tyspec.uscores) table)) :typeof-ambig (b* (((erp expr/tyname table) (dimb-amb-expr/tyname tyspec.expr/type table))) (expr/tyname-case expr/tyname :expr (retok (make-type-spec-typeof-expr :expr expr/tyname.unwrap :uscores tyspec.uscores) table) :tyname (retok (make-type-spec-typeof-type :type expr/tyname.unwrap :uscores tyspec.uscores) table)))))))
Function:
(defun dimb-spec/qual (specqual table) (declare (xargs :guard (and (spec/qual-p specqual) (dimb-tablep table)))) (let ((__function__ 'dimb-spec/qual)) (declare (ignorable __function__)) (b* (((reterr) (irr-spec/qual) (irr-dimb-table))) (spec/qual-case specqual :tyspec (b* (((erp new-tyspec table) (dimb-type-spec specqual.unwrap table))) (retok (spec/qual-tyspec new-tyspec) table)) :tyqual (retok (spec/qual-tyqual specqual.unwrap) (dimb-table-fix table)) :align (b* (((erp new-alignspec table) (dimb-align-spec specqual.unwrap table))) (retok (spec/qual-align new-alignspec) table)) :attrib (retok (spec/qual-attrib specqual.unwrap) (dimb-table-fix table))))))
Function:
(defun dimb-spec/qual-list (specquals table) (declare (xargs :guard (and (spec/qual-listp specquals) (dimb-tablep table)))) (let ((__function__ 'dimb-spec/qual-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp specquals)) (retok nil (dimb-table-fix table))) ((erp new-specqual table) (dimb-spec/qual (car specquals) table)) ((erp new-specquals table) (dimb-spec/qual-list (cdr specquals) table))) (retok (cons new-specqual new-specquals) table))))
Function:
(defun dimb-align-spec (alignspec table) (declare (xargs :guard (and (align-specp alignspec) (dimb-tablep table)))) (let ((__function__ 'dimb-align-spec)) (declare (ignorable __function__)) (b* (((reterr) (irr-align-spec) (irr-dimb-table))) (align-spec-case alignspec :alignas-type (b* (((erp new-type table) (dimb-tyname alignspec.type table))) (retok (align-spec-alignas-type new-type) table)) :alignas-expr (b* (((erp new-arg table) (dimb-const-expr alignspec.arg table))) (retok (align-spec-alignas-expr new-arg) table)) :alignas-ambig (b* (((erp expr/tyname table) (dimb-amb-expr/tyname alignspec.type/arg table))) (expr/tyname-case expr/tyname :expr (retok (align-spec-alignas-expr (const-expr expr/tyname.unwrap)) table) :tyname (retok (align-spec-alignas-type expr/tyname.unwrap) table)))))))
Function:
(defun dimb-declspec (declspec kind table) (declare (xargs :guard (and (declspecp declspec) (dimb-kindp kind) (dimb-tablep table)))) (let ((__function__ 'dimb-declspec)) (declare (ignorable __function__)) (b* (((reterr) (irr-declspec) (irr-dimb-kind) (irr-dimb-table))) (declspec-case declspec :stocla (if (stor-spec-case declspec.unwrap :typedef) (retok (declspec-fix declspec) (dimb-kind-typedef) (dimb-table-fix table)) (retok (declspec-fix declspec) (dimb-kind-fix kind) (dimb-table-fix table))) :tyspec (b* (((erp new-tyspec table) (dimb-type-spec declspec.unwrap table))) (retok (declspec-tyspec new-tyspec) (dimb-kind-fix kind) (dimb-table-fix table))) :tyqual (retok (declspec-fix declspec) (dimb-kind-fix kind) (dimb-table-fix table)) :funspec (retok (declspec-fix declspec) (dimb-kind-fix kind) (dimb-table-fix table)) :align (b* (((erp new-alignspec table) (dimb-align-spec declspec.unwrap table))) (retok (declspec-align new-alignspec) (dimb-kind-fix kind) table)) :attrib (retok (declspec-fix declspec) (dimb-kind-fix kind) (dimb-table-fix table))))))
Function:
(defun dimb-declspec-list (declspecs kind table) (declare (xargs :guard (and (declspec-listp declspecs) (dimb-kindp kind) (dimb-tablep table)))) (let ((__function__ 'dimb-declspec-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-kind) (irr-dimb-table)) ((when (endp declspecs)) (retok nil (dimb-kind-fix kind) (dimb-table-fix table))) ((erp new-declspec kind table) (dimb-declspec (car declspecs) kind table)) ((erp new-declspecs kind table) (dimb-declspec-list (cdr declspecs) kind table))) (retok (cons new-declspec new-declspecs) kind table))))
Function:
(defun dimb-initer (initer table) (declare (xargs :guard (and (initerp initer) (dimb-tablep table)))) (let ((__function__ 'dimb-initer)) (declare (ignorable __function__)) (b* (((reterr) (irr-initer) (irr-dimb-table))) (initer-case initer :single (b* (((erp new-expr table) (dimb-expr initer.expr table))) (retok (initer-single new-expr) table)) :list (b* (((erp new-elems table) (dimb-desiniter-list initer.elems table))) (retok (make-initer-list :elems new-elems :final-comma initer.final-comma) table))))))
Function:
(defun dimb-initer-option (initer? table) (declare (xargs :guard (and (initer-optionp initer?) (dimb-tablep table)))) (let ((__function__ 'dimb-initer-option)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table))) (initer-option-case initer? :some (dimb-initer initer?.val table) :none (retok nil (dimb-table-fix table))))))
Function:
(defun dimb-desiniter (desiniter table) (declare (xargs :guard (and (desiniterp desiniter) (dimb-tablep table)))) (let ((__function__ 'dimb-desiniter)) (declare (ignorable __function__)) (b* (((reterr) (irr-desiniter) (irr-dimb-table)) ((desiniter desiniter) desiniter) ((erp new-designs table) (dimb-designor-list desiniter.design table)) ((erp new-initer table) (dimb-initer desiniter.init table))) (retok (make-desiniter :design new-designs :init new-initer) table))))
Function:
(defun dimb-desiniter-list (desiniters table) (declare (xargs :guard (and (desiniter-listp desiniters) (dimb-tablep table)))) (let ((__function__ 'dimb-desiniter-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp desiniters)) (retok nil (dimb-table-fix table))) ((erp new-desiniter table) (dimb-desiniter (car desiniters) table)) ((erp new-desiniters table) (dimb-desiniter-list (cdr desiniters) table))) (retok (cons new-desiniter new-desiniters) table))))
Function:
(defun dimb-designor (design table) (declare (xargs :guard (and (designorp design) (dimb-tablep table)))) (let ((__function__ 'dimb-designor)) (declare (ignorable __function__)) (b* (((reterr) (irr-designor) (irr-dimb-table))) (designor-case design :sub (b* (((erp new-index table) (dimb-const-expr design.index table))) (retok (designor-sub new-index) table)) :dot (retok (designor-dot design.name) (dimb-table-fix table))))))
Function:
(defun dimb-designor-list (designs table) (declare (xargs :guard (and (designor-listp designs) (dimb-tablep table)))) (let ((__function__ 'dimb-designor-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp designs)) (retok nil (dimb-table-fix table))) ((erp new-design table) (dimb-designor (car designs) table)) ((erp new-designs table) (dimb-designor-list (cdr designs) table))) (retok (cons new-design new-designs) table))))
Function:
(defun dimb-declor (declor fundefp table) (declare (xargs :guard (and (declorp declor) (booleanp fundefp) (dimb-tablep table)))) (let ((__function__ 'dimb-declor)) (declare (ignorable __function__)) (b* (((reterr) (irr-declor) (irr-ident) (irr-dimb-table)) ((declor declor) declor) ((erp new-dirdeclor ident table) (dimb-dirdeclor declor.decl fundefp table))) (retok (make-declor :pointers declor.pointers :decl new-dirdeclor) ident table))))
Function:
(defun dimb-declor-option (declor? table) (declare (xargs :guard (and (declor-optionp declor?) (dimb-tablep table)))) (let ((__function__ 'dimb-declor-option)) (declare (ignorable __function__)) (b* (((reterr) nil nil (irr-dimb-table))) (declor-option-case declor? :some (dimb-declor declor?.val nil table) :none (retok nil nil (dimb-table-fix table))))))
Function:
(defun dimb-dirdeclor (dirdeclor fundefp table) (declare (xargs :guard (and (dirdeclorp dirdeclor) (booleanp fundefp) (dimb-tablep table)))) (let ((__function__ 'dimb-dirdeclor)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirdeclor) (irr-ident) (irr-dimb-table))) (dirdeclor-case dirdeclor :ident (retok (dirdeclor-fix dirdeclor) dirdeclor.unwrap (dimb-table-fix table)) :paren (b* (((erp new-declor ident table) (dimb-declor dirdeclor.unwrap fundefp table))) (retok (dirdeclor-paren new-declor) ident table)) :array (b* (((erp new-dirdeclor ident table) (dimb-dirdeclor dirdeclor.decl fundefp table)) ((erp new-expr? table) (dimb-expr-option dirdeclor.expr? table))) (retok (make-dirdeclor-array :decl new-dirdeclor :tyquals dirdeclor.tyquals :expr? new-expr?) ident table)) :array-static1 (b* (((erp new-dirdeclor ident table) (dimb-dirdeclor dirdeclor.decl fundefp table)) ((erp new-expr table) (dimb-expr dirdeclor.expr table))) (retok (make-dirdeclor-array-static1 :decl new-dirdeclor :tyquals dirdeclor.tyquals :expr new-expr) ident table)) :array-static2 (b* (((erp new-dirdeclor ident table) (dimb-dirdeclor dirdeclor.decl fundefp table)) ((erp new-expr table) (dimb-expr dirdeclor.expr table))) (retok (make-dirdeclor-array-static2 :decl new-dirdeclor :tyquals dirdeclor.tyquals :expr new-expr) ident table)) :array-star (b* (((erp new-dirdeclor ident table) (dimb-dirdeclor dirdeclor.decl fundefp table))) (retok (make-dirdeclor-array-star :decl new-dirdeclor :tyquals dirdeclor.tyquals) ident table)) :function-params (b* (((erp new-dirdeclor ident table) (dimb-dirdeclor dirdeclor.decl fundefp table)) ((mv yes/no names) (dimb-params-to-names dirdeclor.params fundefp table)) ((when yes/no) (retok (make-dirdeclor-function-names :decl new-dirdeclor :names names) ident (if fundefp (dimb-push-scope table) table))) (table (dimb-push-scope table)) ((erp new-params table) (dimb-paramdecl-list dirdeclor.params table)) (table (if fundefp table (dimb-pop-scope table)) )) (retok (make-dirdeclor-function-params :decl new-dirdeclor :params new-params :ellipsis dirdeclor.ellipsis) ident table)) :function-names (b* (((erp new-dirdeclor ident table) (dimb-dirdeclor dirdeclor.decl fundefp table))) (retok (make-dirdeclor-function-names :decl new-dirdeclor :names dirdeclor.names) ident (if fundefp (dimb-push-scope table) table)))))))
Function:
(defun dimb-absdeclor (absdeclor table) (declare (xargs :guard (and (absdeclorp absdeclor) (dimb-tablep table)))) (let ((__function__ 'dimb-absdeclor)) (declare (ignorable __function__)) (b* (((reterr) (irr-absdeclor) (irr-dimb-table)) ((absdeclor absdeclor) absdeclor) ((erp new-decl? table) (dimb-dirabsdeclor-option absdeclor.decl? table))) (retok (make-absdeclor :pointers absdeclor.pointers :decl? new-decl?) table))))
Function:
(defun dimb-absdeclor-option (absdeclor? table) (declare (xargs :guard (and (absdeclor-optionp absdeclor?) (dimb-tablep table)))) (let ((__function__ 'dimb-absdeclor-option)) (declare (ignorable __function__)) (b* (((reterr) nil nil (irr-dimb-table))) (absdeclor-option-case absdeclor? :some (dimb-absdeclor absdeclor?.val table) :none (retok nil (dimb-table-fix table))))))
Function:
(defun dimb-dirabsdeclor (dirabsdeclor table) (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor) (dimb-tablep table)))) (let ((__function__ 'dimb-dirabsdeclor)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirabsdeclor) (irr-dimb-table))) (dirabsdeclor-case dirabsdeclor :dummy-base (prog2$ (raise "Internal error: dummy base case of direct abstract declarator.") (reterr t)) :paren (b* (((erp new-absdeclor table) (dimb-absdeclor dirabsdeclor.unwrap table))) (retok (dirabsdeclor-paren new-absdeclor) table)) :array (b* (((erp new-decl? table) (dimb-dirabsdeclor-option dirabsdeclor.decl? table)) ((erp new-expr? table) (dimb-expr-option dirabsdeclor.expr? table))) (retok (make-dirabsdeclor-array :decl? new-decl? :tyquals dirabsdeclor.tyquals :expr? new-expr?) table)) :array-static1 (b* (((erp new-decl? table) (dimb-dirabsdeclor-option dirabsdeclor.decl? table)) ((erp new-expr table) (dimb-expr dirabsdeclor.expr table))) (retok (make-dirabsdeclor-array-static1 :decl? new-decl? :tyquals dirabsdeclor.tyquals :expr new-expr) table)) :array-static2 (b* (((erp new-decl? table) (dimb-dirabsdeclor-option dirabsdeclor.decl? table)) ((erp new-expr table) (dimb-expr dirabsdeclor.expr table))) (retok (make-dirabsdeclor-array-static2 :decl? new-decl? :tyquals dirabsdeclor.tyquals :expr new-expr) table)) :array-star (b* (((erp new-decl? table) (dimb-dirabsdeclor-option dirabsdeclor.decl? table))) (retok (dirabsdeclor-array-star new-decl?) table)) :function (b* (((erp new-decl? table) (dimb-dirabsdeclor-option dirabsdeclor.decl? table)) (table (dimb-push-scope table)) ((erp new-params table) (dimb-paramdecl-list dirabsdeclor.params table)) (table (dimb-pop-scope table))) (retok (make-dirabsdeclor-function :decl? new-decl? :params new-params :ellipsis dirabsdeclor.ellipsis) table))))))
Function:
(defun dimb-dirabsdeclor-option (dirabsdeclor? table) (declare (xargs :guard (and (dirabsdeclor-optionp dirabsdeclor?) (dimb-tablep table)))) (let ((__function__ 'dimb-dirabsdeclor-option)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table))) (dirabsdeclor-option-case dirabsdeclor? :some (dimb-dirabsdeclor dirabsdeclor?.val table) :none (retok nil (dimb-table-fix table))))))
Function:
(defun dimb-paramdecl (paramdecl table) (declare (xargs :guard (and (paramdeclp paramdecl) (dimb-tablep table)))) (let ((__function__ 'dimb-paramdecl)) (declare (ignorable __function__)) (b* (((reterr) (irr-paramdecl) (irr-dimb-table)) ((paramdecl paramdecl) paramdecl) ((erp new-spec & table) (dimb-declspec-list paramdecl.spec (dimb-kind-objfun) table)) ((erp new-decl table) (dimb-paramdeclor paramdecl.decl table))) (retok (make-paramdecl :spec new-spec :decl new-decl) table))))
Function:
(defun dimb-paramdecl-list (paramdecls table) (declare (xargs :guard (and (paramdecl-listp paramdecls) (dimb-tablep table)))) (let ((__function__ 'dimb-paramdecl-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp paramdecls)) (retok nil (dimb-table-fix table))) ((erp new-paramdecl table) (dimb-paramdecl (car paramdecls) table)) ((erp new-paramdecls table) (dimb-paramdecl-list (cdr paramdecls) table))) (retok (cons new-paramdecl new-paramdecls) table))))
Function:
(defun dimb-paramdeclor (paramdeclor table) (declare (xargs :guard (and (paramdeclorp paramdeclor) (dimb-tablep table)))) (let ((__function__ 'dimb-paramdeclor)) (declare (ignorable __function__)) (b* (((reterr) (irr-paramdeclor) (irr-dimb-table))) (paramdeclor-case paramdeclor :declor (b* (((erp new-declor ident table) (dimb-declor paramdeclor.unwrap nil table)) (table (dimb-add-ident ident (dimb-kind-objfun) table) )) (retok (paramdeclor-declor new-declor) table)) :absdeclor (b* (((erp new-absdeclor table) (dimb-absdeclor paramdeclor.unwrap table))) (retok (paramdeclor-absdeclor new-absdeclor) (dimb-table-fix table))) :none (retok (paramdeclor-none) (dimb-table-fix table)) :ambig (b* (((erp declor/absdeclor ident? table) (dimb-amb-declor/absdeclor paramdeclor.unwrap table))) (declor/absdeclor-case declor/absdeclor :declor (b* (((unless ident?) (raise "Internal error: declarator without identifier.") (reterr t)) (table (dimb-add-ident ident? (dimb-kind-objfun) table) )) (retok (paramdeclor-declor declor/absdeclor.unwrap) table)) :absdeclor (retok (paramdeclor-absdeclor declor/absdeclor.unwrap) (dimb-table-fix table))))))))
Function:
(defun dimb-tyname (tyname table) (declare (xargs :guard (and (tynamep tyname) (dimb-tablep table)))) (let ((__function__ 'dimb-tyname)) (declare (ignorable __function__)) (b* (((reterr) (irr-tyname) (irr-dimb-table)) ((tyname tyname) tyname) ((erp new-specqual table) (dimb-spec/qual-list tyname.specqual table)) ((erp new-decl? table) (dimb-absdeclor-option tyname.decl? table))) (retok (make-tyname :specqual new-specqual :decl? new-decl?) table))))
Function:
(defun dimb-strunispec (strunispec table) (declare (xargs :guard (and (strunispecp strunispec) (dimb-tablep table)))) (let ((__function__ 'dimb-strunispec)) (declare (ignorable __function__)) (b* (((reterr) (irr-strunispec) (irr-dimb-table)) ((strunispec strunispec) strunispec) ((erp new-members table) (dimb-structdecl-list strunispec.members table))) (retok (make-strunispec :name strunispec.name :members new-members) table))))
Function:
(defun dimb-structdecl (structdecl table) (declare (xargs :guard (and (structdeclp structdecl) (dimb-tablep table)))) (let ((__function__ 'dimb-structdecl)) (declare (ignorable __function__)) (b* (((reterr) (irr-structdecl) (irr-dimb-table))) (structdecl-case structdecl :member (b* (((erp new-specqual table) (dimb-spec/qual-list structdecl.specqual table)) ((erp new-declor table) (dimb-structdeclor-list structdecl.declor table))) (retok (make-structdecl-member :extension structdecl.extension :specqual new-specqual :declor new-declor :attrib structdecl.attrib) table)) :statassert (b* (((erp new-statassert table) (dimb-statassert structdecl.unwrap table))) (retok (structdecl-statassert new-statassert) table))))))
Function:
(defun dimb-structdecl-list (structdecls table) (declare (xargs :guard (and (structdecl-listp structdecls) (dimb-tablep table)))) (let ((__function__ 'dimb-structdecl-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp structdecls)) (retok nil (dimb-table-fix table))) ((erp new-structdecl table) (dimb-structdecl (car structdecls) table)) ((erp new-structdecls table) (dimb-structdecl-list (cdr structdecls) table))) (retok (cons new-structdecl new-structdecls) table))))
Function:
(defun dimb-structdeclor (structdeclor table) (declare (xargs :guard (and (structdeclorp structdeclor) (dimb-tablep table)))) (let ((__function__ 'dimb-structdeclor)) (declare (ignorable __function__)) (b* (((reterr) (irr-structdeclor) (irr-dimb-table)) ((structdeclor structdeclor) structdeclor) ((erp new-declor? & table) (dimb-declor-option structdeclor.declor? table)) ((erp new-expr? table) (dimb-const-expr-option structdeclor.expr? table))) (retok (make-structdeclor :declor? new-declor? :expr? new-expr?) table))))
Function:
(defun dimb-structdeclor-list (structdeclors table) (declare (xargs :guard (and (structdeclor-listp structdeclors) (dimb-tablep table)))) (let ((__function__ 'dimb-structdeclor-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp structdeclors)) (retok nil (dimb-table-fix table))) ((erp new-structdeclor table) (dimb-structdeclor (car structdeclors) table)) ((erp new-structdeclors table) (dimb-structdeclor-list (cdr structdeclors) table))) (retok (cons new-structdeclor new-structdeclors) table))))
Function:
(defun dimb-enumspec (enumspec table) (declare (xargs :guard (and (enumspecp enumspec) (dimb-tablep table)))) (let ((__function__ 'dimb-enumspec)) (declare (ignorable __function__)) (b* (((reterr) (irr-enumspec) (irr-dimb-table)) ((enumspec enumspec) enumspec) ((erp new-list table) (dimb-enumer-list enumspec.list table))) (retok (make-enumspec :name enumspec.name :list new-list :final-comma enumspec.final-comma) table))))
Function:
(defun dimb-enumer (enumer table) (declare (xargs :guard (and (enumerp enumer) (dimb-tablep table)))) (let ((__function__ 'dimb-enumer)) (declare (ignorable __function__)) (b* (((reterr) (irr-enumer) (irr-dimb-table)) ((enumer enumer) enumer) ((erp new-value table) (dimb-const-expr-option enumer.value table)) (table (dimb-add-ident enumer.name (dimb-kind-enumconst) table) )) (retok (make-enumer :name enumer.name :value new-value) table))))
Function:
(defun dimb-enumer-list (enumers table) (declare (xargs :guard (and (enumer-listp enumers) (dimb-tablep table)))) (let ((__function__ 'dimb-enumer-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp enumers)) (retok nil (dimb-table-fix table))) ((erp new-enumer table) (dimb-enumer (car enumers) table)) ((erp new-enumers table) (dimb-enumer-list (cdr enumers) table))) (retok (cons new-enumer new-enumers) table))))
Function:
(defun dimb-statassert (statassert table) (declare (xargs :guard (and (statassertp statassert) (dimb-tablep table)))) (let ((__function__ 'dimb-statassert)) (declare (ignorable __function__)) (b* (((reterr) (irr-statassert) (irr-dimb-table)) ((statassert statassert) statassert) ((erp new-test table) (dimb-const-expr statassert.test table))) (retok (make-statassert :test new-test :message statassert.message) table))))
Function:
(defun dimb-amb-expr/tyname (expr/tyname table) (declare (xargs :guard (and (amb-expr/tyname-p expr/tyname) (dimb-tablep table)))) (let ((__function__ 'dimb-amb-expr/tyname)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr/tyname) (irr-dimb-table)) ((amb-expr/tyname expr/tyname) expr/tyname) ((mv erp-expr new-expr table-expr) (dimb-expr expr/tyname.expr table)) ((mv erp-tyname new-tyname table-tyname) (dimb-tyname expr/tyname.tyname table))) (if erp-expr (if erp-tyname (reterr (msg "In the ambiguous expression or type name ~x0, ~ neither the expression nor the type name ~ can be successfully disambiguated ~ given the current table ~x1. ~ The code must be invalid, ~ because at least one must succeed.~%~%~ These are the failures for each:~%~%~ ~@2~%~%~@3" (amb-expr/tyname-fix expr/tyname) (dimb-table-fix table) erp-expr erp-tyname)) (retok (expr/tyname-tyname new-tyname) table-tyname)) (if erp-tyname (retok (expr/tyname-expr new-expr) table-expr) (reterr (msg "In the ambiguous expression or type name ~x0, ~ both the expression and the type name ~ are successfully disambiguated ~ given the current table ~x1. ~ The code must be invalid, ~ because at most one must succeed." (amb-expr/tyname-fix expr/tyname) (dimb-table-fix table))))))))
Function:
(defun dimb-amb-declor/absdeclor (declor/absdeclor table) (declare (xargs :guard (and (amb-declor/absdeclor-p declor/absdeclor) (dimb-tablep table)))) (let ((__function__ 'dimb-amb-declor/absdeclor)) (declare (ignorable __function__)) (b* (((reterr) (irr-declor/absdeclor) nil (irr-dimb-table)) ((amb-declor/absdeclor declor/absdeclor) declor/absdeclor) ((mv erp-declor new-declor ident table-declor) (dimb-declor declor/absdeclor.declor nil table)) ((mv erp-absdeclor new-absdeclor table-absdeclor) (dimb-absdeclor declor/absdeclor.absdeclor table))) (if erp-declor (if erp-absdeclor (reterr (msg "In the ambiguous ~ declarator or abstract declarator ~x0, ~ neither the declarator nor the abstract declarator ~ can be successfully disambiguated ~ given the current table ~x1. ~ The code must be invalid, ~ because at least one must succeed.~%~%~ These are the failures for each:~%~%~ ~@2~%~%~@3" (amb-declor/absdeclor-fix declor/absdeclor) (dimb-table-fix table) erp-declor erp-absdeclor)) (retok (declor/absdeclor-absdeclor new-absdeclor) nil table-absdeclor)) (if erp-absdeclor (retok (declor/absdeclor-declor new-declor) ident table-declor) (b* ((kind (dimb-lookup-ident ident table))) (if (equal kind (dimb-kind-typedef)) (retok (declor/absdeclor-absdeclor new-absdeclor) nil table-absdeclor) (reterr (msg "In the ambiguous ~ declarator or abstract declarator ~x0, ~ both the declarator and the abstract declarator ~ are successfully disambiguated ~ given the current table ~x1, ~ and the identifier ~x2 in the declarator ~ is not a typedef name. ~ The code must be invalid, ~ because at most one must succeed." (amb-declor/absdeclor-fix declor/absdeclor) (dimb-table-fix table) ident)))))))))
Theorem:
(defthm return-type-of-dimb-expr.new-expr (b* (((mv acl2::?erp ?new-expr ?new-table) (dimb-expr expr table))) (exprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-expr.new-table (b* (((mv acl2::?erp ?new-expr ?new-table) (dimb-expr expr table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-expr-list.new-exprs (b* (((mv acl2::?erp ?new-exprs ?new-table) (dimb-expr-list exprs table))) (expr-listp new-exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-expr-list.new-table (b* (((mv acl2::?erp ?new-exprs ?new-table) (dimb-expr-list exprs table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-expr-option.new-expr? (b* (((mv acl2::?erp ?new-expr? ?new-table) (dimb-expr-option expr? table))) (expr-optionp new-expr?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-expr-option.new-table (b* (((mv acl2::?erp ?new-expr? ?new-table) (dimb-expr-option expr? table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-const-expr.new-cexpr (b* (((mv acl2::?erp ?new-cexpr ?new-table) (dimb-const-expr cexpr table))) (const-exprp new-cexpr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-const-expr.new-table (b* (((mv acl2::?erp ?new-cexpr ?new-table) (dimb-const-expr cexpr table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-const-expr-option.new-cexpr? (b* (((mv acl2::?erp ?new-cexpr? ?new-table) (dimb-const-expr-option cexpr? table))) (const-expr-optionp new-cexpr?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-const-expr-option.new-table (b* (((mv acl2::?erp ?new-cexpr? ?new-table) (dimb-const-expr-option cexpr? table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-genassoc.new-assoc (b* (((mv acl2::?erp ?new-assoc ?new-table) (dimb-genassoc assoc table))) (genassocp new-assoc)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-genassoc.new-table (b* (((mv acl2::?erp ?new-assoc ?new-table) (dimb-genassoc assoc table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-genassoc-list.new-assocs (b* (((mv acl2::?erp ?new-assocs ?new-table) (dimb-genassoc-list assocs table))) (genassoc-listp new-assocs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-genassoc-list.new-table (b* (((mv acl2::?erp ?new-assocs ?new-table) (dimb-genassoc-list assocs table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-type-spec.new-tyspec (b* (((mv acl2::?erp ?new-tyspec ?new-table) (dimb-type-spec tyspec table))) (type-specp new-tyspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-type-spec.new-table (b* (((mv acl2::?erp ?new-tyspec ?new-table) (dimb-type-spec tyspec table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-spec/qual.new-specqual (b* (((mv acl2::?erp ?new-specqual ?new-table) (dimb-spec/qual specqual table))) (spec/qual-p new-specqual)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-spec/qual.new-table (b* (((mv acl2::?erp ?new-specqual ?new-table) (dimb-spec/qual specqual table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-spec/qual-list.new-specquals (b* (((mv acl2::?erp ?new-specquals ?new-table) (dimb-spec/qual-list specquals table))) (spec/qual-listp new-specquals)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-spec/qual-list.new-table (b* (((mv acl2::?erp ?new-specquals ?new-table) (dimb-spec/qual-list specquals table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-align-spec.new-alignspec (b* (((mv acl2::?erp ?new-alignspec ?new-table) (dimb-align-spec alignspec table))) (align-specp new-alignspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-align-spec.new-table (b* (((mv acl2::?erp ?new-alignspec ?new-table) (dimb-align-spec alignspec table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declspec.new-declspec (b* (((mv acl2::?erp ?new-declspec ?new-kind ?new-table) (dimb-declspec declspec kind table))) (declspecp new-declspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declspec.new-kind (b* (((mv acl2::?erp ?new-declspec ?new-kind ?new-table) (dimb-declspec declspec kind table))) (dimb-kindp new-kind)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declspec.new-table (b* (((mv acl2::?erp ?new-declspec ?new-kind ?new-table) (dimb-declspec declspec kind table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declspec-list.new-declspecs (b* (((mv acl2::?erp ?new-declspecs ?new-kind ?new-table) (dimb-declspec-list declspecs kind table))) (declspec-listp new-declspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declspec-list.new-kind (b* (((mv acl2::?erp ?new-declspecs ?new-kind ?new-table) (dimb-declspec-list declspecs kind table))) (dimb-kindp new-kind)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declspec-list.new-table (b* (((mv acl2::?erp ?new-declspecs ?new-kind ?new-table) (dimb-declspec-list declspecs kind table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-initer.new-initer (b* (((mv acl2::?erp ?new-initer ?new-table) (dimb-initer initer table))) (initerp new-initer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-initer.new-table (b* (((mv acl2::?erp ?new-initer ?new-table) (dimb-initer initer table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-initer-option.new-initer? (b* (((mv acl2::?erp ?new-initer? ?new-table) (dimb-initer-option initer? table))) (initer-optionp new-initer?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-initer-option.new-table (b* (((mv acl2::?erp ?new-initer? ?new-table) (dimb-initer-option initer? table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-desiniter.new-desiniter (b* (((mv acl2::?erp ?new-desiniter ?new-table) (dimb-desiniter desiniter table))) (desiniterp new-desiniter)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-desiniter.new-table (b* (((mv acl2::?erp ?new-desiniter ?new-table) (dimb-desiniter desiniter table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-desiniter-list.new-desiniters (b* (((mv acl2::?erp ?new-desiniters ?new-table) (dimb-desiniter-list desiniters table))) (desiniter-listp new-desiniters)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-desiniter-list.new-table (b* (((mv acl2::?erp ?new-desiniters ?new-table) (dimb-desiniter-list desiniters table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-designor.new-design (b* (((mv acl2::?erp ?new-design ?new-table) (dimb-designor design table))) (designorp new-design)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-designor.new-table (b* (((mv acl2::?erp ?new-design ?new-table) (dimb-designor design table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-designor-list.new-designs (b* (((mv acl2::?erp ?new-designs ?new-table) (dimb-designor-list designs table))) (designor-listp new-designs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-designor-list.new-table (b* (((mv acl2::?erp ?new-designs ?new-table) (dimb-designor-list designs table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declor.new-declor (b* (((mv acl2::?erp ?new-declor ?ident acl2::?table) (dimb-declor declor fundefp table))) (declorp new-declor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declor.ident (b* (((mv acl2::?erp ?new-declor ?ident acl2::?table) (dimb-declor declor fundefp table))) (identp ident)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declor.table (b* (((mv acl2::?erp ?new-declor ?ident acl2::?table) (dimb-declor declor fundefp table))) (dimb-tablep table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declor-option.new-declor? (b* (((mv acl2::?erp ?new-declor? ?ident? ?new-table) (dimb-declor-option declor? table))) (declor-optionp new-declor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declor-option.ident? (b* (((mv acl2::?erp ?new-declor? ?ident? ?new-table) (dimb-declor-option declor? table))) (ident-optionp ident?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-declor-option.new-table (b* (((mv acl2::?erp ?new-declor? ?ident? ?new-table) (dimb-declor-option declor? table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-dirdeclor.new-dirdeclor (b* (((mv acl2::?erp ?new-dirdeclor ?ident ?new-table) (dimb-dirdeclor dirdeclor fundefp table))) (dirdeclorp new-dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-dirdeclor.ident (b* (((mv acl2::?erp ?new-dirdeclor ?ident ?new-table) (dimb-dirdeclor dirdeclor fundefp table))) (identp ident)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-dirdeclor.new-table (b* (((mv acl2::?erp ?new-dirdeclor ?ident ?new-table) (dimb-dirdeclor dirdeclor fundefp table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-absdeclor.new-absdeclor (b* (((mv acl2::?erp ?new-absdeclor ?new-table) (dimb-absdeclor absdeclor table))) (absdeclorp new-absdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-absdeclor.new-table (b* (((mv acl2::?erp ?new-absdeclor ?new-table) (dimb-absdeclor absdeclor table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-absdeclor-option.new-absdeclor? (b* (((mv acl2::?erp ?new-absdeclor? ?new-table) (dimb-absdeclor-option absdeclor? table))) (absdeclor-optionp new-absdeclor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-absdeclor-option.new-table (b* (((mv acl2::?erp ?new-absdeclor? ?new-table) (dimb-absdeclor-option absdeclor? table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-dirabsdeclor.new-dirabsdeclor (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-table) (dimb-dirabsdeclor dirabsdeclor table))) (dirabsdeclorp new-dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-dirabsdeclor.new-table (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-table) (dimb-dirabsdeclor dirabsdeclor table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-dirabsdeclor-option.new-dirabsdeclor? (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-table) (dimb-dirabsdeclor-option dirabsdeclor? table))) (dirabsdeclor-optionp new-dirabsdeclor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-dirabsdeclor-option.new-table (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-table) (dimb-dirabsdeclor-option dirabsdeclor? table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-paramdecl.new-paramdecl (b* (((mv acl2::?erp ?new-paramdecl ?new-table) (dimb-paramdecl paramdecl table))) (paramdeclp new-paramdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-paramdecl.new-table (b* (((mv acl2::?erp ?new-paramdecl ?new-table) (dimb-paramdecl paramdecl table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-paramdecl-list.new-paramdecls (b* (((mv acl2::?erp ?new-paramdecls ?new-table) (dimb-paramdecl-list paramdecls table))) (paramdecl-listp new-paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-paramdecl-list.new-table (b* (((mv acl2::?erp ?new-paramdecls ?new-table) (dimb-paramdecl-list paramdecls table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-paramdeclor.new-paramdeclor (b* (((mv acl2::?erp ?new-paramdeclor ?new-table) (dimb-paramdeclor paramdeclor table))) (paramdeclorp new-paramdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-paramdeclor.new-table (b* (((mv acl2::?erp ?new-paramdeclor ?new-table) (dimb-paramdeclor paramdeclor table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-tyname.new-tyname (b* (((mv acl2::?erp ?new-tyname ?new-table) (dimb-tyname tyname table))) (tynamep new-tyname)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-tyname.new-table (b* (((mv acl2::?erp ?new-tyname ?new-table) (dimb-tyname tyname table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-strunispec.new-strunispec (b* (((mv acl2::?erp ?new-strunispec ?new-table) (dimb-strunispec strunispec table))) (strunispecp new-strunispec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-strunispec.new-table (b* (((mv acl2::?erp ?new-strunispec ?new-table) (dimb-strunispec strunispec table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-structdecl.new-structdecl (b* (((mv acl2::?erp ?new-structdecl ?new-table) (dimb-structdecl structdecl table))) (structdeclp new-structdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-structdecl.new-table (b* (((mv acl2::?erp ?new-structdecl ?new-table) (dimb-structdecl structdecl table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-structdecl-list.new-structdecls (b* (((mv acl2::?erp ?new-structdecls ?new-table) (dimb-structdecl-list structdecls table))) (structdecl-listp new-structdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-structdecl-list.new-table (b* (((mv acl2::?erp ?new-structdecls ?new-table) (dimb-structdecl-list structdecls table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-structdeclor.new-structdeclor (b* (((mv acl2::?erp ?new-structdeclor ?new-table) (dimb-structdeclor structdeclor table))) (structdeclorp new-structdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-structdeclor.new-table (b* (((mv acl2::?erp ?new-structdeclor ?new-table) (dimb-structdeclor structdeclor table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-structdeclor-list.new-structdeclors (b* (((mv acl2::?erp ?new-structdeclors ?new-table) (dimb-structdeclor-list structdeclors table))) (structdeclor-listp new-structdeclors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-structdeclor-list.new-table (b* (((mv acl2::?erp ?new-structdeclors ?new-table) (dimb-structdeclor-list structdeclors table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-enumspec.new-enumspec (b* (((mv acl2::?erp ?new-enumspec ?new-table) (dimb-enumspec enumspec table))) (enumspecp new-enumspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-enumspec.new-table (b* (((mv acl2::?erp ?new-enumspec ?new-table) (dimb-enumspec enumspec table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-enumer.new-enumer (b* (((mv acl2::?erp ?new-enumer ?new-table) (dimb-enumer enumer table))) (enumerp new-enumer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-enumer.new-table (b* (((mv acl2::?erp ?new-enumer ?new-table) (dimb-enumer enumer table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-enumer-list.new-enumers (b* (((mv acl2::?erp ?new-enumers ?new-table) (dimb-enumer-list enumers table))) (enumer-listp new-enumers)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-enumer-list.new-table (b* (((mv acl2::?erp ?new-enumers ?new-table) (dimb-enumer-list enumers table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-statassert.new-statassert (b* (((mv acl2::?erp ?new-statassert ?new-table) (dimb-statassert statassert table))) (statassertp new-statassert)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-statassert.new-table (b* (((mv acl2::?erp ?new-statassert ?new-table) (dimb-statassert statassert table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-amb-expr/tyname.expr-or-tyname (b* (((mv acl2::?erp ?expr-or-tyname ?new-table) (dimb-amb-expr/tyname expr/tyname table))) (expr/tyname-p expr-or-tyname)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-amb-expr/tyname.new-table (b* (((mv acl2::?erp ?expr-or-tyname ?new-table) (dimb-amb-expr/tyname expr/tyname table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-amb-declor/absdeclor.declor-or-absdeclor (b* (((mv acl2::?erp ?declor-or-absdeclor ?ident? ?new-table) (dimb-amb-declor/absdeclor declor/absdeclor table))) (declor/absdeclor-p declor-or-absdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-amb-declor/absdeclor.ident? (b* (((mv acl2::?erp ?declor-or-absdeclor ?ident? ?new-table) (dimb-amb-declor/absdeclor declor/absdeclor table))) (ident-optionp ident?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-amb-declor/absdeclor.new-table (b* (((mv acl2::?erp ?declor-or-absdeclor ?ident? ?new-table) (dimb-amb-declor/absdeclor declor/absdeclor table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm dimb-expr-of-expr-fix-expr (equal (dimb-expr (expr-fix expr) table) (dimb-expr expr table)))
Theorem:
(defthm dimb-expr-of-dimb-table-fix-table (equal (dimb-expr expr (dimb-table-fix table)) (dimb-expr expr table)))
Theorem:
(defthm dimb-expr-list-of-expr-list-fix-exprs (equal (dimb-expr-list (expr-list-fix exprs) table) (dimb-expr-list exprs table)))
Theorem:
(defthm dimb-expr-list-of-dimb-table-fix-table (equal (dimb-expr-list exprs (dimb-table-fix table)) (dimb-expr-list exprs table)))
Theorem:
(defthm dimb-expr-option-of-expr-option-fix-expr? (equal (dimb-expr-option (expr-option-fix expr?) table) (dimb-expr-option expr? table)))
Theorem:
(defthm dimb-expr-option-of-dimb-table-fix-table (equal (dimb-expr-option expr? (dimb-table-fix table)) (dimb-expr-option expr? table)))
Theorem:
(defthm dimb-const-expr-of-const-expr-fix-cexpr (equal (dimb-const-expr (const-expr-fix cexpr) table) (dimb-const-expr cexpr table)))
Theorem:
(defthm dimb-const-expr-of-dimb-table-fix-table (equal (dimb-const-expr cexpr (dimb-table-fix table)) (dimb-const-expr cexpr table)))
Theorem:
(defthm dimb-const-expr-option-of-const-expr-option-fix-cexpr? (equal (dimb-const-expr-option (const-expr-option-fix cexpr?) table) (dimb-const-expr-option cexpr? table)))
Theorem:
(defthm dimb-const-expr-option-of-dimb-table-fix-table (equal (dimb-const-expr-option cexpr? (dimb-table-fix table)) (dimb-const-expr-option cexpr? table)))
Theorem:
(defthm dimb-genassoc-of-genassoc-fix-assoc (equal (dimb-genassoc (genassoc-fix assoc) table) (dimb-genassoc assoc table)))
Theorem:
(defthm dimb-genassoc-of-dimb-table-fix-table (equal (dimb-genassoc assoc (dimb-table-fix table)) (dimb-genassoc assoc table)))
Theorem:
(defthm dimb-genassoc-list-of-genassoc-list-fix-assocs (equal (dimb-genassoc-list (genassoc-list-fix assocs) table) (dimb-genassoc-list assocs table)))
Theorem:
(defthm dimb-genassoc-list-of-dimb-table-fix-table (equal (dimb-genassoc-list assocs (dimb-table-fix table)) (dimb-genassoc-list assocs table)))
Theorem:
(defthm dimb-type-spec-of-type-spec-fix-tyspec (equal (dimb-type-spec (type-spec-fix tyspec) table) (dimb-type-spec tyspec table)))
Theorem:
(defthm dimb-type-spec-of-dimb-table-fix-table (equal (dimb-type-spec tyspec (dimb-table-fix table)) (dimb-type-spec tyspec table)))
Theorem:
(defthm dimb-spec/qual-of-spec/qual-fix-specqual (equal (dimb-spec/qual (spec/qual-fix specqual) table) (dimb-spec/qual specqual table)))
Theorem:
(defthm dimb-spec/qual-of-dimb-table-fix-table (equal (dimb-spec/qual specqual (dimb-table-fix table)) (dimb-spec/qual specqual table)))
Theorem:
(defthm dimb-spec/qual-list-of-spec/qual-list-fix-specquals (equal (dimb-spec/qual-list (spec/qual-list-fix specquals) table) (dimb-spec/qual-list specquals table)))
Theorem:
(defthm dimb-spec/qual-list-of-dimb-table-fix-table (equal (dimb-spec/qual-list specquals (dimb-table-fix table)) (dimb-spec/qual-list specquals table)))
Theorem:
(defthm dimb-align-spec-of-align-spec-fix-alignspec (equal (dimb-align-spec (align-spec-fix alignspec) table) (dimb-align-spec alignspec table)))
Theorem:
(defthm dimb-align-spec-of-dimb-table-fix-table (equal (dimb-align-spec alignspec (dimb-table-fix table)) (dimb-align-spec alignspec table)))
Theorem:
(defthm dimb-declspec-of-declspec-fix-declspec (equal (dimb-declspec (declspec-fix declspec) kind table) (dimb-declspec declspec kind table)))
Theorem:
(defthm dimb-declspec-of-dimb-kind-fix-kind (equal (dimb-declspec declspec (dimb-kind-fix kind) table) (dimb-declspec declspec kind table)))
Theorem:
(defthm dimb-declspec-of-dimb-table-fix-table (equal (dimb-declspec declspec kind (dimb-table-fix table)) (dimb-declspec declspec kind table)))
Theorem:
(defthm dimb-declspec-list-of-declspec-list-fix-declspecs (equal (dimb-declspec-list (declspec-list-fix declspecs) kind table) (dimb-declspec-list declspecs kind table)))
Theorem:
(defthm dimb-declspec-list-of-dimb-kind-fix-kind (equal (dimb-declspec-list declspecs (dimb-kind-fix kind) table) (dimb-declspec-list declspecs kind table)))
Theorem:
(defthm dimb-declspec-list-of-dimb-table-fix-table (equal (dimb-declspec-list declspecs kind (dimb-table-fix table)) (dimb-declspec-list declspecs kind table)))
Theorem:
(defthm dimb-initer-of-initer-fix-initer (equal (dimb-initer (initer-fix initer) table) (dimb-initer initer table)))
Theorem:
(defthm dimb-initer-of-dimb-table-fix-table (equal (dimb-initer initer (dimb-table-fix table)) (dimb-initer initer table)))
Theorem:
(defthm dimb-initer-option-of-initer-option-fix-initer? (equal (dimb-initer-option (initer-option-fix initer?) table) (dimb-initer-option initer? table)))
Theorem:
(defthm dimb-initer-option-of-dimb-table-fix-table (equal (dimb-initer-option initer? (dimb-table-fix table)) (dimb-initer-option initer? table)))
Theorem:
(defthm dimb-desiniter-of-desiniter-fix-desiniter (equal (dimb-desiniter (desiniter-fix desiniter) table) (dimb-desiniter desiniter table)))
Theorem:
(defthm dimb-desiniter-of-dimb-table-fix-table (equal (dimb-desiniter desiniter (dimb-table-fix table)) (dimb-desiniter desiniter table)))
Theorem:
(defthm dimb-desiniter-list-of-desiniter-list-fix-desiniters (equal (dimb-desiniter-list (desiniter-list-fix desiniters) table) (dimb-desiniter-list desiniters table)))
Theorem:
(defthm dimb-desiniter-list-of-dimb-table-fix-table (equal (dimb-desiniter-list desiniters (dimb-table-fix table)) (dimb-desiniter-list desiniters table)))
Theorem:
(defthm dimb-designor-of-designor-fix-design (equal (dimb-designor (designor-fix design) table) (dimb-designor design table)))
Theorem:
(defthm dimb-designor-of-dimb-table-fix-table (equal (dimb-designor design (dimb-table-fix table)) (dimb-designor design table)))
Theorem:
(defthm dimb-designor-list-of-designor-list-fix-designs (equal (dimb-designor-list (designor-list-fix designs) table) (dimb-designor-list designs table)))
Theorem:
(defthm dimb-designor-list-of-dimb-table-fix-table (equal (dimb-designor-list designs (dimb-table-fix table)) (dimb-designor-list designs table)))
Theorem:
(defthm dimb-declor-of-declor-fix-declor (equal (dimb-declor (declor-fix declor) fundefp table) (dimb-declor declor fundefp table)))
Theorem:
(defthm dimb-declor-of-bool-fix-fundefp (equal (dimb-declor declor (bool-fix fundefp) table) (dimb-declor declor fundefp table)))
Theorem:
(defthm dimb-declor-of-dimb-table-fix-table (equal (dimb-declor declor fundefp (dimb-table-fix table)) (dimb-declor declor fundefp table)))
Theorem:
(defthm dimb-declor-option-of-declor-option-fix-declor? (equal (dimb-declor-option (declor-option-fix declor?) table) (dimb-declor-option declor? table)))
Theorem:
(defthm dimb-declor-option-of-dimb-table-fix-table (equal (dimb-declor-option declor? (dimb-table-fix table)) (dimb-declor-option declor? table)))
Theorem:
(defthm dimb-dirdeclor-of-dirdeclor-fix-dirdeclor (equal (dimb-dirdeclor (dirdeclor-fix dirdeclor) fundefp table) (dimb-dirdeclor dirdeclor fundefp table)))
Theorem:
(defthm dimb-dirdeclor-of-bool-fix-fundefp (equal (dimb-dirdeclor dirdeclor (bool-fix fundefp) table) (dimb-dirdeclor dirdeclor fundefp table)))
Theorem:
(defthm dimb-dirdeclor-of-dimb-table-fix-table (equal (dimb-dirdeclor dirdeclor fundefp (dimb-table-fix table)) (dimb-dirdeclor dirdeclor fundefp table)))
Theorem:
(defthm dimb-absdeclor-of-absdeclor-fix-absdeclor (equal (dimb-absdeclor (absdeclor-fix absdeclor) table) (dimb-absdeclor absdeclor table)))
Theorem:
(defthm dimb-absdeclor-of-dimb-table-fix-table (equal (dimb-absdeclor absdeclor (dimb-table-fix table)) (dimb-absdeclor absdeclor table)))
Theorem:
(defthm dimb-absdeclor-option-of-absdeclor-option-fix-absdeclor? (equal (dimb-absdeclor-option (absdeclor-option-fix absdeclor?) table) (dimb-absdeclor-option absdeclor? table)))
Theorem:
(defthm dimb-absdeclor-option-of-dimb-table-fix-table (equal (dimb-absdeclor-option absdeclor? (dimb-table-fix table)) (dimb-absdeclor-option absdeclor? table)))
Theorem:
(defthm dimb-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor (equal (dimb-dirabsdeclor (dirabsdeclor-fix dirabsdeclor) table) (dimb-dirabsdeclor dirabsdeclor table)))
Theorem:
(defthm dimb-dirabsdeclor-of-dimb-table-fix-table (equal (dimb-dirabsdeclor dirabsdeclor (dimb-table-fix table)) (dimb-dirabsdeclor dirabsdeclor table)))
Theorem:
(defthm dimb-dirabsdeclor-option-of-dirabsdeclor-option-fix-dirabsdeclor? (equal (dimb-dirabsdeclor-option (dirabsdeclor-option-fix dirabsdeclor?) table) (dimb-dirabsdeclor-option dirabsdeclor? table)))
Theorem:
(defthm dimb-dirabsdeclor-option-of-dimb-table-fix-table (equal (dimb-dirabsdeclor-option dirabsdeclor? (dimb-table-fix table)) (dimb-dirabsdeclor-option dirabsdeclor? table)))
Theorem:
(defthm dimb-paramdecl-of-paramdecl-fix-paramdecl (equal (dimb-paramdecl (paramdecl-fix paramdecl) table) (dimb-paramdecl paramdecl table)))
Theorem:
(defthm dimb-paramdecl-of-dimb-table-fix-table (equal (dimb-paramdecl paramdecl (dimb-table-fix table)) (dimb-paramdecl paramdecl table)))
Theorem:
(defthm dimb-paramdecl-list-of-paramdecl-list-fix-paramdecls (equal (dimb-paramdecl-list (paramdecl-list-fix paramdecls) table) (dimb-paramdecl-list paramdecls table)))
Theorem:
(defthm dimb-paramdecl-list-of-dimb-table-fix-table (equal (dimb-paramdecl-list paramdecls (dimb-table-fix table)) (dimb-paramdecl-list paramdecls table)))
Theorem:
(defthm dimb-paramdeclor-of-paramdeclor-fix-paramdeclor (equal (dimb-paramdeclor (paramdeclor-fix paramdeclor) table) (dimb-paramdeclor paramdeclor table)))
Theorem:
(defthm dimb-paramdeclor-of-dimb-table-fix-table (equal (dimb-paramdeclor paramdeclor (dimb-table-fix table)) (dimb-paramdeclor paramdeclor table)))
Theorem:
(defthm dimb-tyname-of-tyname-fix-tyname (equal (dimb-tyname (tyname-fix tyname) table) (dimb-tyname tyname table)))
Theorem:
(defthm dimb-tyname-of-dimb-table-fix-table (equal (dimb-tyname tyname (dimb-table-fix table)) (dimb-tyname tyname table)))
Theorem:
(defthm dimb-strunispec-of-strunispec-fix-strunispec (equal (dimb-strunispec (strunispec-fix strunispec) table) (dimb-strunispec strunispec table)))
Theorem:
(defthm dimb-strunispec-of-dimb-table-fix-table (equal (dimb-strunispec strunispec (dimb-table-fix table)) (dimb-strunispec strunispec table)))
Theorem:
(defthm dimb-structdecl-of-structdecl-fix-structdecl (equal (dimb-structdecl (structdecl-fix structdecl) table) (dimb-structdecl structdecl table)))
Theorem:
(defthm dimb-structdecl-of-dimb-table-fix-table (equal (dimb-structdecl structdecl (dimb-table-fix table)) (dimb-structdecl structdecl table)))
Theorem:
(defthm dimb-structdecl-list-of-structdecl-list-fix-structdecls (equal (dimb-structdecl-list (structdecl-list-fix structdecls) table) (dimb-structdecl-list structdecls table)))
Theorem:
(defthm dimb-structdecl-list-of-dimb-table-fix-table (equal (dimb-structdecl-list structdecls (dimb-table-fix table)) (dimb-structdecl-list structdecls table)))
Theorem:
(defthm dimb-structdeclor-of-structdeclor-fix-structdeclor (equal (dimb-structdeclor (structdeclor-fix structdeclor) table) (dimb-structdeclor structdeclor table)))
Theorem:
(defthm dimb-structdeclor-of-dimb-table-fix-table (equal (dimb-structdeclor structdeclor (dimb-table-fix table)) (dimb-structdeclor structdeclor table)))
Theorem:
(defthm dimb-structdeclor-list-of-structdeclor-list-fix-structdeclors (equal (dimb-structdeclor-list (structdeclor-list-fix structdeclors) table) (dimb-structdeclor-list structdeclors table)))
Theorem:
(defthm dimb-structdeclor-list-of-dimb-table-fix-table (equal (dimb-structdeclor-list structdeclors (dimb-table-fix table)) (dimb-structdeclor-list structdeclors table)))
Theorem:
(defthm dimb-enumspec-of-enumspec-fix-enumspec (equal (dimb-enumspec (enumspec-fix enumspec) table) (dimb-enumspec enumspec table)))
Theorem:
(defthm dimb-enumspec-of-dimb-table-fix-table (equal (dimb-enumspec enumspec (dimb-table-fix table)) (dimb-enumspec enumspec table)))
Theorem:
(defthm dimb-enumer-of-enumer-fix-enumer (equal (dimb-enumer (enumer-fix enumer) table) (dimb-enumer enumer table)))
Theorem:
(defthm dimb-enumer-of-dimb-table-fix-table (equal (dimb-enumer enumer (dimb-table-fix table)) (dimb-enumer enumer table)))
Theorem:
(defthm dimb-enumer-list-of-enumer-list-fix-enumers (equal (dimb-enumer-list (enumer-list-fix enumers) table) (dimb-enumer-list enumers table)))
Theorem:
(defthm dimb-enumer-list-of-dimb-table-fix-table (equal (dimb-enumer-list enumers (dimb-table-fix table)) (dimb-enumer-list enumers table)))
Theorem:
(defthm dimb-statassert-of-statassert-fix-statassert (equal (dimb-statassert (statassert-fix statassert) table) (dimb-statassert statassert table)))
Theorem:
(defthm dimb-statassert-of-dimb-table-fix-table (equal (dimb-statassert statassert (dimb-table-fix table)) (dimb-statassert statassert table)))
Theorem:
(defthm dimb-amb-expr/tyname-of-amb-expr/tyname-fix-expr/tyname (equal (dimb-amb-expr/tyname (amb-expr/tyname-fix expr/tyname) table) (dimb-amb-expr/tyname expr/tyname table)))
Theorem:
(defthm dimb-amb-expr/tyname-of-dimb-table-fix-table (equal (dimb-amb-expr/tyname expr/tyname (dimb-table-fix table)) (dimb-amb-expr/tyname expr/tyname table)))
Theorem:
(defthm dimb-amb-declor/absdeclor-of-amb-declor/absdeclor-fix-declor/absdeclor (equal (dimb-amb-declor/absdeclor (amb-declor/absdeclor-fix declor/absdeclor) table) (dimb-amb-declor/absdeclor declor/absdeclor table)))
Theorem:
(defthm dimb-amb-declor/absdeclor-of-dimb-table-fix-table (equal (dimb-amb-declor/absdeclor declor/absdeclor (dimb-table-fix table)) (dimb-amb-declor/absdeclor declor/absdeclor table)))
Theorem:
(defthm dimb-expr-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (dimb-expr expr table) (dimb-expr expr-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-expr-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-expr expr table) (dimb-expr expr table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-expr-list-expr-list-equiv-congruence-on-exprs (implies (expr-list-equiv exprs exprs-equiv) (equal (dimb-expr-list exprs table) (dimb-expr-list exprs-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-expr-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-expr-list exprs table) (dimb-expr-list exprs table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-expr-option-expr-option-equiv-congruence-on-expr? (implies (expr-option-equiv expr? expr?-equiv) (equal (dimb-expr-option expr? table) (dimb-expr-option expr?-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-expr-option-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-expr-option expr? table) (dimb-expr-option expr? table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-const-expr-const-expr-equiv-congruence-on-cexpr (implies (const-expr-equiv cexpr cexpr-equiv) (equal (dimb-const-expr cexpr table) (dimb-const-expr cexpr-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-const-expr-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-const-expr cexpr table) (dimb-const-expr cexpr table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-const-expr-option-const-expr-option-equiv-congruence-on-cexpr? (implies (const-expr-option-equiv cexpr? cexpr?-equiv) (equal (dimb-const-expr-option cexpr? table) (dimb-const-expr-option cexpr?-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-const-expr-option-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-const-expr-option cexpr? table) (dimb-const-expr-option cexpr? table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-genassoc-genassoc-equiv-congruence-on-assoc (implies (genassoc-equiv assoc assoc-equiv) (equal (dimb-genassoc assoc table) (dimb-genassoc assoc-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-genassoc-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-genassoc assoc table) (dimb-genassoc assoc table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-genassoc-list-genassoc-list-equiv-congruence-on-assocs (implies (genassoc-list-equiv assocs assocs-equiv) (equal (dimb-genassoc-list assocs table) (dimb-genassoc-list assocs-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-genassoc-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-genassoc-list assocs table) (dimb-genassoc-list assocs table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-type-spec-type-spec-equiv-congruence-on-tyspec (implies (type-spec-equiv tyspec tyspec-equiv) (equal (dimb-type-spec tyspec table) (dimb-type-spec tyspec-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-type-spec-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-type-spec tyspec table) (dimb-type-spec tyspec table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-spec/qual-spec/qual-equiv-congruence-on-specqual (implies (spec/qual-equiv specqual specqual-equiv) (equal (dimb-spec/qual specqual table) (dimb-spec/qual specqual-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-spec/qual-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-spec/qual specqual table) (dimb-spec/qual specqual table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-spec/qual-list-spec/qual-list-equiv-congruence-on-specquals (implies (spec/qual-list-equiv specquals specquals-equiv) (equal (dimb-spec/qual-list specquals table) (dimb-spec/qual-list specquals-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-spec/qual-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-spec/qual-list specquals table) (dimb-spec/qual-list specquals table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-align-spec-align-spec-equiv-congruence-on-alignspec (implies (align-spec-equiv alignspec alignspec-equiv) (equal (dimb-align-spec alignspec table) (dimb-align-spec alignspec-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-align-spec-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-align-spec alignspec table) (dimb-align-spec alignspec table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-declspec-declspec-equiv-congruence-on-declspec (implies (declspec-equiv declspec declspec-equiv) (equal (dimb-declspec declspec kind table) (dimb-declspec declspec-equiv kind table))) :rule-classes :congruence)
Theorem:
(defthm dimb-declspec-dimb-kind-equiv-congruence-on-kind (implies (dimb-kind-equiv kind kind-equiv) (equal (dimb-declspec declspec kind table) (dimb-declspec declspec kind-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-declspec-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-declspec declspec kind table) (dimb-declspec declspec kind table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-declspec-list-declspec-list-equiv-congruence-on-declspecs (implies (declspec-list-equiv declspecs declspecs-equiv) (equal (dimb-declspec-list declspecs kind table) (dimb-declspec-list declspecs-equiv kind table))) :rule-classes :congruence)
Theorem:
(defthm dimb-declspec-list-dimb-kind-equiv-congruence-on-kind (implies (dimb-kind-equiv kind kind-equiv) (equal (dimb-declspec-list declspecs kind table) (dimb-declspec-list declspecs kind-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-declspec-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-declspec-list declspecs kind table) (dimb-declspec-list declspecs kind table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-initer-initer-equiv-congruence-on-initer (implies (initer-equiv initer initer-equiv) (equal (dimb-initer initer table) (dimb-initer initer-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-initer-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-initer initer table) (dimb-initer initer table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-initer-option-initer-option-equiv-congruence-on-initer? (implies (initer-option-equiv initer? initer?-equiv) (equal (dimb-initer-option initer? table) (dimb-initer-option initer?-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-initer-option-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-initer-option initer? table) (dimb-initer-option initer? table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-desiniter-desiniter-equiv-congruence-on-desiniter (implies (desiniter-equiv desiniter desiniter-equiv) (equal (dimb-desiniter desiniter table) (dimb-desiniter desiniter-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-desiniter-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-desiniter desiniter table) (dimb-desiniter desiniter table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-desiniter-list-desiniter-list-equiv-congruence-on-desiniters (implies (desiniter-list-equiv desiniters desiniters-equiv) (equal (dimb-desiniter-list desiniters table) (dimb-desiniter-list desiniters-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-desiniter-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-desiniter-list desiniters table) (dimb-desiniter-list desiniters table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-designor-designor-equiv-congruence-on-design (implies (designor-equiv design design-equiv) (equal (dimb-designor design table) (dimb-designor design-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-designor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-designor design table) (dimb-designor design table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-designor-list-designor-list-equiv-congruence-on-designs (implies (designor-list-equiv designs designs-equiv) (equal (dimb-designor-list designs table) (dimb-designor-list designs-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-designor-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-designor-list designs table) (dimb-designor-list designs table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-declor-declor-equiv-congruence-on-declor (implies (declor-equiv declor declor-equiv) (equal (dimb-declor declor fundefp table) (dimb-declor declor-equiv fundefp table))) :rule-classes :congruence)
Theorem:
(defthm dimb-declor-iff-congruence-on-fundefp (implies (iff fundefp fundefp-equiv) (equal (dimb-declor declor fundefp table) (dimb-declor declor fundefp-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-declor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-declor declor fundefp table) (dimb-declor declor fundefp table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-declor-option-declor-option-equiv-congruence-on-declor? (implies (declor-option-equiv declor? declor?-equiv) (equal (dimb-declor-option declor? table) (dimb-declor-option declor?-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-declor-option-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-declor-option declor? table) (dimb-declor-option declor? table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor (implies (dirdeclor-equiv dirdeclor dirdeclor-equiv) (equal (dimb-dirdeclor dirdeclor fundefp table) (dimb-dirdeclor dirdeclor-equiv fundefp table))) :rule-classes :congruence)
Theorem:
(defthm dimb-dirdeclor-iff-congruence-on-fundefp (implies (iff fundefp fundefp-equiv) (equal (dimb-dirdeclor dirdeclor fundefp table) (dimb-dirdeclor dirdeclor fundefp-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-dirdeclor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-dirdeclor dirdeclor fundefp table) (dimb-dirdeclor dirdeclor fundefp table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-absdeclor-absdeclor-equiv-congruence-on-absdeclor (implies (absdeclor-equiv absdeclor absdeclor-equiv) (equal (dimb-absdeclor absdeclor table) (dimb-absdeclor absdeclor-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-absdeclor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-absdeclor absdeclor table) (dimb-absdeclor absdeclor table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-absdeclor-option-absdeclor-option-equiv-congruence-on-absdeclor? (implies (absdeclor-option-equiv absdeclor? absdeclor?-equiv) (equal (dimb-absdeclor-option absdeclor? table) (dimb-absdeclor-option absdeclor?-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-absdeclor-option-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-absdeclor-option absdeclor? table) (dimb-absdeclor-option absdeclor? table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor (implies (dirabsdeclor-equiv dirabsdeclor dirabsdeclor-equiv) (equal (dimb-dirabsdeclor dirabsdeclor table) (dimb-dirabsdeclor dirabsdeclor-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-dirabsdeclor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-dirabsdeclor dirabsdeclor table) (dimb-dirabsdeclor dirabsdeclor table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-dirabsdeclor-option-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor? (implies (dirabsdeclor-option-equiv dirabsdeclor? dirabsdeclor?-equiv) (equal (dimb-dirabsdeclor-option dirabsdeclor? table) (dimb-dirabsdeclor-option dirabsdeclor?-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-dirabsdeclor-option-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-dirabsdeclor-option dirabsdeclor? table) (dimb-dirabsdeclor-option dirabsdeclor? table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-paramdecl-paramdecl-equiv-congruence-on-paramdecl (implies (paramdecl-equiv paramdecl paramdecl-equiv) (equal (dimb-paramdecl paramdecl table) (dimb-paramdecl paramdecl-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-paramdecl-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-paramdecl paramdecl table) (dimb-paramdecl paramdecl table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-paramdecl-list-paramdecl-list-equiv-congruence-on-paramdecls (implies (paramdecl-list-equiv paramdecls paramdecls-equiv) (equal (dimb-paramdecl-list paramdecls table) (dimb-paramdecl-list paramdecls-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-paramdecl-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-paramdecl-list paramdecls table) (dimb-paramdecl-list paramdecls table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-paramdeclor-paramdeclor-equiv-congruence-on-paramdeclor (implies (paramdeclor-equiv paramdeclor paramdeclor-equiv) (equal (dimb-paramdeclor paramdeclor table) (dimb-paramdeclor paramdeclor-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-paramdeclor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-paramdeclor paramdeclor table) (dimb-paramdeclor paramdeclor table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-tyname-tyname-equiv-congruence-on-tyname (implies (tyname-equiv tyname tyname-equiv) (equal (dimb-tyname tyname table) (dimb-tyname tyname-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-tyname-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-tyname tyname table) (dimb-tyname tyname table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-strunispec-strunispec-equiv-congruence-on-strunispec (implies (strunispec-equiv strunispec strunispec-equiv) (equal (dimb-strunispec strunispec table) (dimb-strunispec strunispec-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-strunispec-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-strunispec strunispec table) (dimb-strunispec strunispec table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-structdecl-structdecl-equiv-congruence-on-structdecl (implies (structdecl-equiv structdecl structdecl-equiv) (equal (dimb-structdecl structdecl table) (dimb-structdecl structdecl-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-structdecl-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-structdecl structdecl table) (dimb-structdecl structdecl table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-structdecl-list-structdecl-list-equiv-congruence-on-structdecls (implies (structdecl-list-equiv structdecls structdecls-equiv) (equal (dimb-structdecl-list structdecls table) (dimb-structdecl-list structdecls-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-structdecl-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-structdecl-list structdecls table) (dimb-structdecl-list structdecls table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-structdeclor-structdeclor-equiv-congruence-on-structdeclor (implies (structdeclor-equiv structdeclor structdeclor-equiv) (equal (dimb-structdeclor structdeclor table) (dimb-structdeclor structdeclor-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-structdeclor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-structdeclor structdeclor table) (dimb-structdeclor structdeclor table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-structdeclor-list-structdeclor-list-equiv-congruence-on-structdeclors (implies (structdeclor-list-equiv structdeclors structdeclors-equiv) (equal (dimb-structdeclor-list structdeclors table) (dimb-structdeclor-list structdeclors-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-structdeclor-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-structdeclor-list structdeclors table) (dimb-structdeclor-list structdeclors table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-enumspec-enumspec-equiv-congruence-on-enumspec (implies (enumspec-equiv enumspec enumspec-equiv) (equal (dimb-enumspec enumspec table) (dimb-enumspec enumspec-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-enumspec-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-enumspec enumspec table) (dimb-enumspec enumspec table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-enumer-enumer-equiv-congruence-on-enumer (implies (enumer-equiv enumer enumer-equiv) (equal (dimb-enumer enumer table) (dimb-enumer enumer-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-enumer-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-enumer enumer table) (dimb-enumer enumer table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-enumer-list-enumer-list-equiv-congruence-on-enumers (implies (enumer-list-equiv enumers enumers-equiv) (equal (dimb-enumer-list enumers table) (dimb-enumer-list enumers-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-enumer-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-enumer-list enumers table) (dimb-enumer-list enumers table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-statassert-statassert-equiv-congruence-on-statassert (implies (statassert-equiv statassert statassert-equiv) (equal (dimb-statassert statassert table) (dimb-statassert statassert-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-statassert-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-statassert statassert table) (dimb-statassert statassert table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-amb-expr/tyname-amb-expr/tyname-equiv-congruence-on-expr/tyname (implies (amb-expr/tyname-equiv expr/tyname expr/tyname-equiv) (equal (dimb-amb-expr/tyname expr/tyname table) (dimb-amb-expr/tyname expr/tyname-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-amb-expr/tyname-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-amb-expr/tyname expr/tyname table) (dimb-amb-expr/tyname expr/tyname table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-amb-declor/absdeclor-amb-declor/absdeclor-equiv-congruence-on-declor/absdeclor (implies (amb-declor/absdeclor-equiv declor/absdeclor declor/absdeclor-equiv) (equal (dimb-amb-declor/absdeclor declor/absdeclor table) (dimb-amb-declor/absdeclor declor/absdeclor-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-amb-declor/absdeclor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-amb-declor/absdeclor declor/absdeclor table) (dimb-amb-declor/absdeclor declor/absdeclor table-equiv))) :rule-classes :congruence)
Theorem:
(defthm expr-unambp-of-dimb-expr (b* (((mv acl2::?erp ?new-expr ?new-table) (dimb-expr expr table))) (implies (not erp) (expr-unambp new-expr))))
Theorem:
(defthm expr-list-unambp-of-dimb-expr-list (b* (((mv acl2::?erp ?new-exprs ?new-table) (dimb-expr-list exprs table))) (implies (not erp) (expr-list-unambp new-exprs))))
Theorem:
(defthm expr-option-unambp-of-dimb-expr-option (b* (((mv acl2::?erp ?new-expr? ?new-table) (dimb-expr-option expr? table))) (implies (not erp) (expr-option-unambp new-expr?))))
Theorem:
(defthm const-expr-unambp-of-dimb-const-expr (b* (((mv acl2::?erp ?new-cexpr ?new-table) (dimb-const-expr cexpr table))) (implies (not erp) (const-expr-unambp new-cexpr))))
Theorem:
(defthm const-expr-option-unambp-of-dimb-const-expr-option (b* (((mv acl2::?erp ?new-cexpr? ?new-table) (dimb-const-expr-option cexpr? table))) (implies (not erp) (const-expr-option-unambp new-cexpr?))))
Theorem:
(defthm genassoc-unambp-of-dimb-genassoc (b* (((mv acl2::?erp ?new-assoc ?new-table) (dimb-genassoc assoc table))) (implies (not erp) (genassoc-unambp new-assoc))))
Theorem:
(defthm genassoc-list-unambp-of-dimb-genassoc-list (b* (((mv acl2::?erp ?new-assocs ?new-table) (dimb-genassoc-list assocs table))) (implies (not erp) (genassoc-list-unambp new-assocs))))
Theorem:
(defthm type-spec-unambp-of-dimb-type-spec (b* (((mv acl2::?erp ?new-tyspec ?new-table) (dimb-type-spec tyspec table))) (implies (not erp) (type-spec-unambp new-tyspec))))
Theorem:
(defthm spec/qual-unambp-of-dimb-spec/qual (b* (((mv acl2::?erp ?new-specqual ?new-table) (dimb-spec/qual specqual table))) (implies (not erp) (spec/qual-unambp new-specqual))))
Theorem:
(defthm spec/qual-list-unambp-of-dimb-spec/qual-list (b* (((mv acl2::?erp ?new-specquals ?new-table) (dimb-spec/qual-list specquals table))) (implies (not erp) (spec/qual-list-unambp new-specquals))))
Theorem:
(defthm align-spec-unambp-of-dimb-align-spec (b* (((mv acl2::?erp ?new-alignspec ?new-table) (dimb-align-spec alignspec table))) (implies (not erp) (align-spec-unambp new-alignspec))))
Theorem:
(defthm declspec-unambp-of-dimb-declspec (b* (((mv acl2::?erp ?new-declspec ?new-kind ?new-table) (dimb-declspec declspec kind table))) (implies (not erp) (declspec-unambp new-declspec))))
Theorem:
(defthm declspec-list-unambp-of-dimb-declspec-list (b* (((mv acl2::?erp ?new-declspecs ?new-kind ?new-table) (dimb-declspec-list declspecs kind table))) (implies (not erp) (declspec-list-unambp new-declspecs))))
Theorem:
(defthm initer-unambp-of-dimb-initer (b* (((mv acl2::?erp ?new-initer ?new-table) (dimb-initer initer table))) (implies (not erp) (initer-unambp new-initer))))
Theorem:
(defthm initer-option-unambp-of-dimb-initer-option (b* (((mv acl2::?erp ?new-initer? ?new-table) (dimb-initer-option initer? table))) (implies (not erp) (initer-option-unambp new-initer?))))
Theorem:
(defthm desiniter-unambp-of-dimb-desiniter (b* (((mv acl2::?erp ?new-desiniter ?new-table) (dimb-desiniter desiniter table))) (implies (not erp) (desiniter-unambp new-desiniter))))
Theorem:
(defthm desiniter-list-unambp-of-dimb-desiniter-list (b* (((mv acl2::?erp ?new-desiniters ?new-table) (dimb-desiniter-list desiniters table))) (implies (not erp) (desiniter-list-unambp new-desiniters))))
Theorem:
(defthm designor-unambp-of-dimb-designor (b* (((mv acl2::?erp ?new-design ?new-table) (dimb-designor design table))) (implies (not erp) (designor-unambp new-design))))
Theorem:
(defthm designor-list-unambp-of-dimb-designor-list (b* (((mv acl2::?erp ?new-designs ?new-table) (dimb-designor-list designs table))) (implies (not erp) (designor-list-unambp new-designs))))
Theorem:
(defthm declor-unambp-of-dimb-declor (b* (((mv acl2::?erp ?new-declor ?ident acl2::?table) (dimb-declor declor fundefp table))) (implies (not erp) (declor-unambp new-declor))))
Theorem:
(defthm declor-option-unambp-of-dimb-declor-option (b* (((mv acl2::?erp ?new-declor? ?ident? ?new-table) (dimb-declor-option declor? table))) (implies (not erp) (declor-option-unambp new-declor?))))
Theorem:
(defthm dirdeclor-unambp-of-dimb-dirdeclor (b* (((mv acl2::?erp ?new-dirdeclor ?ident ?new-table) (dimb-dirdeclor dirdeclor fundefp table))) (implies (not erp) (dirdeclor-unambp new-dirdeclor))))
Theorem:
(defthm absdeclor-unambp-of-dimb-absdeclor (b* (((mv acl2::?erp ?new-absdeclor ?new-table) (dimb-absdeclor absdeclor table))) (implies (not erp) (absdeclor-unambp new-absdeclor))))
Theorem:
(defthm absdeclor-option-unambp-of-dimb-absdeclor-option (b* (((mv acl2::?erp ?new-absdeclor? ?new-table) (dimb-absdeclor-option absdeclor? table))) (implies (not erp) (absdeclor-option-unambp new-absdeclor?))))
Theorem:
(defthm dirabsdeclor-unambp-of-dimb-dirabsdeclor (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-table) (dimb-dirabsdeclor dirabsdeclor table))) (implies (not erp) (dirabsdeclor-unambp new-dirabsdeclor))))
Theorem:
(defthm dirabsdeclor-option-unambp-of-dimb-dirabsdeclor-option (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-table) (dimb-dirabsdeclor-option dirabsdeclor? table))) (implies (not erp) (dirabsdeclor-option-unambp new-dirabsdeclor?))))
Theorem:
(defthm paramdecl-unambp-of-dimb-paramdecl (b* (((mv acl2::?erp ?new-paramdecl ?new-table) (dimb-paramdecl paramdecl table))) (implies (not erp) (paramdecl-unambp new-paramdecl))))
Theorem:
(defthm paramdecl-list-unambp-of-dimb-paramdecl-list (b* (((mv acl2::?erp ?new-paramdecls ?new-table) (dimb-paramdecl-list paramdecls table))) (implies (not erp) (paramdecl-list-unambp new-paramdecls))))
Theorem:
(defthm paramdeclor-unambp-of-dimb-paramdeclor (b* (((mv acl2::?erp ?new-paramdeclor ?new-table) (dimb-paramdeclor paramdeclor table))) (implies (not erp) (paramdeclor-unambp new-paramdeclor))))
Theorem:
(defthm tyname-unambp-of-dimb-tyname (b* (((mv acl2::?erp ?new-tyname ?new-table) (dimb-tyname tyname table))) (implies (not erp) (tyname-unambp new-tyname))))
Theorem:
(defthm strunispec-unambp-of-dimb-strunispec (b* (((mv acl2::?erp ?new-strunispec ?new-table) (dimb-strunispec strunispec table))) (implies (not erp) (strunispec-unambp new-strunispec))))
Theorem:
(defthm structdecl-unambp-of-dimb-structdecl (b* (((mv acl2::?erp ?new-structdecl ?new-table) (dimb-structdecl structdecl table))) (implies (not erp) (structdecl-unambp new-structdecl))))
Theorem:
(defthm structdecl-list-unambp-of-dimb-structdecl-list (b* (((mv acl2::?erp ?new-structdecls ?new-table) (dimb-structdecl-list structdecls table))) (implies (not erp) (structdecl-list-unambp new-structdecls))))
Theorem:
(defthm structdeclor-unambp-of-dimb-structdeclor (b* (((mv acl2::?erp ?new-structdeclor ?new-table) (dimb-structdeclor structdeclor table))) (implies (not erp) (structdeclor-unambp new-structdeclor))))
Theorem:
(defthm structdeclor-list-unambp-of-dimb-structdeclor-list (b* (((mv acl2::?erp ?new-structdeclors ?new-table) (dimb-structdeclor-list structdeclors table))) (implies (not erp) (structdeclor-list-unambp new-structdeclors))))
Theorem:
(defthm enumspec-unambp-of-dimb-enumspec (b* (((mv acl2::?erp ?new-enumspec ?new-table) (dimb-enumspec enumspec table))) (implies (not erp) (enumspec-unambp new-enumspec))))
Theorem:
(defthm enumer-unambp-of-dimb-enumer (b* (((mv acl2::?erp ?new-enumer ?new-table) (dimb-enumer enumer table))) (implies (not erp) (enumer-unambp new-enumer))))
Theorem:
(defthm enumer-list-unambp-of-dimb-enumer-list (b* (((mv acl2::?erp ?new-enumers ?new-table) (dimb-enumer-list enumers table))) (implies (not erp) (enumer-list-unambp new-enumers))))
Theorem:
(defthm statassert-unambp-of-dimb-statassert (b* (((mv acl2::?erp ?new-statassert ?new-table) (dimb-statassert statassert table))) (implies (not erp) (statassert-unambp new-statassert))))
Theorem:
(defthm expr/tyname-unambp-of-dimb-amb-expr/tyname (b* (((mv acl2::?erp ?expr-or-tyname ?new-table) (dimb-amb-expr/tyname expr/tyname table))) (implies (not erp) (expr/tyname-unambp expr-or-tyname))))
Theorem:
(defthm declor/absdeclor-unambp-of-dimb-amb-declor/absdeclor (b* (((mv acl2::?erp ?declor-or-absdeclor ?ident? ?new-table) (dimb-amb-declor/absdeclor declor/absdeclor table))) (implies (not erp) (declor/absdeclor-unambp declor-or-absdeclor))))