Validate expressions, declarations, statements, and related artifacts.
Since we currently have an approximate model of types, with the `unknown type' among them (see type), wherever a certain kind of type is required (e.g. an integer type), we also need to allow the unknown type, because that could the required kind of type. Our currently approximate validator must not reject valid programs, because it needs to deal with any practical programs we encounter. Eventually, when we refine our validator and our model of types to no longer be approximate and include the unknown type, we will rescind this extra allowance for the unknown type.
Each validation function takes and returns an abstract syntax entity (of the appropriate kind) and returns a transformed one (of the same kind). Currently there is no change, but soon we will be adding information to the abstract syntax.
Function:
(defun valid-expr (expr table ienv) (declare (xargs :guard (and (exprp expr) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (expr-unambp expr))) (b* (((reterr) (irr-expr) (irr-type) nil (irr-valid-table))) (expr-case expr :ident (b* (((erp type linkage uid) (valid-var expr.ident table)) (info (make-var-info :type type :linkage linkage :uid uid))) (retok (make-expr-ident :ident expr.ident :info info) type nil (valid-table-fix table))) :const (b* (((erp const type) (valid-const expr.const table ienv)) (info (make-expr-const-info :type type))) (retok (make-expr-const :const const :info info) type nil (valid-table-fix table))) :string (b* (((erp type) (valid-stringlit-list expr.strings ienv)) (info (make-expr-string-info :type type))) (retok (change-expr-string expr :info info) type nil (valid-table-fix table))) :paren (b* (((erp new-inner type types table) (valid-expr expr.inner table ienv))) (retok (expr-paren new-inner) type types table)) :gensel (b* (((erp new-control type-control types-control table) (valid-expr expr.control table ienv)) ((erp new-assocs type-alist types-assoc table) (valid-genassoc-list expr.assocs table ienv)) ((erp type) (valid-gensel expr type-control type-alist))) (retok (make-expr-gensel :control new-control :assocs new-assocs) type (union types-control types-assoc) table)) :arrsub (b* (((erp new-arg1 type-arg1 types-arg1 table) (valid-expr expr.arg1 table ienv)) ((erp new-arg2 type-arg2 types-arg2 table) (valid-expr expr.arg2 table ienv)) ((erp type) (valid-arrsub expr type-arg1 type-arg2)) (info (make-expr-arrsub-info :type type))) (retok (make-expr-arrsub :arg1 new-arg1 :arg2 new-arg2 :info info) type (union types-arg1 types-arg2) table)) :funcall (b* (((erp new-fun type-fun types-fun table) (valid-expr expr.fun table ienv)) ((erp new-args types-arg rtypes-arg table) (valid-expr-list expr.args table ienv)) ((erp type) (valid-funcall expr type-fun types-arg ienv)) (info (make-expr-funcall-info :type type))) (retok (make-expr-funcall :fun new-fun :args new-args :info info) type (union types-fun rtypes-arg) table)) :member (b* (((erp new-arg type-arg types-arg table) (valid-expr expr.arg table ienv)) ((erp type) (valid-member expr type-arg))) (retok (make-expr-member :arg new-arg :name expr.name) type types-arg table)) :memberp (b* (((erp new-arg type-arg types-arg table) (valid-expr expr.arg table ienv)) ((erp type) (valid-memberp expr type-arg))) (retok (make-expr-memberp :arg new-arg :name expr.name) type types-arg table)) :complit (b* (((erp new-type type types-type table) (valid-tyname expr.type table ienv)) ((when (type-case type :function)) (retmsg$ "The type of the compound literal ~x0 ~ is a function type." (expr-fix expr))) ((when (type-case type :void)) (retmsg$ "The type of the compound literal ~x0 ~ is void." (expr-fix expr))) (lifetime (if (> (valid-table-num-scopes table) 1) (lifetime-auto) (lifetime-static))) ((erp new-elems types-elems table) (valid-desiniter-list expr.elems type lifetime table ienv))) (retok (make-expr-complit :type new-type :elems new-elems :final-comma expr.final-comma) type (union types-type types-elems) table)) :unary (b* (((erp new-arg type-arg types-arg table) (valid-expr expr.arg table ienv)) ((erp type) (valid-unary expr expr.op type-arg ienv)) (info (make-expr-unary-info :type type))) (retok (make-expr-unary :op expr.op :arg new-arg :info info) type types-arg table)) :label-addr (retok (expr-label-addr expr.arg) (type-pointer (type-void)) nil (valid-table-fix table)) :sizeof (b* (((erp new-type type types table) (valid-tyname expr.type table ienv)) ((erp type1) (valid-sizeof/alignof expr type))) (retok (expr-sizeof new-type) type1 types table)) :alignof (b* (((erp new-type type types table) (valid-tyname expr.type table ienv)) ((erp type1) (valid-sizeof/alignof expr type))) (retok (make-expr-alignof :type new-type :uscores expr.uscores) type1 types table)) :cast (b* (((erp new-type type-cast types-cast table) (valid-tyname expr.type table ienv)) ((erp new-arg type-arg types-arg table) (valid-expr expr.arg table ienv)) ((erp type) (valid-cast expr type-cast type-arg))) (retok (make-expr-cast :type new-type :arg new-arg) type (union types-cast types-arg) table)) :binary (b* (((erp new-arg1 type-arg1 types-arg1 table) (valid-expr expr.arg1 table ienv)) ((erp new-arg2 type-arg2 types-arg2 table) (valid-expr expr.arg2 table ienv)) ((erp type) (valid-binary expr expr.op type-arg1 type-arg2 ienv)) (info (make-expr-binary-info :type type))) (retok (make-expr-binary :op expr.op :arg1 new-arg1 :arg2 new-arg2 :info info) type (union types-arg1 types-arg2) table)) :cond (b* (((erp new-test type-test types-test table) (valid-expr expr.test table ienv)) ((erp new-then type-then? types-then table) (valid-expr-option expr.then table ienv)) (type-then (or type-then? type-test)) ((erp new-else type-else types-else table) (valid-expr expr.else table ienv)) ((erp type) (valid-cond expr type-test type-then type-else ienv))) (retok (make-expr-cond :test new-test :then new-then :else new-else) type (union types-test (union types-then types-else)) table)) :comma (b* (((erp new-first & types1 table) (valid-expr expr.first table ienv)) ((erp new-next type types2 table) (valid-expr expr.next table ienv))) (retok (make-expr-comma :first new-first :next new-next) type (union types1 types2) table)) :stmt (b* (((erp new-cstmt types type? table) (valid-comp-stmt expr.stmt nil table ienv)) (type (or type? (type-void)))) (retok (expr-stmt new-cstmt) type types table)) :tycompat (b* (((erp new-type1 & types1 table) (valid-tyname expr.type1 table ienv)) ((erp new-type2 & types2 table) (valid-tyname expr.type2 table ienv))) (retok (make-expr-tycompat :type1 new-type1 :type2 new-type2) (type-sint) (union types1 types2) table)) :offsetof (b* (((erp new-type & types table) (valid-tyname expr.type table ienv)) ((erp new-member more-types table) (valid-member-designor expr.member table ienv))) (retok (make-expr-offsetof :type new-type :member new-member) (type-unknown) (union types more-types) table)) :va-arg (b* (((erp new-list & list-types table) (valid-expr expr.list table ienv)) ((erp new-type & type-types table) (valid-tyname expr.type table ienv))) (retok (make-expr-va-arg :list new-list :type new-type) (type-unknown) (union list-types type-types) table)) :extension (b* (((erp new-expr type types table) (valid-expr expr.expr table ienv))) (retok (expr-extension new-expr) type types table)) :otherwise (prog2$ (impossible) (retmsg$ "")))))
Function:
(defun valid-expr-list (exprs table ienv) (declare (xargs :guard (and (expr-listp exprs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (expr-list-unambp exprs))) (b* (((reterr) nil nil nil (irr-valid-table)) ((when (endp exprs)) (retok nil nil nil (valid-table-fix table))) ((erp new-expr type return-types table) (valid-expr (car exprs) table ienv)) ((erp new-exprs types more-return-types table) (valid-expr-list (cdr exprs) table ienv))) (retok (cons new-expr new-exprs) (cons type types) (union return-types more-return-types) table)))
Function:
(defun valid-expr-option (expr? table ienv) (declare (xargs :guard (and (expr-optionp expr?) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (expr-option-unambp expr?))) (b* (((reterr) nil nil nil (irr-valid-table))) (expr-option-case expr? :some (valid-expr expr?.val table ienv) :none (retok nil nil nil (valid-table-fix table)))))
Function:
(defun valid-const-expr (cexpr table ienv) (declare (xargs :guard (and (const-exprp cexpr) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (const-expr-unambp cexpr))) (b* (((reterr) (irr-const-expr) (irr-type) nil (irr-valid-table)) ((erp new-expr type types table) (valid-expr (const-expr->expr cexpr) table ienv))) (retok (const-expr new-expr) type types table)))
Function:
(defun valid-const-expr-option (cexpr? table ienv) (declare (xargs :guard (and (const-expr-optionp cexpr?) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (const-expr-option-unambp cexpr?))) (b* (((reterr) nil nil nil (irr-valid-table))) (const-expr-option-case cexpr? :some (valid-const-expr cexpr?.val table ienv) :none (retok nil nil nil (valid-table-fix table)))))
Function:
(defun valid-genassoc (genassoc table ienv) (declare (xargs :guard (and (genassocp genassoc) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (genassoc-unambp genassoc))) (b* (((reterr) (irr-genassoc) nil (irr-type) nil (irr-valid-table))) (genassoc-case genassoc :type (b* (((erp new-type tyname-type tyname-types table) (valid-tyname genassoc.type table ienv)) ((erp new-expr expr-type expr-types table) (valid-expr genassoc.expr table ienv))) (retok (make-genassoc-type :type new-type :expr new-expr) tyname-type expr-type (union tyname-types expr-types) table)) :default (b* (((erp new-expr expr-type expr-types table) (valid-expr genassoc.expr table ienv))) (retok (genassoc-default new-expr) nil expr-type expr-types table)))))
Function:
(defun valid-genassoc-list (genassocs table ienv) (declare (xargs :guard (and (genassoc-listp genassocs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (genassoc-list-unambp genassocs))) (b* (((reterr) nil nil nil (irr-valid-table)) ((when (endp genassocs)) (retok nil nil nil (valid-table-fix table))) ((erp new-genassoc tyname-type? expr-type types table) (valid-genassoc (car genassocs) table ienv)) ((erp new-genassocs type-alist more-types table) (valid-genassoc-list (cdr genassocs) table ienv))) (retok (cons new-genassoc new-genassocs) (acons tyname-type? expr-type type-alist) (union types more-types) table)))
Function:
(defun valid-member-designor (memdesign table ienv) (declare (xargs :guard (and (member-designorp memdesign) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (member-designor-unambp memdesign))) (b* (((reterr) (irr-member-designor) nil (irr-valid-table))) (member-designor-case memdesign :ident (retok (member-designor-fix memdesign) nil (valid-table-fix table)) :dot (b* (((erp new-member types table) (valid-member-designor memdesign.member table ienv))) (retok (make-member-designor-dot :member new-member :name memdesign.name) types table)) :sub (b* (((erp new-member types table) (valid-member-designor memdesign.member table ienv)) ((erp new-expr & more-types table) (valid-expr memdesign.index table ienv))) (retok (make-member-designor-sub :member new-member :index new-expr) (union types more-types) table)))))
Function:
(defun valid-type-spec (tyspec type? tyspecs table ienv) (declare (xargs :guard (and (type-specp tyspec) (type-optionp type?) (type-spec-listp tyspecs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (type-spec-unambp tyspec) (type-spec-list-unambp tyspecs) (not (and type? tyspecs))))) (b* (((reterr) (irr-type-spec) nil nil nil (irr-valid-table)) ((when type?) (retmsg$ "Since the type ~x0 has been determined, ~ there must be no more type specifiers, ~ but ~x1 follows instead." (type-option-fix type?) (type-spec-fix tyspec))) (same-table (valid-table-fix table)) (ext-tyspecs (rcons (type-spec-fix tyspec) (type-spec-list-fix tyspecs))) (msg-bad-preceding (msg$ "The type specifier ~x0 ~ must not be preceded by ~x1." (type-spec-fix tyspec) (type-spec-list-fix tyspecs)))) (type-spec-case tyspec :void (if (endp tyspecs) (retok (type-spec-void) (type-void) nil nil same-table) (reterr msg-bad-preceding)) :char (retok (type-spec-char) nil ext-tyspecs nil same-table) :short (retok (type-spec-short) nil ext-tyspecs nil same-table) :int (retok (type-spec-int) nil ext-tyspecs nil same-table) :long (retok (type-spec-long) nil ext-tyspecs nil same-table) :float (retok (type-spec-float) nil ext-tyspecs nil same-table) :double (retok (type-spec-double) nil ext-tyspecs nil same-table) :signed (retok (type-spec-signed tyspec.uscores) nil ext-tyspecs nil same-table) :unsigned (retok (type-spec-unsigned) nil ext-tyspecs nil same-table) :bool (if (endp tyspecs) (retok (type-spec-bool) (type-bool) nil nil same-table) (reterr msg-bad-preceding)) :complex (retok (type-spec-complex) nil ext-tyspecs nil same-table) :atomic (b* (((unless (endp tyspecs)) (reterr msg-bad-preceding)) ((erp new-type type types table) (valid-tyname tyspec.type table ienv))) (retok (type-spec-atomic new-type) type nil types table)) :struct (b* (((unless (endp tyspecs)) (reterr msg-bad-preceding)) ((erp new-spec types table) (valid-struni-spec tyspec.spec table ienv)) ((struni-spec tyspec.spec) tyspec.spec)) (retok (type-spec-struct new-spec) (type-struct tyspec.spec.name?) nil types table)) :union (b* (((unless (endp tyspecs)) (reterr msg-bad-preceding)) ((erp new-spec types table) (valid-struni-spec tyspec.spec table ienv))) (retok (type-spec-union new-spec) (type-union) nil types table)) :enum (b* (((unless (endp tyspecs)) (reterr msg-bad-preceding)) ((erp new-spec types table) (valid-enum-spec tyspec.spec table ienv))) (retok (type-spec-enum new-spec) (type-enum) nil types table)) :typedef (b* (((unless (endp tyspecs)) (reterr msg-bad-preceding)) ((mv info? -) (valid-lookup-ord tyspec.name table)) ((unless info?) (retmsg$ "The identifier ~x0 is not an in-scope ~ ordinary identifier." (ident->unwrap tyspec.name)))) (valid-ord-info-case info? :typedef (retok (type-spec-typedef tyspec.name) info?.def nil nil same-table) :otherwise (retmsg$ "The identifier ~x0 does not ~ represent a typedef."))) :int128 (retok (make-type-spec-int128 :uscoret tyspec.uscoret) nil ext-tyspecs nil same-table) :locase-float80 (retok (type-spec-locase-float80) nil ext-tyspecs nil same-table) :locase-float128 (retok (type-spec-locase-float128) nil ext-tyspecs nil same-table) :float16 (retok (type-spec-float16) nil ext-tyspecs nil same-table) :float16x (retok (type-spec-float16x) nil ext-tyspecs nil same-table) :float32 (retok (type-spec-float32) nil ext-tyspecs nil same-table) :float32x (retok (type-spec-float32x) nil ext-tyspecs nil same-table) :float64 (retok (type-spec-float64) nil ext-tyspecs nil same-table) :float64x (retok (type-spec-float64x) nil ext-tyspecs nil same-table) :float128 (retok (type-spec-float128) nil ext-tyspecs nil same-table) :float128x (retok (type-spec-float128x) nil ext-tyspecs nil same-table) :builtin-va-list (if (endp tyspecs) (retok (type-spec-builtin-va-list) (type-unknown) nil nil same-table) (reterr msg-bad-preceding)) :struct-empty (if (endp tyspecs) (retok (make-type-spec-struct-empty :attribs tyspec.attribs :name? tyspec.name?) (type-struct tyspec.name?) nil nil same-table) (reterr msg-bad-preceding)) :typeof-expr (if (endp tyspecs) (retok (type-spec-fix tyspec) (type-unknown) nil nil same-table) (reterr msg-bad-preceding)) :typeof-type (if (endp tyspecs) (retok (type-spec-fix tyspec) (type-unknown) nil nil same-table) (reterr msg-bad-preceding)) :auto-type (if (endp tyspecs) (retok (type-spec-fix tyspec) (type-unknown) nil nil same-table) (reterr msg-bad-preceding)) :otherwise (prog2$ (impossible) (retmsg$ "")))))
Function:
(defun valid-spec/qual (specqual type? tyspecs table ienv) (declare (xargs :guard (and (spec/qual-p specqual) (type-optionp type?) (type-spec-listp tyspecs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (spec/qual-unambp specqual) (type-spec-list-unambp tyspecs) (not (and type? tyspecs))))) (b* (((reterr) (irr-spec/qual) nil nil nil (irr-valid-table))) (spec/qual-case specqual :typespec (b* (((erp new-spec type? tyspecs types table) (valid-type-spec specqual.spec type? tyspecs table ienv))) (retok (spec/qual-typespec new-spec) type? tyspecs types table)) :typequal (retok (spec/qual-typequal specqual.qual) (type-option-fix type?) (type-spec-list-fix tyspecs) nil (valid-table-fix table)) :align (b* (((erp new-spec types table) (valid-align-spec specqual.spec table ienv))) (retok (spec/qual-align new-spec) (type-option-fix type?) (type-spec-list-fix tyspecs) types table)) :attrib (retok (spec/qual-attrib specqual.spec) (type-option-fix type?) (type-spec-list-fix tyspecs) nil (valid-table-fix table)))))
Function:
(defun valid-spec/qual-list (specquals type? tyspecs table ienv) (declare (xargs :guard (and (spec/qual-listp specquals) (type-optionp type?) (type-spec-listp tyspecs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (spec/qual-list-unambp specquals) (type-spec-list-unambp tyspecs) (not (and type? tyspecs))))) (b* (((reterr) nil (irr-type) nil (irr-valid-table)) ((when (endp specquals)) (cond (type? (retok nil (type-option-fix type?) nil (valid-table-fix table))) ((consp tyspecs) (b* (((erp type) (valid-type-spec-list-residual tyspecs))) (retok nil type nil (valid-table-fix table)))) (t (retmsg$ "The specifier and qualifier list ~x0 ~ contains no type specifiers." (spec/qual-list-fix specquals))))) ((erp new-specqual type? tyspecs types table) (valid-spec/qual (car specquals) type? tyspecs table ienv)) ((erp new-specquals type more-types table) (valid-spec/qual-list (cdr specquals) type? tyspecs table ienv))) (retok (cons new-specqual new-specquals) type (union types more-types) table)))
Function:
(defun valid-align-spec (align table ienv) (declare (xargs :guard (and (align-specp align) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (align-spec-unambp align))) (b* (((reterr) (irr-align-spec) nil (irr-valid-table))) (align-spec-case align :alignas-type (b* (((erp new-type type types table) (valid-tyname align.type table ienv)) ((when (type-case type :function)) (retmsg$ "In the alignment specifier ~x0, ~ the argument ~x2 is a function type." (align-spec-fix align) type))) (retok (align-spec-alignas-type new-type) types table)) :alignas-expr (b* (((erp new-expr type types table) (valid-const-expr align.expr table ienv)) ((unless (or (type-integerp type) (type-case type :unknown))) (retmsg$ "In the alignment specifier ~x0, ~ the argument has type ~x1." (align-spec-fix align) type))) (retok (align-spec-alignas-expr new-expr) types table)) :alignas-ambig (prog2$ (impossible) (retmsg$ "")))))
Function:
(defun valid-decl-spec (declspec type? tyspecs storspecs table ienv) (declare (xargs :guard (and (decl-specp declspec) (type-optionp type?) (type-spec-listp tyspecs) (stor-spec-listp storspecs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (decl-spec-unambp declspec) (type-spec-list-unambp tyspecs) (not (and type? tyspecs))))) (b* (((reterr) (irr-decl-spec) nil nil nil nil (irr-valid-table))) (decl-spec-case declspec :stoclass (retok (decl-spec-stoclass declspec.spec) (type-option-fix type?) (type-spec-list-fix tyspecs) (rcons declspec.spec (stor-spec-list-fix storspecs)) nil (valid-table-fix table)) :typespec (b* (((erp new-spec type? tyspecs types table) (valid-type-spec declspec.spec type? tyspecs table ienv))) (retok (decl-spec-typespec new-spec) type? tyspecs (stor-spec-list-fix storspecs) types table)) :typequal (retok (decl-spec-typequal declspec.qual) (type-option-fix type?) (type-spec-list-fix tyspecs) (stor-spec-list-fix storspecs) nil (valid-table-fix table)) :function (retok (decl-spec-function declspec.spec) (type-option-fix type?) (type-spec-list-fix tyspecs) (stor-spec-list-fix storspecs) nil (valid-table-fix table)) :align (b* (((erp new-spec types table) (valid-align-spec declspec.spec table ienv))) (retok (decl-spec-align new-spec) (type-option-fix type?) (type-spec-list-fix tyspecs) (stor-spec-list-fix storspecs) types table)) :attrib (retok (decl-spec-attrib declspec.spec) (type-option-fix type?) (type-spec-list-fix tyspecs) (stor-spec-list-fix storspecs) nil (valid-table-fix table)) :stdcall (retok (decl-spec-stdcall) (type-option-fix type?) (type-spec-list-fix tyspecs) (stor-spec-list-fix storspecs) nil (valid-table-fix table)) :declspec (retok (decl-spec-declspec declspec.arg) (type-option-fix type?) (type-spec-list-fix tyspecs) (stor-spec-list-fix storspecs) nil (valid-table-fix table)))))
Function:
(defun valid-decl-spec-list (declspecs type? tyspecs storspecs table ienv) (declare (xargs :guard (and (decl-spec-listp declspecs) (type-optionp type?) (type-spec-listp tyspecs) (stor-spec-listp storspecs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (decl-spec-list-unambp declspecs) (type-spec-list-unambp tyspecs) (not (and type? tyspecs))))) (b* (((reterr) nil (irr-type) nil nil (irr-valid-table)) ((when (endp declspecs)) (cond (type? (retok nil (type-option-fix type?) (stor-spec-list-fix storspecs) nil (valid-table-fix table))) ((consp tyspecs) (b* (((erp type) (valid-type-spec-list-residual tyspecs))) (retok nil type (stor-spec-list-fix storspecs) nil (valid-table-fix table)))) (t (retmsg$ "The declaration specifiers ~x0 ~ contain no type specifiers." (decl-spec-list-fix declspecs))))) ((erp new-declspec type? tyspecs storspecs types table) (valid-decl-spec (car declspecs) type? tyspecs storspecs table ienv)) ((erp new-declspecs type storspecs more-types table) (valid-decl-spec-list (cdr declspecs) type? tyspecs storspecs table ienv))) (retok (cons new-declspec new-declspecs) type storspecs (union types more-types) table)))
Function:
(defun valid-initer (initer target-type lifetime table ienv) (declare (xargs :guard (and (initerp initer) (typep target-type) (lifetimep lifetime) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (initer-unambp initer) (not (type-case target-type :function)) (not (type-case target-type :void))))) (b* (((reterr) (irr-initer) nil (irr-valid-table))) (cond ((type-case target-type :unknown) (initer-case initer :single (b* (((erp new-expr & types table) (valid-expr initer.expr table ienv))) (retok (initer-single new-expr) types table)) :list (b* (((erp new-elems types table) (valid-desiniter-list initer.elems (type-unknown) lifetime table ienv))) (retok (make-initer-list :elems new-elems :final-comma initer.final-comma) types table)))) ((type-scalarp target-type) (b* (((erp expr) (b* (((reterr) (irr-expr))) (initer-case initer :single (retok initer.expr) :list (b* (((unless (and (consp initer.elems) (endp (cdr initer.elems)))) (retmsg$ "The initializer list ~x0 ~ for the target type ~x1 ~ is not a singleton." (initer-fix initer) (type-fix target-type))) ((desiniter desiniter) (car initer.elems)) ((unless (endp desiniter.designors)) (retmsg$ "The initializer list ~x0 ~ for the target type ~x1 ~ is a singleton ~ but it has designators." (initer-fix initer) (type-fix target-type))) ((unless (initer-case desiniter.initer :single)) (retmsg$ "The initializer list ~x0 ~ for the target type ~x1 ~ is a singleton without designators ~ but the inner initializer ~ is not a single expression." (initer-fix initer) (type-fix target-type)))) (retok (initer-single->expr desiniter.initer)))))) ((erp new-expr init-type types table) (valid-expr expr table ienv)) (type (type-fpconvert (type-apconvert init-type))) ((unless (or (and (type-arithmeticp target-type) (or (type-arithmeticp type) (type-case type :unknown))) (and (type-case target-type :bool) (or (type-case type :pointer) (type-case type :unknown))) (and (type-case target-type :pointer) (or (and (type-case type :pointer) (let ((target-type-to (type-pointer->to target-type)) (type-to (type-pointer->to type))) (or (type-compatiblep target-type-to type-to ienv) (and (type-case target-type-to :void) (not (type-case type-to :function))) (and (type-case type-to :void) (not (type-case target-type-to :function)))))) (type-case type :unknown) (expr-null-pointer-constp expr type))))) (retmsg$ "The initializer ~x0 for the target type ~x1 ~ has type ~x2." (initer-fix initer) (type-fix target-type) init-type)) (new-initer (initer-case initer :single (initer-single new-expr) :list (make-initer-list :elems (list (make-desiniter :designors nil :initer (initer-single new-expr))) :final-comma initer.final-comma)))) (retok new-initer types table))) ((and (or (type-case target-type :struct) (type-case target-type :union)) (initer-case initer :single) (lifetime-case lifetime :auto)) (b* (((erp new-expr type types table) (valid-expr (initer-single->expr initer) table ienv)) ((unless (or (type-equiv type target-type) (type-case type :unknown))) (retmsg$ "The initializer ~x0 for the target type ~x1 ~ of an object in automatic storage has type ~x2.~%" (initer-fix initer) (type-fix target-type) table))) (retok (initer-single new-expr) types table))) ((and (type-case target-type :array) (initer-case initer :single) (expr-case (initer-single->expr initer) :string)) (b* (((erp type) (valid-stringlit-list (expr-string->strings (initer-single->expr initer)) ienv)) (info (make-expr-string-info :type type))) (retok (initer-single (make-expr-string :strings (expr-string->strings (initer-single->expr initer)) :info info)) nil (valid-table-fix table)))) ((and (or (type-aggregatep target-type) (type-case target-type :union)) (initer-case initer :list)) (b* (((erp new-elems types table) (valid-desiniter-list (initer-list->elems initer) target-type lifetime table ienv))) (retok (make-initer-list :elems new-elems :final-comma (initer-list->final-comma initer)) types table))) (t (retmsg$ "The initializer ~x0 for the target type ~x1 is disallowed." (initer-fix initer) (type-fix target-type))))))
Function:
(defun valid-initer-option (initer? target-type lifetime? table ienv) (declare (xargs :guard (and (initer-optionp initer?) (typep target-type) (lifetime-optionp lifetime?) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (initer-option-unambp initer?) (or (not initer?) lifetime?) (or (not initer?) (not (type-case target-type :function))) (or (not initer?) (not (type-case target-type :void)))))) (b* (((reterr) nil nil (irr-valid-table))) (initer-option-case initer? :some (valid-initer initer?.val target-type (lifetime-option-fix lifetime?) table ienv) :none (retok nil nil (valid-table-fix table)))))
Function:
(defun valid-desiniter (desiniter target-type lifetime table ienv) (declare (xargs :guard (and (desiniterp desiniter) (typep target-type) (lifetimep lifetime) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (desiniter-unambp desiniter) (not (type-case target-type :function)) (not (type-case target-type :void))))) (b* (((reterr) (irr-desiniter) nil (irr-valid-table)) ((desiniter desiniter) desiniter) ((erp new-design initer-type types table) (valid-designor-list desiniter.designors target-type table ienv)) ((erp new-init more-types table) (valid-initer desiniter.initer initer-type lifetime table ienv))) (retok (make-desiniter :designors new-design :initer new-init) (union types more-types) table)))
Function:
(defun valid-desiniter-list (desiniters target-type lifetime table ienv) (declare (xargs :guard (and (desiniter-listp desiniters) (typep target-type) (lifetimep lifetime) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (desiniter-list-unambp desiniters) (not (type-case target-type :function)) (not (type-case target-type :void))))) (b* (((reterr) nil nil (irr-valid-table)) ((when (endp desiniters)) (retok nil nil (valid-table-fix table))) (target-type (if (type-case target-type :array (or (type-case target-type.of :array) (type-case target-type.of :struct) (type-case target-type.of :union) (type-case target-type.of :unknown)) :struct t :union t :otherwise nil) (type-unknown) target-type)) ((erp new-desiniter types table) (valid-desiniter (car desiniters) target-type lifetime table ienv)) ((erp new-desiniters more-types table) (valid-desiniter-list (cdr desiniters) target-type lifetime table ienv))) (retok (cons new-desiniter new-desiniters) (union types more-types) table)))
Function:
(defun valid-designor (designor target-type table ienv) (declare (xargs :guard (and (designorp designor) (typep target-type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (designor-unambp designor) (not (type-case target-type :function)) (not (type-case target-type :void))))) (b* (((reterr) (irr-designor) (irr-type) nil (irr-valid-table))) (designor-case designor :sub (b* (((erp new-index index-type index-types table) (valid-const-expr designor.index table ienv)) ((erp new-range? range?-type? range?-types table) (valid-const-expr-option designor.range? table ienv)) ((unless (or (type-integerp index-type) (type-case index-type :unknown))) (retmsg$ "The first or only index of the designator ~x0 ~ has type ~x1." (designor-fix designor) index-type)) ((unless (or (not range?-type?) (type-integerp range?-type?) (type-case range?-type? :unknown))) (retmsg$ "The second index of the designator ~x0 ~ has type ~x1." (designor-fix designor) range?-type?)) ((when (type-case target-type :unknown)) (retok (make-designor-sub :index new-index :range? new-range?) (type-unknown) (union index-types range?-types) table)) ((unless (type-case target-type :array)) (retmsg$ "The target type of the designator ~x0 is ~x1." (designor-fix designor) (type-fix target-type))) (element-type (type-array->of target-type)) ((when (or (type-case element-type :function) (type-case element-type :void))) (retmsg$ "The result of applying the designator ~x0 to type ~x1 is ~x2." (designor-fix designor) (type-fix target-type) element-type))) (retok (make-designor-sub :index new-index :range? new-range?) element-type (union index-types range?-types) table)) :dot (b* (((unless (or (type-case target-type :struct) (type-case target-type :union) (type-case target-type :unknown))) (retmsg$ "The target type of the designator ~x0 is ~x1." (designor-fix designor) (type-fix target-type)))) (retok (designor-dot designor.name) (type-unknown) nil (valid-table-fix table))))))
Function:
(defun valid-designor-list (designors target-type table ienv) (declare (xargs :guard (and (designor-listp designors) (typep target-type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (and (designor-list-unambp designors) (not (type-case target-type :function)) (not (type-case target-type :void))))) (b* (((reterr) nil (irr-type) nil (irr-valid-table)) ((when (endp designors)) (type-case target-type :array (if (or (type-case target-type.of :function) (type-case target-type.of :void)) (retmsg$ "The result of applying the empty designator list to type ~x0 is ~x1." (type-fix target-type) target-type.of) (retok nil target-type.of nil (valid-table-fix table))) :otherwise (retok nil (type-unknown) nil (valid-table-fix table)))) ((erp new-designor target-type types table) (valid-designor (car designors) target-type table ienv)) ((when (endp (cdr designors))) (retok (list new-designor) target-type types table)) ((erp new-designors target-type more-types table) (valid-designor-list (cdr designors) target-type table ienv)) ((unless (mbt (and (not (type-case target-type :function)) (not (type-case target-type :void))))) (prog2$ (impossible) (retmsg$ "")))) (retok (cons new-designor new-designors) target-type (union types more-types) table)))
Function:
(defun valid-declor (declor fundef-params-p type table ienv) (declare (xargs :guard (and (declorp declor) (booleanp fundef-params-p) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (declor-unambp declor))) (b* (((reterr) (irr-declor) (irr-type) (irr-ident) nil (irr-valid-table)) ((declor declor) declor) (type (make-pointers-to declor.pointers type)) ((erp new-dirdeclor type ident types table) (valid-dirdeclor declor.direct fundef-params-p type table ienv))) (retok (make-declor :pointers declor.pointers :direct new-dirdeclor) type ident types table)))
Function:
(defun valid-declor-option (declor? type table ienv) (declare (xargs :guard (and (declor-optionp declor?) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (declor-option-unambp declor?))) (b* (((reterr) nil (irr-type) nil nil (irr-valid-table))) (declor-option-case declor? :none (retok nil (type-fix type) nil nil (valid-table-fix table)) :some (b* (((erp new-declor type ident types table) (valid-declor declor?.val nil type table ienv))) (retok new-declor type ident types table)))))
Function:
(defun valid-dirdeclor (dirdeclor fundef-params-p type table ienv) (declare (xargs :guard (and (dirdeclorp dirdeclor) (booleanp fundef-params-p) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (dirdeclor-unambp dirdeclor))) (b* (((reterr) (irr-dirdeclor) (irr-type) (irr-ident) nil (irr-valid-table))) (dirdeclor-case dirdeclor :ident (retok (dirdeclor-ident dirdeclor.ident) (type-fix type) dirdeclor.ident nil (valid-table-fix table)) :paren (b* (((erp new-declor type ident types table) (valid-declor dirdeclor.inner fundef-params-p type table ienv))) (retok (dirdeclor-paren new-declor) type ident types table)) :array (b* ((type (make-type-array :of type)) ((erp new-dirdeclor type ident types table) (valid-dirdeclor dirdeclor.declor fundef-params-p type table ienv)) ((erp new-expr? index-type? more-types table) (valid-expr-option dirdeclor.size? table ienv)) ((when (and index-type? (not (type-integerp index-type?)) (not (type-case index-type? :unknown)))) (retmsg$ "The index expression ~ of the direct declarator ~x0 ~ has type ~x1." (dirdeclor-fix dirdeclor) index-type?))) (retok (make-dirdeclor-array :declor new-dirdeclor :qualspecs dirdeclor.qualspecs :size? new-expr?) type ident (union types more-types) table)) :array-static1 (b* ((type (make-type-array :of type)) ((erp new-dirdeclor type ident types table) (valid-dirdeclor dirdeclor.declor fundef-params-p type table ienv)) ((erp new-expr index-type more-types table) (valid-expr dirdeclor.size table ienv)) ((unless (or (type-integerp index-type) (type-case index-type :unknown))) (retmsg$ "The index expression ~ of the direct declarator ~x0 ~ has type ~x1." (dirdeclor-fix dirdeclor) index-type))) (retok (make-dirdeclor-array-static1 :declor new-dirdeclor :qualspecs dirdeclor.qualspecs :size new-expr) type ident (union types more-types) table)) :array-static2 (b* ((type (make-type-array :of type)) ((erp new-dirdeclor type ident types table) (valid-dirdeclor dirdeclor.declor fundef-params-p type table ienv)) ((erp new-expr index-type more-types table) (valid-expr dirdeclor.size table ienv)) ((unless (or (type-integerp index-type) (type-case index-type :unknown))) (retmsg$ "The index expression ~ of the direct declarator ~x0 ~ has type ~x1." (dirdeclor-fix dirdeclor) index-type))) (retok (make-dirdeclor-array-static2 :declor new-dirdeclor :qualspecs dirdeclor.qualspecs :size new-expr) type ident (union types more-types) table)) :array-star (b* ((type (make-type-array :of type)) ((erp new-dirdeclor type ident types table) (valid-dirdeclor dirdeclor.declor fundef-params-p type table ienv))) (retok (make-dirdeclor-array-star :declor new-dirdeclor :qualspecs dirdeclor.qualspecs) type ident types table)) :function-params (b* (((when (or (type-case type :function) (type-case type :array))) (retmsg$ "The direct declarator ~x0 has type ~x1." (dirdeclor-fix dirdeclor) (type-fix type))) (outermost-fundef-params-p (and fundef-params-p (not (dirdeclor-has-params-p dirdeclor.declor)))) (table (valid-push-scope table)) ((erp new-params type-params return-types0 table) (b* (((reterr) nil (irr-type-params) nil table) ((when (equal dirdeclor.params (list (make-param-declon :specs (list (decl-spec-typespec (type-spec-void))) :declor (param-declor-none) :attribs nil)))) (retok dirdeclor.params (make-type-params-prototype :params nil :ellipsis nil) nil table)) ((erp new-params types return-types table) (valid-param-declon-list dirdeclor.params outermost-fundef-params-p table ienv))) (retok new-params (make-type-params-prototype :params types :ellipsis dirdeclor.ellipsis) return-types table))) (table (if outermost-fundef-params-p table (valid-pop-scope table)) ) (type (make-type-function :ret type :params type-params)) ((erp new-dirdeclor type ident return-types1 table) (valid-dirdeclor dirdeclor.declor fundef-params-p type table ienv))) (retok (make-dirdeclor-function-params :declor new-dirdeclor :params new-params :ellipsis dirdeclor.ellipsis) type ident (union return-types0 return-types1) table)) :function-names (b* (((when (or (type-case type :function) (type-case type :array))) (retmsg$ "The direct declarator ~x0 has type ~x1." (dirdeclor-fix dirdeclor) (type-fix type))) (outermost-fundef-params-p (and fundef-params-p (not (dirdeclor-has-params-p dirdeclor)))) ((erp type table) (b* (((reterr) (irr-type) table)) (if fundef-params-p (if (no-duplicatesp-equal dirdeclor.names) (retok (make-type-function :ret type :params (make-type-params-old-style :params (make-list (len dirdeclor.names) :initial-element (type-unknown)))) (valid-push-scope table)) (retmsg$ "The list of parameter names ~ in the function declarator ~x0 ~ has duplicates." (dirdeclor-fix dirdeclor))) (if (endp dirdeclor.names) (retok (make-type-function :ret type :params (type-params-unspecified)) table) (retmsg$ "A non-empty list of parameter names ~ occurs in a function declarator ~x0 ~ that is not part of a function definition." (dirdeclor-fix dirdeclor)))))) ((erp new-dirdeclor type ident types table) (valid-dirdeclor dirdeclor.declor outermost-fundef-params-p type table ienv))) (retok (make-dirdeclor-function-names :declor new-dirdeclor :names dirdeclor.names) type ident types table)))))
Function:
(defun valid-absdeclor (absdeclor type table ienv) (declare (xargs :guard (and (absdeclorp absdeclor) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (absdeclor-unambp absdeclor))) (b* (((reterr) (irr-absdeclor) (irr-type) nil (irr-valid-table)) ((absdeclor absdeclor) absdeclor) (type (make-pointers-to absdeclor.pointers type)) ((erp new-direct? type types table) (valid-dirabsdeclor-option absdeclor.direct? type table ienv))) (retok (make-absdeclor :pointers absdeclor.pointers :direct? new-direct?) type types table)))
Function:
(defun valid-absdeclor-option (absdeclor? type table ienv) (declare (xargs :guard (and (absdeclor-optionp absdeclor?) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (absdeclor-option-unambp absdeclor?))) (b* (((reterr) nil (irr-type) nil (irr-valid-table))) (absdeclor-option-case absdeclor? :none (retok nil (type-fix type) nil (valid-table-fix table)) :some (valid-absdeclor absdeclor?.val type table ienv))))
Function:
(defun valid-dirabsdeclor (dirabsdeclor type table ienv) (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (dirabsdeclor-unambp dirabsdeclor))) (b* (((reterr) (irr-dirabsdeclor) (irr-type) nil (irr-valid-table))) (dirabsdeclor-case dirabsdeclor :paren (b* (((erp new-absdeclor type types table) (valid-absdeclor dirabsdeclor.inner type table ienv))) (retok (dirabsdeclor-paren new-absdeclor) type types table)) :array (b* ((type (make-type-array :of type)) ((erp new-declor? type types table) (valid-dirabsdeclor-option dirabsdeclor.declor? type table ienv)) ((erp new-size? index-type? more-types table) (valid-expr-option dirabsdeclor.size? table ienv)) ((when (and index-type? (not (type-integerp index-type?)) (not (type-case index-type? :unknown)))) (retmsg$ "The index expression ~ of the direct abstract declarator ~x0 ~ has type ~x1." (dirabsdeclor-fix dirabsdeclor) index-type?))) (retok (make-dirabsdeclor-array :declor? new-declor? :qualspecs dirabsdeclor.qualspecs :size? new-size?) type (union types more-types) table)) :array-static1 (b* ((type (make-type-array :of type)) ((erp new-declor? type types table) (valid-dirabsdeclor-option dirabsdeclor.declor? type table ienv)) ((erp new-size index-type more-types table) (valid-expr dirabsdeclor.size table ienv)) ((unless (or (type-integerp index-type) (type-case index-type :unknown))) (retmsg$ "The index expression ~ of the direct abstract declarator ~x0 ~ has type ~x1." (dirabsdeclor-fix dirabsdeclor) index-type))) (retok (make-dirabsdeclor-array-static1 :declor? new-declor? :qualspecs dirabsdeclor.qualspecs :size new-size) type (union types more-types) table)) :array-static2 (b* ((type (make-type-array :of type)) ((erp new-declor? type types table) (valid-dirabsdeclor-option dirabsdeclor.declor? type table ienv)) ((erp new-size index-type more-types table) (valid-expr dirabsdeclor.size table ienv)) ((unless (or (type-integerp index-type) (type-case index-type :unknown))) (retmsg$ "The index expression ~ of the direct abstract declarator ~x0 ~ has type ~x1." (dirabsdeclor-fix dirabsdeclor) index-type))) (retok (make-dirabsdeclor-array-static2 :declor? new-declor? :qualspecs dirabsdeclor.qualspecs :size new-size) type (union types more-types) table)) :array-star (b* ((type (make-type-array :of type)) ((erp new-declor? type types table) (valid-dirabsdeclor-option dirabsdeclor.declor? type table ienv))) (retok (dirabsdeclor-array-star new-declor?) type types table)) :function (b* (((when (or (type-case type :function) (type-case type :array))) (retmsg$ "The direct abstract declarator ~x0 ~ has type ~x1." (dirabsdeclor-fix dirabsdeclor) (type-fix type))) (table (valid-push-scope table)) ((erp new-params type-params return-types0 table) (b* (((reterr) nil (irr-type-params) nil table) ((when (equal dirabsdeclor.params (list (make-param-declon :specs (list (decl-spec-typespec (type-spec-void))) :declor (param-declor-none) :attribs nil)))) (retok dirabsdeclor.params (make-type-params-prototype :params nil :ellipsis nil) nil table)) ((erp new-params types return-types table) (valid-param-declon-list dirabsdeclor.params nil table ienv))) (retok new-params (make-type-params-prototype :params types :ellipsis dirabsdeclor.ellipsis) return-types table))) (table (valid-pop-scope table)) (type (make-type-function :ret type :params type-params)) ((erp new-declor? type return-types1 table) (valid-dirabsdeclor-option dirabsdeclor.declor? type table ienv))) (retok (make-dirabsdeclor-function :declor? new-declor? :params new-params :ellipsis dirabsdeclor.ellipsis) type (union return-types0 return-types1) table)) :dummy-base (prog2$ (impossible) (retmsg$ "")))))
Function:
(defun valid-dirabsdeclor-option (dirabsdeclor? type table ienv) (declare (xargs :guard (and (dirabsdeclor-optionp dirabsdeclor?) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (dirabsdeclor-option-unambp dirabsdeclor?))) (b* (((reterr) nil (irr-type) nil (irr-valid-table))) (dirabsdeclor-option-case dirabsdeclor? :none (retok nil (type-fix type) nil (valid-table-fix table)) :some (valid-dirabsdeclor dirabsdeclor?.val type table ienv))))
Function:
(defun valid-param-declon (paramdecl fundef-params-p table ienv) (declare (xargs :guard (and (param-declonp paramdecl) (booleanp fundef-params-p) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (param-declon-unambp paramdecl))) (b* (((reterr) (irr-param-declon) (irr-type) nil (irr-valid-table)) ((param-declon paramdecl) paramdecl) ((erp new-specs type storspecs types table) (valid-decl-spec-list paramdecl.specs nil nil nil table ienv)) ((unless (or (endp storspecs) (stor-spec-list-register-p storspecs))) (retmsg$ "The parameter declaration ~x0 ~ has storage class specifiers ~x1." (param-declon-fix paramdecl) (stor-spec-list-fix storspecs))) ((erp new-decl type ident? more-types uid? table) (valid-param-declor paramdecl.declor type table ienv)) ((when (and fundef-params-p (not ident?))) (retmsg$ "The parameter declaration ~x0 ~ is for a function definition but has no identifier." (param-declon-fix paramdecl))) (type (type-case type :array (make-type-pointer :to type.of) :function (make-type-pointer :to type) :otherwise type)) ((when (not ident?)) (retok (make-param-declon :specs new-specs :declor new-decl :attribs paramdecl.attribs) type (union types more-types) table)) (ord-info (make-valid-ord-info-objfun :type type :linkage (linkage-none) :defstatus (valid-defstatus-defined) :uid uid?)) ((mv info? currentp) (valid-lookup-ord ident? table)) ((when (and info? currentp)) (retmsg$ "The parameter declared in ~x0 ~ in already declared in the current scope ~ with associated information ~x1." (param-declon-fix paramdecl) info?)) (table (valid-add-ord ident? ord-info table) )) (retok (make-param-declon :specs new-specs :declor new-decl :attribs paramdecl.attribs) type (union types more-types) table)))
Function:
(defun valid-param-declon-list (paramdecls fundef-params-p table ienv) (declare (xargs :guard (and (param-declon-listp paramdecls) (booleanp fundef-params-p) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (param-declon-list-unambp paramdecls))) (b* (((reterr) nil nil nil (irr-valid-table)) ((when (endp paramdecls)) (retok nil nil nil (valid-table-fix table))) ((erp new-paramdecl type return-types0 table) (valid-param-declon (car paramdecls) fundef-params-p table ienv)) ((erp new-paramdecls types return-types1 table) (valid-param-declon-list (cdr paramdecls) fundef-params-p table ienv))) (retok (cons new-paramdecl new-paramdecls) (cons type types) (union return-types0 return-types1) table)))
Function:
(defun valid-param-declor (paramdeclor type table ienv) (declare (xargs :guard (and (param-declorp paramdeclor) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (param-declor-unambp paramdeclor))) (b* (((reterr) (irr-param-declor) (irr-type) (irr-ident) nil nil (irr-valid-table))) (param-declor-case paramdeclor :nonabstract (b* (((erp new-declor type ident types table) (valid-declor paramdeclor.declor nil type table ienv)) ((mv uid table) (valid-get-fresh-uid ident (linkage-none) table)) (info (make-param-declor-nonabstract-info :type type :uid uid))) (retok (make-param-declor-nonabstract :declor new-declor :info info) type ident types uid table)) :abstract (b* (((erp new-absdeclor type types table) (valid-absdeclor paramdeclor.declor type table ienv))) (retok (param-declor-abstract new-absdeclor) type nil types nil table)) :none (retok (param-declor-none) (type-fix type) nil nil nil (valid-table-fix table)) :ambig (prog2$ (impossible) (retmsg$ "")))))
Function:
(defun valid-tyname (tyname table ienv) (declare (xargs :guard (and (tynamep tyname) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (tyname-unambp tyname))) (b* (((reterr) (irr-tyname) (irr-type) nil (irr-valid-table)) ((tyname tyname) tyname) ((erp new-specquals type types table) (valid-spec/qual-list tyname.specquals nil nil table ienv)) ((erp new-decl? type more-types table) (valid-absdeclor-option tyname.declor? type table ienv)) (info (make-tyname-info :type type))) (retok (make-tyname :specquals new-specquals :declor? new-decl? :info info) type (union types more-types) table)))
Function:
(defun valid-struni-spec (struni-spec table ienv) (declare (xargs :guard (and (struni-specp struni-spec) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (struni-spec-unambp struni-spec))) (b* (((reterr) (irr-struni-spec) nil (irr-valid-table)) ((struni-spec struni-spec) struni-spec) ((when (and (not struni-spec.name?) (endp struni-spec.members))) (retmsg$ "The structure or union specifier ~x0 ~ has no name and no members." (struni-spec-fix struni-spec))) ((erp new-members types table) (valid-struct-declon-list struni-spec.members nil table ienv))) (retok (make-struni-spec :attribs struni-spec.attribs :name? struni-spec.name? :members new-members) types table)))
Function:
(defun valid-struct-declon (structdeclon previous table ienv) (declare (xargs :guard (and (struct-declonp structdeclon) (ident-listp previous) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (struct-declon-unambp structdeclon))) (b* (((reterr) (irr-struct-declon) nil nil (irr-valid-table))) (struct-declon-case structdeclon :member (b* (((erp new-specquals type types table) (valid-spec/qual-list structdeclon.specquals nil nil table ienv)) ((erp new-declors previous more-types table) (valid-struct-declor-list structdeclon.declors previous type table ienv))) (retok (make-struct-declon-member :extension structdeclon.extension :specquals new-specquals :declors new-declors :attribs structdeclon.attribs) previous (union types more-types) table)) :statassert (b* (((erp new-statassert types table) (valid-statassert structdeclon.statassert table ienv))) (retok (struct-declon-statassert new-statassert) (ident-list-fix previous) types table)) :empty (retok (struct-declon-empty) (ident-list-fix previous) nil (valid-table-fix table)))))
Function:
(defun valid-struct-declon-list (structdeclons previous table ienv) (declare (xargs :guard (and (struct-declon-listp structdeclons) (ident-listp previous) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (struct-declon-list-unambp structdeclons))) (b* (((reterr) nil nil (irr-valid-table)) ((when (endp structdeclons)) (retok nil nil (valid-table-fix table))) ((erp new-structdeclon previous types table) (valid-struct-declon (car structdeclons) previous table ienv)) ((erp new-structdeclons more-types table) (valid-struct-declon-list (cdr structdeclons) previous table ienv))) (retok (cons new-structdeclon new-structdeclons) (union types more-types) table)))
Function:
(defun valid-struct-declor (structdeclor previous type table ienv) (declare (xargs :guard (and (struct-declorp structdeclor) (ident-listp previous) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (struct-declor-unambp structdeclor))) (b* (((reterr) (irr-struct-declor) nil nil (irr-valid-table)) ((struct-declor structdeclor) structdeclor) ((when (and (not structdeclor.declor?) (not structdeclor.expr?))) (retmsg$ "The structure declarator ~x0 is empty." (struct-declor-fix structdeclor))) ((erp new-declor? & ident? types table) (valid-declor-option structdeclor.declor? type table ienv)) (previous (ident-list-fix previous)) ((when (and ident? (member-equal ident? previous))) (retmsg$ "The structure declarator ~x0 ~ duplicates the member name." (struct-declor-fix structdeclor))) (previous (if ident? (rcons ident? previous) previous)) ((erp new-expr? width-type? more-types table) (valid-const-expr-option structdeclor.expr? table ienv)) ((when (and width-type? (not (type-integerp width-type?)) (not (type-case width-type? :unknown)))) (retmsg$ "The structure declarator ~x0 ~ has a width of type ~x1." (struct-declor-fix structdeclor) width-type?))) (retok (make-struct-declor :declor? new-declor? :expr? new-expr?) previous (union types more-types) table)))
Function:
(defun valid-struct-declor-list (structdeclors previous type table ienv) (declare (xargs :guard (and (struct-declor-listp structdeclors) (ident-listp previous) (typep type) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (struct-declor-list-unambp structdeclors))) (b* (((reterr) nil nil nil (irr-valid-table)) ((when (endp structdeclors)) (retok nil (ident-list-fix previous) nil (valid-table-fix table))) ((erp new-structdeclor previous types table) (valid-struct-declor (car structdeclors) previous type table ienv)) ((erp new-structdeclors previous more-types table) (valid-struct-declor-list (cdr structdeclors) previous type table ienv))) (retok (cons new-structdeclor new-structdeclors) previous (union types more-types) table)))
Function:
(defun valid-enum-spec (enumspec table ienv) (declare (xargs :guard (and (enum-specp enumspec) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (enum-spec-unambp enumspec))) (b* (((reterr) (irr-enum-spec) nil (irr-valid-table)) ((enum-spec enumspec) enumspec) ((when (and (not enumspec.name?) (endp enumspec.enumers))) (retmsg$ "The enumeration specifier ~x0 ~ has no name and no enumerators." (enum-spec-fix enumspec))) ((erp new-enumers types table) (valid-enumer-list enumspec.enumers table ienv))) (retok (make-enum-spec :name? enumspec.name? :enumers new-enumers :final-comma enumspec.final-comma) types table)))
Function:
(defun valid-enumer (enumer table ienv) (declare (xargs :guard (and (enumerp enumer) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (enumer-unambp enumer))) (b* (((reterr) (irr-enumer) nil (irr-valid-table)) ((enumer enumer) enumer) ((mv info? currentp) (valid-lookup-ord enumer.name table)) ((when (and info? currentp)) (retmsg$ "The enumerator declared in ~x0 ~ in already declared in the current scope ~ with associated information ~x1." (enumer-fix enumer) info?)) (table (valid-add-ord enumer.name (valid-ord-info-enumconst) table) ) ((erp new-value? type? types table) (valid-const-expr-option enumer.value? table ienv)) ((when (and type? (not (type-integerp type?)) (not (type-case type? :unknown)))) (retmsg$ "The value of the numerator ~x0 has type ~x1." (enumer-fix enumer) type?))) (retok (make-enumer :name enumer.name :value? new-value?) types table)))
Function:
(defun valid-enumer-list (enumers table ienv) (declare (xargs :guard (and (enumer-listp enumers) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (enumer-list-unambp enumers))) (b* (((reterr) nil nil (irr-valid-table)) ((when (endp enumers)) (retok nil nil (valid-table-fix table))) ((erp new-enumer types table) (valid-enumer (car enumers) table ienv)) ((erp new-enumers more-types table) (valid-enumer-list (cdr enumers) table ienv))) (retok (cons new-enumer new-enumers) (union types more-types) table)))
Function:
(defun valid-statassert (statassert table ienv) (declare (xargs :guard (and (statassertp statassert) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (statassert-unambp statassert))) (b* (((reterr) (irr-statassert) nil (irr-valid-table)) ((statassert statassert) statassert) ((erp new-test type types table) (valid-const-expr statassert.test table ienv)) ((unless (or (type-integerp type) (type-case type :unknown))) (retmsg$ "The expression in the static assertion declaration ~x0 ~ has type ~x1." (statassert-fix statassert) type)) ((erp &) (valid-stringlit-list statassert.message ienv))) (retok (make-statassert :test new-test :message statassert.message) types table)))
Function:
(defun valid-init-declor (initdeclor type storspecs table ienv) (declare (xargs :guard (and (init-declorp initdeclor) (typep type) (stor-spec-listp storspecs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (init-declor-unambp initdeclor))) (let ((__function__ 'valid-init-declor)) (declare (ignorable __function__)) (b* (((reterr) (irr-init-declor) nil (irr-valid-table)) ((valid-table table) table) ((init-declor initdeclor) initdeclor) ((erp new-declor type ident types table) (valid-declor initdeclor.declor nil type table ienv)) ((erp typedefp linkage lifetime?) (valid-stor-spec-list storspecs ident type nil table)) ((when typedefp) (b* (((when initdeclor.initer?) (retmsg$ "The typedef name ~x0 ~ has an initializer ~x1." ident initdeclor.initer?)) ((mv info? currentp) (valid-lookup-ord ident table)) ((when (and info? currentp (or (not (valid-ord-info-case info? :typedef)) (not (type-compatiblep (valid-ord-info-typedef->def info?) type ienv))))) (retmsg$ "The typedef name ~x0 ~ is already declared in the current scope ~ with associated information ~x1." ident info?)) (table (valid-add-ord ident (valid-ord-info-typedef type) table) ) (anno-info (make-init-declor-info :type type :typedefp t :uid? nil))) (retok (make-init-declor :declor new-declor :asm? initdeclor.asm? :attribs initdeclor.attribs :initer? nil :info anno-info) types table))) ((when (and initdeclor.initer? (or (type-case type :function) (type-case type :void)))) (retmsg$ "The identifier ~x0 has type ~x1, ~ which disallows the initializer, ~ but the initializer ~x2 is present." ident type initdeclor.initer?)) ((mv info? currentp) (valid-lookup-ord ident table)) (defstatus (if (type-case type :function) (valid-defstatus-undefined) (if (> (valid-table-num-scopes table) 1) (if (linkage-case linkage :external) (valid-defstatus-undefined) (valid-defstatus-defined)) (if initdeclor.initer? (valid-defstatus-defined) (if (member-equal (stor-spec-extern) (stor-spec-list-fix storspecs)) (valid-defstatus-undefined) (valid-defstatus-tentative)))))) ((mv uid table) (valid-get-fresh-uid ident linkage table)) (new-info (make-valid-ord-info-objfun :type type :linkage linkage :defstatus defstatus :uid uid)) (table (valid-add-ord ident new-info table) ) (anno-info (make-init-declor-info :type type :typedefp nil :uid? uid)) ((erp new-initer? more-types table) (valid-initer-option initdeclor.initer? type lifetime? table ienv)) ((when (and (linkage-case linkage :external) (let ((ext-info? (valid-lookup-ext ident table))) (and ext-info? (not (type-compatiblep (valid-ext-info->type ext-info?) type ienv)))))) (retmsg$ "The identifier ~x0 with external linkage and type ~x1 ~ was previously declared with incompatible type ~x2." ident type (valid-ext-info->type (valid-lookup-ext ident table)))) ((when (and (linkage-case linkage :external) (valid-has-internalp ident table))) (retmsg$ "The identifier ~x0 with external linkage ~ was previously declared with internal linkage ~ in the same translation unit." ident)) ((when (and (linkage-case linkage :internal) (let ((ext-info? (valid-lookup-ext ident table))) (and ext-info? (in table.filepath (valid-ext-info->declared-in ext-info?)))))) (retmsg$ "The identifier ~x0 with internal linkage ~ was previously declared with external linkage ~ in the same translation unit." ident)) ((when (not info?)) (retok (make-init-declor :declor new-declor :asm? initdeclor.asm? :attribs initdeclor.attribs :initer? new-initer? :info anno-info) (union types more-types) table)) ((when (or (valid-ord-info-case info? :typedef) (valid-ord-info-case info? :enumconst))) (if currentp (retmsg$ "The identifier ~x0 ~ is already declared in the current scope ~ with associated information ~x1." ident info?) (retok (make-init-declor :declor new-declor :asm? initdeclor.asm? :attribs initdeclor.attribs :initer? new-initer? :info anno-info) (union types more-types) table))) ((valid-ord-info-objfun info) info?) ((when (or (linkage-case linkage :none) (linkage-case info.linkage :none))) (if currentp (retmsg$ "The identifier ~x0 ~ is already declared in the current scope ~ with associated information ~x1." ident info?) (retok (make-init-declor :declor new-declor :asm? initdeclor.asm? :attribs initdeclor.attribs :initer? new-initer? :info anno-info) (union types more-types) table))) ((unless (or (equal type info.type) (equal type (type-unknown)) (equal info.type (type-unknown)))) (retmsg$ "The identifier ~x0 ~ is declared with type ~x1 ~ after being declared with type ~x2." ident type info.type)) ((when (and (linkage-case linkage :internal) (linkage-case info.linkage :external))) (retmsg$ "The identifier ~x0 ~ is declared with internal linkage ~ after being declared with external linkage." ident)) ((when (and (linkage-case linkage :external) (linkage-case info.linkage :internal))) (raise "Internal error: ~ the identifier ~x0 ~ is declared with external linkage ~ after being declared with internal linkage." ident) (retmsg$ ""))) (retok (make-init-declor :declor new-declor :asm? initdeclor.asm? :attribs initdeclor.attribs :initer? new-initer? :info anno-info) (union types more-types) table))))
Function:
(defun valid-init-declor-list (initdeclors type storspecs table ienv) (declare (xargs :guard (and (init-declor-listp initdeclors) (typep type) (stor-spec-listp storspecs) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (init-declor-list-unambp initdeclors))) (b* (((reterr) nil nil (irr-valid-table)) ((when (endp initdeclors)) (retok nil nil (valid-table-fix table))) ((erp new-initdeclor types table) (valid-init-declor (car initdeclors) type storspecs table ienv)) ((erp new-initdeclors more-types table) (valid-init-declor-list (cdr initdeclors) type storspecs table ienv))) (retok (cons new-initdeclor new-initdeclors) (union types more-types) table)))
Function:
(defun valid-declon (declon table ienv) (declare (xargs :guard (and (declonp declon) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (declon-unambp declon))) (b* (((reterr) (irr-declon) nil (irr-valid-table))) (declon-case declon :declon (b* (((erp new-specs type storspecs types table) (valid-decl-spec-list declon.specs nil nil nil table ienv)) ((when (and (endp declon.declors) (not (type-case type :struct)) (not (type-case type :union)) (not (type-case type :enum)))) (retmsg$ "The declaration ~x0 declares ~ neither a declarator nor a tag." (declon-fix declon))) ((erp new-declors more-types table) (valid-init-declor-list declon.declors type storspecs table ienv))) (retok (make-declon-declon :extension declon.extension :specs new-specs :declors new-declors) (union types more-types) table)) :statassert (b* (((erp new-statassert types table) (valid-statassert declon.statassert table ienv))) (retok (declon-statassert new-statassert) types table)))))
Function:
(defun valid-declon-list (declons table ienv) (declare (xargs :guard (and (declon-listp declons) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (declon-list-unambp declons))) (b* (((reterr) nil nil (irr-valid-table)) ((when (endp declons)) (retok nil nil (valid-table-fix table))) ((erp new-declon types table) (valid-declon (car declons) table ienv)) ((erp new-declons more-types table) (valid-declon-list (cdr declons) table ienv))) (retok (cons new-declon new-declons) (union types more-types) table)))
Function:
(defun valid-label (label table ienv) (declare (xargs :guard (and (labelp label) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (label-unambp label))) (b* (((reterr) (irr-label) nil (irr-valid-table))) (label-case label :name (retok (label-fix label) nil (valid-table-fix table)) :casexpr (b* (((erp new-expr type types table) (valid-const-expr label.expr table ienv)) ((unless (or (type-integerp type) (type-case type :unknown))) (retmsg$ "The first or only 'case' expression ~ in the label ~x0 has type ~x1." (label-fix label) type)) ((erp new-range? type? more-types table) (valid-const-expr-option label.range? table ienv)) ((when (and type? (not (type-integerp type?)) (not (type-case type? :unknown)))) (retmsg$ "The second 'case' expression~ in the label ~x0 has type ~x1." (label-fix label) type?))) (retok (make-label-casexpr :expr new-expr :range? new-range?) (union types more-types) table)) :default (retok (label-default) nil (valid-table-fix table)))))
Function:
(defun valid-stmt (stmt table ienv) (declare (xargs :guard (and (stmtp stmt) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (stmt-unambp stmt))) (b* (((reterr) (irr-stmt) nil nil (irr-valid-table))) (stmt-case stmt :labeled (b* (((erp new-label types table) (valid-label stmt.label table ienv)) ((erp new-stmt more-types type? table) (valid-stmt stmt.stmt table ienv))) (retok (make-stmt-labeled :label new-label :stmt new-stmt) (union types more-types) type? table)) :compound (b* (((erp new-cstmt types type? table) (valid-comp-stmt stmt.stmt nil table ienv))) (retok (stmt-compound new-cstmt) types type? table)) :expr (b* (((erp new-expr? type? types table) (valid-expr-option stmt.expr? table ienv))) (retok (make-stmt-expr :expr? new-expr? :info nil) types type? table)) :if (b* ((table (valid-push-scope table)) ((erp new-test test-type test-types table) (valid-expr stmt.test table ienv)) ((unless (or (type-scalarp test-type) (type-case test-type :unknown))) (retmsg$ "The test of the statement ~x0 has type ~x1." (stmt-fix stmt) test-type)) (table (valid-push-scope table)) ((erp new-then then-types & table) (valid-stmt stmt.then table ienv)) (table (valid-pop-scope table)) (table (valid-pop-scope table))) (retok (make-stmt-if :test new-test :then new-then) (union test-types then-types) nil table)) :ifelse (b* ((table (valid-push-scope table)) ((erp new-test test-type test-types table) (valid-expr stmt.test table ienv)) ((unless (or (type-scalarp test-type) (type-case test-type :unknown))) (retmsg$ "The test of the statement ~x0 has type ~x1." (stmt-fix stmt) test-type)) (table (valid-push-scope table)) ((erp new-then then-types & table) (valid-stmt stmt.then table ienv)) (table (valid-pop-scope table)) (table (valid-push-scope table)) ((erp new-else else-types & table) (valid-stmt stmt.else table ienv)) (table (valid-pop-scope table)) (table (valid-pop-scope table))) (retok (make-stmt-ifelse :test new-test :then new-then :else new-else) (union test-types (union then-types else-types)) nil table)) :switch (b* ((table (valid-push-scope table)) ((erp new-target target-type target-types table) (valid-expr stmt.target table ienv)) ((unless (or (type-integerp target-type) (type-case target-type :unknown))) (retmsg$ "The target of the statement ~x0 has type ~x1." (stmt-fix stmt) target-type)) (table (valid-push-scope table)) ((erp new-body body-types & table) (valid-stmt stmt.body table ienv)) (table (valid-pop-scope table)) (table (valid-pop-scope table))) (retok (make-stmt-switch :target new-target :body new-body) (union target-types body-types) nil table)) :while (b* ((table (valid-push-scope table)) ((erp new-test test-type test-types table) (valid-expr stmt.test table ienv)) ((unless (or (type-scalarp test-type) (type-case test-type :unknown))) (retmsg$ "The test of the statement ~x0 has type ~x1." (stmt-fix stmt) test-type)) (table (valid-push-scope table)) ((erp new-body body-types & table) (valid-stmt stmt.body table ienv)) (table (valid-pop-scope table)) (table (valid-pop-scope table)) (types (union test-types body-types))) (retok (make-stmt-while :test new-test :body new-body) types nil table)) :dowhile (b* ((table (valid-push-scope table)) (table (valid-push-scope table)) ((erp new-body body-types & table) (valid-stmt stmt.body table ienv)) (table (valid-pop-scope table)) ((erp new-test test-type test-types table) (valid-expr stmt.test table ienv)) ((unless (or (type-scalarp test-type) (type-case test-type :unknown))) (retmsg$ "The test of the statement ~x0 has type ~x1." (stmt-fix stmt) test-type)) (table (valid-pop-scope table))) (retok (make-stmt-dowhile :body new-body :test new-test) (union test-types body-types) nil table)) :for-expr (b* ((table (valid-push-scope table)) ((erp new-init & init-types table) (valid-expr-option stmt.init table ienv)) ((erp new-test test-type? test-types table) (valid-expr-option stmt.test table ienv)) ((when (and test-type? (not (type-scalarp test-type?)) (not (type-case test-type? :unknown)))) (retmsg$ "The test of the statement ~x0 has type ~x1." (stmt-fix stmt) test-type?)) ((erp new-next & next-types table) (valid-expr-option stmt.next table ienv)) (table (valid-push-scope table)) ((erp new-body body-types & table) (valid-stmt stmt.body table ienv)) (table (valid-pop-scope table)) (table (valid-pop-scope table))) (retok (make-stmt-for-expr :init new-init :test new-test :next new-next :body new-body) (union init-types (union test-types (union next-types body-types))) nil table)) :for-declon (b* ((table (valid-push-scope table)) ((erp new-init init-types table) (valid-declon stmt.init table ienv)) ((erp new-test test-type? test-types table) (valid-expr-option stmt.test table ienv)) ((when (and test-type? (not (type-scalarp test-type?)) (not (type-case test-type? :unknown)))) (retmsg$ "The test of the statement ~x0 has type ~x1." (stmt-fix stmt) test-type?)) ((erp new-next & next-types table) (valid-expr-option stmt.next table ienv)) (table (valid-push-scope table)) ((erp new-body body-types & table) (valid-stmt stmt.body table ienv)) (table (valid-pop-scope table)) (table (valid-pop-scope table))) (retok (make-stmt-for-declon :init new-init :test new-test :next new-next :body new-body) (union init-types (union test-types (union next-types body-types))) nil table)) :for-ambig (prog2$ (impossible) (retmsg$ "")) :goto (retok (stmt-goto stmt.label) nil nil (valid-table-fix table)) :gotoe (retok (stmt-gotoe stmt.label) nil nil (valid-table-fix table)) :continue (retok (stmt-continue) nil nil (valid-table-fix table)) :break (retok (stmt-break) nil nil (valid-table-fix table)) :return (b* (((erp new-expr? type? types table) (valid-expr-option stmt.expr? table ienv)) (return-type (or type? (type-void)))) (retok (make-stmt-return :expr? new-expr? :info nil) (insert return-type types) nil table)) :asm (retok (stmt-asm stmt.stmt) nil nil (valid-table-fix table)))))
Function:
(defun valid-comp-stmt (cstmt fundefp table ienv) (declare (xargs :guard (and (comp-stmtp cstmt) (booleanp fundefp) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (comp-stmt-unambp cstmt))) (b* (((reterr) (irr-comp-stmt) nil nil (irr-valid-table)) ((comp-stmt cstmt) cstmt) (table (if fundefp table (valid-push-scope table)) ) ((erp new-items types last-expr-type? table) (valid-block-item-list cstmt.items table ienv)) (table (if fundefp table (valid-pop-scope table)) )) (retok (make-comp-stmt :labels cstmt.labels :items new-items) types last-expr-type? table)))
Function:
(defun valid-block-item (item table ienv) (declare (xargs :guard (and (block-itemp item) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (block-item-unambp item))) (b* (((reterr) (irr-block-item) nil nil (irr-valid-table))) (block-item-case item :declon (b* (((erp new-declon types table) (valid-declon item.declon table ienv))) (retok (make-block-item-declon :declon new-declon :info nil) types nil table)) :stmt (b* (((erp new-stmt types last-expr-type? table) (valid-stmt item.stmt table ienv))) (retok (make-block-item-stmt :stmt new-stmt :info nil) types last-expr-type? table)) :ambig (prog2$ (impossible) (retmsg$ "")))))
Function:
(defun valid-block-item-list (items table ienv) (declare (xargs :guard (and (block-item-listp items) (valid-tablep table) (ienvp ienv)))) (declare (xargs :guard (block-item-list-unambp items))) (b* (((reterr) nil nil nil (irr-valid-table)) ((when (endp items)) (retok nil nil nil (valid-table-fix table))) ((erp new-item types last-expr-type? table) (valid-block-item (car items) table ienv)) ((when (endp (cdr items))) (retok (list new-item) types last-expr-type? table)) ((erp new-items more-types last-expr-type? table) (valid-block-item-list (cdr items) table ienv))) (retok (cons new-item new-items) (union types more-types) last-expr-type? table)))
Theorem:
(defthm return-type-of-valid-expr.erp (b* (((mv acl2::?erp ?new-expr ?type ?return-types ?new-table) (valid-expr expr table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr.new-expr (b* (((mv acl2::?erp ?new-expr ?type ?return-types ?new-table) (valid-expr expr table ienv))) (exprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr.type (b* (((mv acl2::?erp ?new-expr ?type ?return-types ?new-table) (valid-expr expr table ienv))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr.return-types (b* (((mv acl2::?erp ?new-expr ?type ?return-types ?new-table) (valid-expr expr table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr.new-table (b* (((mv acl2::?erp ?new-expr ?type ?return-types ?new-table) (valid-expr expr table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-list.erp (b* (((mv acl2::?erp ?new-exprs ?types ?return-types ?new-table) (valid-expr-list exprs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-list.new-exprs (b* (((mv acl2::?erp ?new-exprs ?types ?return-types ?new-table) (valid-expr-list exprs table ienv))) (expr-listp new-exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-list.types (b* (((mv acl2::?erp ?new-exprs ?types ?return-types ?new-table) (valid-expr-list exprs table ienv))) (type-listp types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-list.return-types (b* (((mv acl2::?erp ?new-exprs ?types ?return-types ?new-table) (valid-expr-list exprs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-list.new-table (b* (((mv acl2::?erp ?new-exprs ?types ?return-types ?new-table) (valid-expr-list exprs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-option.erp (b* (((mv acl2::?erp ?new-expr? ?type? ?return-types ?new-table) (valid-expr-option expr? table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-option.new-expr? (b* (((mv acl2::?erp ?new-expr? ?type? ?return-types ?new-table) (valid-expr-option expr? table ienv))) (expr-optionp new-expr?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-option.type? (b* (((mv acl2::?erp ?new-expr? ?type? ?return-types ?new-table) (valid-expr-option expr? table ienv))) (type-optionp type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-option.return-types (b* (((mv acl2::?erp ?new-expr? ?type? ?return-types ?new-table) (valid-expr-option expr? table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-expr-option.new-table (b* (((mv acl2::?erp ?new-expr? ?type? ?return-types ?new-table) (valid-expr-option expr? table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr.erp (b* (((mv acl2::?erp ?new-cexpr ?type ?return-types ?new-table) (valid-const-expr cexpr table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr.new-cexpr (b* (((mv acl2::?erp ?new-cexpr ?type ?return-types ?new-table) (valid-const-expr cexpr table ienv))) (const-exprp new-cexpr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr.type (b* (((mv acl2::?erp ?new-cexpr ?type ?return-types ?new-table) (valid-const-expr cexpr table ienv))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr.return-types (b* (((mv acl2::?erp ?new-cexpr ?type ?return-types ?new-table) (valid-const-expr cexpr table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr.new-table (b* (((mv acl2::?erp ?new-cexpr ?type ?return-types ?new-table) (valid-const-expr cexpr table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr-option.erp (b* (((mv acl2::?erp ?new-cexpr? ?type? ?return-types ?new-table) (valid-const-expr-option cexpr? table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr-option.new-cexpr? (b* (((mv acl2::?erp ?new-cexpr? ?type? ?return-types ?new-table) (valid-const-expr-option cexpr? table ienv))) (const-expr-optionp new-cexpr?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr-option.type? (b* (((mv acl2::?erp ?new-cexpr? ?type? ?return-types ?new-table) (valid-const-expr-option cexpr? table ienv))) (type-optionp type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr-option.return-types (b* (((mv acl2::?erp ?new-cexpr? ?type? ?return-types ?new-table) (valid-const-expr-option cexpr? table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-const-expr-option.new-table (b* (((mv acl2::?erp ?new-cexpr? ?type? ?return-types ?new-table) (valid-const-expr-option cexpr? table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc.erp (b* (((mv acl2::?erp ?new-genassoc ?tyname-type ?expr-type ?return-types ?new-table) (valid-genassoc genassoc table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc.new-genassoc (b* (((mv acl2::?erp ?new-genassoc ?tyname-type ?expr-type ?return-types ?new-table) (valid-genassoc genassoc table ienv))) (genassocp new-genassoc)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc.tyname-type (b* (((mv acl2::?erp ?new-genassoc ?tyname-type ?expr-type ?return-types ?new-table) (valid-genassoc genassoc table ienv))) (type-optionp tyname-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc.expr-type (b* (((mv acl2::?erp ?new-genassoc ?tyname-type ?expr-type ?return-types ?new-table) (valid-genassoc genassoc table ienv))) (typep expr-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc.return-types (b* (((mv acl2::?erp ?new-genassoc ?tyname-type ?expr-type ?return-types ?new-table) (valid-genassoc genassoc table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc.new-table (b* (((mv acl2::?erp ?new-genassoc ?tyname-type ?expr-type ?return-types ?new-table) (valid-genassoc genassoc table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc-list.erp (b* (((mv acl2::?erp ?new-genassocs ?type-alist ?return-types ?new-table) (valid-genassoc-list genassocs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc-list.new-genassocs (b* (((mv acl2::?erp ?new-genassocs ?type-alist ?return-types ?new-table) (valid-genassoc-list genassocs table ienv))) (genassoc-listp new-genassocs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc-list.type-alist (b* (((mv acl2::?erp ?new-genassocs ?type-alist ?return-types ?new-table) (valid-genassoc-list genassocs table ienv))) (type-option-type-alistp type-alist)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc-list.return-types (b* (((mv acl2::?erp ?new-genassocs ?type-alist ?return-types ?new-table) (valid-genassoc-list genassocs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-genassoc-list.new-table (b* (((mv acl2::?erp ?new-genassocs ?type-alist ?return-types ?new-table) (valid-genassoc-list genassocs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-member-designor.erp (b* (((mv acl2::?erp ?new-memdesign ?return-types ?new-table) (valid-member-designor memdesign table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-member-designor.new-memdesign (b* (((mv acl2::?erp ?new-memdesign ?return-types ?new-table) (valid-member-designor memdesign table ienv))) (member-designorp new-memdesign)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-member-designor.return-types (b* (((mv acl2::?erp ?new-memdesign ?return-types ?new-table) (valid-member-designor memdesign table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-member-designor.new-table (b* (((mv acl2::?erp ?new-memdesign ?return-types ?new-table) (valid-member-designor memdesign table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-type-spec.erp (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-type-spec.new-tyspec (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (type-specp new-tyspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-type-spec.new-type? (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (type-optionp new-type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-type-spec.new-tyspecs (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (type-spec-listp new-tyspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-type-spec.return-types (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-type-spec.new-table (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual.erp (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual.new-specqual (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (spec/qual-p new-specqual)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual.new-type? (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (type-optionp new-type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual.new-tyspecs (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (type-spec-listp new-tyspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual.return-types (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual.new-table (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual-list.erp (b* (((mv acl2::?erp ?new-specquals ?type ?return-types ?new-table) (valid-spec/qual-list specquals type? tyspecs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual-list.new-specquals (b* (((mv acl2::?erp ?new-specquals ?type ?return-types ?new-table) (valid-spec/qual-list specquals type? tyspecs table ienv))) (spec/qual-listp new-specquals)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual-list.type (b* (((mv acl2::?erp ?new-specquals ?type ?return-types ?new-table) (valid-spec/qual-list specquals type? tyspecs table ienv))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual-list.return-types (b* (((mv acl2::?erp ?new-specquals ?type ?return-types ?new-table) (valid-spec/qual-list specquals type? tyspecs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-spec/qual-list.new-table (b* (((mv acl2::?erp ?new-specquals ?type ?return-types ?new-table) (valid-spec/qual-list specquals type? tyspecs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-align-spec.erp (b* (((mv acl2::?erp ?new-align ?return-types ?new-table) (valid-align-spec align table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-align-spec.new-align (b* (((mv acl2::?erp ?new-align ?return-types ?new-table) (valid-align-spec align table ienv))) (align-specp new-align)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-align-spec.return-types (b* (((mv acl2::?erp ?new-align ?return-types ?new-table) (valid-align-spec align table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-align-spec.new-table (b* (((mv acl2::?erp ?new-align ?return-types ?new-table) (valid-align-spec align table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec.erp (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec.new-declspec (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (decl-specp new-declspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec.new-type? (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (type-optionp new-type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec.new-tyspecs (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (type-spec-listp new-tyspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec.new-storspecs (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (stor-spec-listp new-storspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec.return-types (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec.new-table (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec-list.erp (b* (((mv acl2::?erp ?new-declspecs ?type ?all-storspecs ?return-types ?new-table) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec-list.new-declspecs (b* (((mv acl2::?erp ?new-declspecs ?type ?all-storspecs ?return-types ?new-table) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv))) (decl-spec-listp new-declspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec-list.type (b* (((mv acl2::?erp ?new-declspecs ?type ?all-storspecs ?return-types ?new-table) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec-list.all-storspecs (b* (((mv acl2::?erp ?new-declspecs ?type ?all-storspecs ?return-types ?new-table) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv))) (stor-spec-listp all-storspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec-list.return-types (b* (((mv acl2::?erp ?new-declspecs ?type ?all-storspecs ?return-types ?new-table) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-decl-spec-list.new-table (b* (((mv acl2::?erp ?new-declspecs ?type ?all-storspecs ?return-types ?new-table) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-initer.erp (b* (((mv acl2::?erp ?new-initer ?return-types ?new-table) (valid-initer initer target-type lifetime table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-initer.new-initer (b* (((mv acl2::?erp ?new-initer ?return-types ?new-table) (valid-initer initer target-type lifetime table ienv))) (initerp new-initer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-initer.return-types (b* (((mv acl2::?erp ?new-initer ?return-types ?new-table) (valid-initer initer target-type lifetime table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-initer.new-table (b* (((mv acl2::?erp ?new-initer ?return-types ?new-table) (valid-initer initer target-type lifetime table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-initer-option.erp (b* (((mv acl2::?erp ?new-initer? ?return-types ?new-table) (valid-initer-option initer? target-type lifetime? table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-initer-option.new-initer? (b* (((mv acl2::?erp ?new-initer? ?return-types ?new-table) (valid-initer-option initer? target-type lifetime? table ienv))) (initer-optionp new-initer?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-initer-option.return-types (b* (((mv acl2::?erp ?new-initer? ?return-types ?new-table) (valid-initer-option initer? target-type lifetime? table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-initer-option.new-table (b* (((mv acl2::?erp ?new-initer? ?return-types ?new-table) (valid-initer-option initer? target-type lifetime? table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-desiniter.erp (b* (((mv acl2::?erp ?new-desiniter ?return-types ?new-table) (valid-desiniter desiniter target-type lifetime table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-desiniter.new-desiniter (b* (((mv acl2::?erp ?new-desiniter ?return-types ?new-table) (valid-desiniter desiniter target-type lifetime table ienv))) (desiniterp new-desiniter)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-desiniter.return-types (b* (((mv acl2::?erp ?new-desiniter ?return-types ?new-table) (valid-desiniter desiniter target-type lifetime table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-desiniter.new-table (b* (((mv acl2::?erp ?new-desiniter ?return-types ?new-table) (valid-desiniter desiniter target-type lifetime table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-desiniter-list.erp (b* (((mv acl2::?erp ?new-desiniters ?return-types ?new-table) (valid-desiniter-list desiniters target-type lifetime table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-desiniter-list.new-desiniters (b* (((mv acl2::?erp ?new-desiniters ?return-types ?new-table) (valid-desiniter-list desiniters target-type lifetime table ienv))) (desiniter-listp new-desiniters)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-desiniter-list.return-types (b* (((mv acl2::?erp ?new-desiniters ?return-types ?new-table) (valid-desiniter-list desiniters target-type lifetime table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-desiniter-list.new-table (b* (((mv acl2::?erp ?new-desiniters ?return-types ?new-table) (valid-desiniter-list desiniters target-type lifetime table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor.erp (b* (((mv acl2::?erp ?new-designor ?new-target-type ?return-types ?new-table) (valid-designor designor target-type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor.new-designor (b* (((mv acl2::?erp ?new-designor ?new-target-type ?return-types ?new-table) (valid-designor designor target-type table ienv))) (designorp new-designor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor.new-target-type (b* (((mv acl2::?erp ?new-designor ?new-target-type ?return-types ?new-table) (valid-designor designor target-type table ienv))) (typep new-target-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor.return-types (b* (((mv acl2::?erp ?new-designor ?new-target-type ?return-types ?new-table) (valid-designor designor target-type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor.new-table (b* (((mv acl2::?erp ?new-designor ?new-target-type ?return-types ?new-table) (valid-designor designor target-type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor-list.erp (b* (((mv acl2::?erp ?new-designors ?new-target-type ?return-types ?new-table) (valid-designor-list designors target-type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor-list.new-designors (b* (((mv acl2::?erp ?new-designors ?new-target-type ?return-types ?new-table) (valid-designor-list designors target-type table ienv))) (designor-listp new-designors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor-list.new-target-type (b* (((mv acl2::?erp ?new-designors ?new-target-type ?return-types ?new-table) (valid-designor-list designors target-type table ienv))) (typep new-target-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor-list.return-types (b* (((mv acl2::?erp ?new-designors ?new-target-type ?return-types ?new-table) (valid-designor-list designors target-type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-designor-list.new-table (b* (((mv acl2::?erp ?new-designors ?new-target-type ?return-types ?new-table) (valid-designor-list designors target-type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor.erp (b* (((mv acl2::?erp ?new-declor ?new-type ?ident ?return-types ?new-table) (valid-declor declor fundef-params-p type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor.new-declor (b* (((mv acl2::?erp ?new-declor ?new-type ?ident ?return-types ?new-table) (valid-declor declor fundef-params-p type table ienv))) (declorp new-declor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor.new-type (b* (((mv acl2::?erp ?new-declor ?new-type ?ident ?return-types ?new-table) (valid-declor declor fundef-params-p type table ienv))) (typep new-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor.ident (b* (((mv acl2::?erp ?new-declor ?new-type ?ident ?return-types ?new-table) (valid-declor declor fundef-params-p type table ienv))) (identp ident)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor.return-types (b* (((mv acl2::?erp ?new-declor ?new-type ?ident ?return-types ?new-table) (valid-declor declor fundef-params-p type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor.new-table (b* (((mv acl2::?erp ?new-declor ?new-type ?ident ?return-types ?new-table) (valid-declor declor fundef-params-p type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor-option.erp (b* (((mv acl2::?erp ?new-declor? ?new-type ?ident? ?return-types ?new-table) (valid-declor-option declor? type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor-option.new-declor? (b* (((mv acl2::?erp ?new-declor? ?new-type ?ident? ?return-types ?new-table) (valid-declor-option declor? type table ienv))) (declor-optionp new-declor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor-option.new-type (b* (((mv acl2::?erp ?new-declor? ?new-type ?ident? ?return-types ?new-table) (valid-declor-option declor? type table ienv))) (typep new-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor-option.ident? (b* (((mv acl2::?erp ?new-declor? ?new-type ?ident? ?return-types ?new-table) (valid-declor-option declor? type table ienv))) (ident-optionp ident?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor-option.return-types (b* (((mv acl2::?erp ?new-declor? ?new-type ?ident? ?return-types ?new-table) (valid-declor-option declor? type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declor-option.new-table (b* (((mv acl2::?erp ?new-declor? ?new-type ?ident? ?return-types ?new-table) (valid-declor-option declor? type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirdeclor.erp (b* (((mv acl2::?erp ?new-dirdeclor ?new-type ?ident ?return-types ?new-table) (valid-dirdeclor dirdeclor fundef-params-p type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirdeclor.new-dirdeclor (b* (((mv acl2::?erp ?new-dirdeclor ?new-type ?ident ?return-types ?new-table) (valid-dirdeclor dirdeclor fundef-params-p type table ienv))) (dirdeclorp new-dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirdeclor.new-type (b* (((mv acl2::?erp ?new-dirdeclor ?new-type ?ident ?return-types ?new-table) (valid-dirdeclor dirdeclor fundef-params-p type table ienv))) (typep new-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirdeclor.ident (b* (((mv acl2::?erp ?new-dirdeclor ?new-type ?ident ?return-types ?new-table) (valid-dirdeclor dirdeclor fundef-params-p type table ienv))) (identp ident)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirdeclor.return-types (b* (((mv acl2::?erp ?new-dirdeclor ?new-type ?ident ?return-types ?new-table) (valid-dirdeclor dirdeclor fundef-params-p type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirdeclor.new-table (b* (((mv acl2::?erp ?new-dirdeclor ?new-type ?ident ?return-types ?new-table) (valid-dirdeclor dirdeclor fundef-params-p type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor.erp (b* (((mv acl2::?erp ?new-absdeclor ?new-type ?return-types ?new-table) (valid-absdeclor absdeclor type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor.new-absdeclor (b* (((mv acl2::?erp ?new-absdeclor ?new-type ?return-types ?new-table) (valid-absdeclor absdeclor type table ienv))) (absdeclorp new-absdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor.new-type (b* (((mv acl2::?erp ?new-absdeclor ?new-type ?return-types ?new-table) (valid-absdeclor absdeclor type table ienv))) (typep new-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor.return-types (b* (((mv acl2::?erp ?new-absdeclor ?new-type ?return-types ?new-table) (valid-absdeclor absdeclor type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor.new-table (b* (((mv acl2::?erp ?new-absdeclor ?new-type ?return-types ?new-table) (valid-absdeclor absdeclor type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor-option.erp (b* (((mv acl2::?erp ?new-absdeclor? ?new-type ?return-types ?new-table) (valid-absdeclor-option absdeclor? type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor-option.new-absdeclor? (b* (((mv acl2::?erp ?new-absdeclor? ?new-type ?return-types ?new-table) (valid-absdeclor-option absdeclor? type table ienv))) (absdeclor-optionp new-absdeclor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor-option.new-type (b* (((mv acl2::?erp ?new-absdeclor? ?new-type ?return-types ?new-table) (valid-absdeclor-option absdeclor? type table ienv))) (typep new-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor-option.return-types (b* (((mv acl2::?erp ?new-absdeclor? ?new-type ?return-types ?new-table) (valid-absdeclor-option absdeclor? type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-absdeclor-option.new-table (b* (((mv acl2::?erp ?new-absdeclor? ?new-type ?return-types ?new-table) (valid-absdeclor-option absdeclor? type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor.erp (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-type ?return-types ?new-table) (valid-dirabsdeclor dirabsdeclor type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor.new-dirabsdeclor (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-type ?return-types ?new-table) (valid-dirabsdeclor dirabsdeclor type table ienv))) (dirabsdeclorp new-dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor.new-type (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-type ?return-types ?new-table) (valid-dirabsdeclor dirabsdeclor type table ienv))) (typep new-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor.return-types (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-type ?return-types ?new-table) (valid-dirabsdeclor dirabsdeclor type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor.new-table (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-type ?return-types ?new-table) (valid-dirabsdeclor dirabsdeclor type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor-option.erp (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-type ?return-types ?new-table) (valid-dirabsdeclor-option dirabsdeclor? type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor-option.new-dirabsdeclor? (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-type ?return-types ?new-table) (valid-dirabsdeclor-option dirabsdeclor? type table ienv))) (dirabsdeclor-optionp new-dirabsdeclor?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor-option.new-type (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-type ?return-types ?new-table) (valid-dirabsdeclor-option dirabsdeclor? type table ienv))) (typep new-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor-option.return-types (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-type ?return-types ?new-table) (valid-dirabsdeclor-option dirabsdeclor? type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-dirabsdeclor-option.new-table (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-type ?return-types ?new-table) (valid-dirabsdeclor-option dirabsdeclor? type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon.erp (b* (((mv acl2::?erp ?new-paramdecl ?type ?return-types ?new-table) (valid-param-declon paramdecl fundef-params-p table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon.new-paramdecl (b* (((mv acl2::?erp ?new-paramdecl ?type ?return-types ?new-table) (valid-param-declon paramdecl fundef-params-p table ienv))) (param-declonp new-paramdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon.type (b* (((mv acl2::?erp ?new-paramdecl ?type ?return-types ?new-table) (valid-param-declon paramdecl fundef-params-p table ienv))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon.return-types (b* (((mv acl2::?erp ?new-paramdecl ?type ?return-types ?new-table) (valid-param-declon paramdecl fundef-params-p table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon.new-table (b* (((mv acl2::?erp ?new-paramdecl ?type ?return-types ?new-table) (valid-param-declon paramdecl fundef-params-p table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon-list.erp (b* (((mv acl2::?erp ?new-paramdecls ?types ?return-types ?new-table) (valid-param-declon-list paramdecls fundef-params-p table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon-list.new-paramdecls (b* (((mv acl2::?erp ?new-paramdecls ?types ?return-types ?new-table) (valid-param-declon-list paramdecls fundef-params-p table ienv))) (param-declon-listp new-paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon-list.types (b* (((mv acl2::?erp ?new-paramdecls ?types ?return-types ?new-table) (valid-param-declon-list paramdecls fundef-params-p table ienv))) (type-listp types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon-list.return-types (b* (((mv acl2::?erp ?new-paramdecls ?types ?return-types ?new-table) (valid-param-declon-list paramdecls fundef-params-p table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declon-list.new-table (b* (((mv acl2::?erp ?new-paramdecls ?types ?return-types ?new-table) (valid-param-declon-list paramdecls fundef-params-p table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declor.erp (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declor.new-paramdeclor (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (param-declorp new-paramdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declor.new-type (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (typep new-type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declor.ident? (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (ident-optionp ident?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declor.return-types (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declor.uid? (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (uid-optionp uid?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-param-declor.new-table (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-tyname.erp (b* (((mv acl2::?erp ?new-tyname ?type ?return-types ?new-table) (valid-tyname tyname table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-tyname.new-tyname (b* (((mv acl2::?erp ?new-tyname ?type ?return-types ?new-table) (valid-tyname tyname table ienv))) (tynamep new-tyname)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-tyname.type (b* (((mv acl2::?erp ?new-tyname ?type ?return-types ?new-table) (valid-tyname tyname table ienv))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-tyname.return-types (b* (((mv acl2::?erp ?new-tyname ?type ?return-types ?new-table) (valid-tyname tyname table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-tyname.new-table (b* (((mv acl2::?erp ?new-tyname ?type ?return-types ?new-table) (valid-tyname tyname table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struni-spec.erp (b* (((mv acl2::?erp ?new-struni-spec ?return-types ?new-table) (valid-struni-spec struni-spec table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struni-spec.new-struni-spec (b* (((mv acl2::?erp ?new-struni-spec ?return-types ?new-table) (valid-struni-spec struni-spec table ienv))) (struni-specp new-struni-spec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struni-spec.return-types (b* (((mv acl2::?erp ?new-struni-spec ?return-types ?new-table) (valid-struni-spec struni-spec table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struni-spec.new-table (b* (((mv acl2::?erp ?new-struni-spec ?return-types ?new-table) (valid-struni-spec struni-spec table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon.erp (b* (((mv acl2::?erp ?new-structdeclon ?new-previous ?return-types ?new-table) (valid-struct-declon structdeclon previous table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon.new-structdeclon (b* (((mv acl2::?erp ?new-structdeclon ?new-previous ?return-types ?new-table) (valid-struct-declon structdeclon previous table ienv))) (struct-declonp new-structdeclon)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon.new-previous (b* (((mv acl2::?erp ?new-structdeclon ?new-previous ?return-types ?new-table) (valid-struct-declon structdeclon previous table ienv))) (ident-listp new-previous)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon.return-types (b* (((mv acl2::?erp ?new-structdeclon ?new-previous ?return-types ?new-table) (valid-struct-declon structdeclon previous table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon.new-table (b* (((mv acl2::?erp ?new-structdeclon ?new-previous ?return-types ?new-table) (valid-struct-declon structdeclon previous table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon-list.erp (b* (((mv acl2::?erp ?new-structdeclons ?return-types ?new-table) (valid-struct-declon-list structdeclons previous table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon-list.new-structdeclons (b* (((mv acl2::?erp ?new-structdeclons ?return-types ?new-table) (valid-struct-declon-list structdeclons previous table ienv))) (struct-declon-listp new-structdeclons)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon-list.return-types (b* (((mv acl2::?erp ?new-structdeclons ?return-types ?new-table) (valid-struct-declon-list structdeclons previous table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declon-list.new-table (b* (((mv acl2::?erp ?new-structdeclons ?return-types ?new-table) (valid-struct-declon-list structdeclons previous table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor.erp (b* (((mv acl2::?erp ?new-structdeclor ?new-previous ?return-types ?new-table) (valid-struct-declor structdeclor previous type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor.new-structdeclor (b* (((mv acl2::?erp ?new-structdeclor ?new-previous ?return-types ?new-table) (valid-struct-declor structdeclor previous type table ienv))) (struct-declorp new-structdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor.new-previous (b* (((mv acl2::?erp ?new-structdeclor ?new-previous ?return-types ?new-table) (valid-struct-declor structdeclor previous type table ienv))) (ident-listp new-previous)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor.return-types (b* (((mv acl2::?erp ?new-structdeclor ?new-previous ?return-types ?new-table) (valid-struct-declor structdeclor previous type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor.new-table (b* (((mv acl2::?erp ?new-structdeclor ?new-previous ?return-types ?new-table) (valid-struct-declor structdeclor previous type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor-list.erp (b* (((mv acl2::?erp ?new-structdeclors ?new-previous ?return-types ?new-table) (valid-struct-declor-list structdeclors previous type table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor-list.new-structdeclors (b* (((mv acl2::?erp ?new-structdeclors ?new-previous ?return-types ?new-table) (valid-struct-declor-list structdeclors previous type table ienv))) (struct-declor-listp new-structdeclors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor-list.new-previous (b* (((mv acl2::?erp ?new-structdeclors ?new-previous ?return-types ?new-table) (valid-struct-declor-list structdeclors previous type table ienv))) (ident-listp new-previous)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor-list.return-types (b* (((mv acl2::?erp ?new-structdeclors ?new-previous ?return-types ?new-table) (valid-struct-declor-list structdeclors previous type table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-struct-declor-list.new-table (b* (((mv acl2::?erp ?new-structdeclors ?new-previous ?return-types ?new-table) (valid-struct-declor-list structdeclors previous type table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enum-spec.erp (b* (((mv acl2::?erp ?new-enumspec ?return-types ?new-table) (valid-enum-spec enumspec table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enum-spec.new-enumspec (b* (((mv acl2::?erp ?new-enumspec ?return-types ?new-table) (valid-enum-spec enumspec table ienv))) (enum-specp new-enumspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enum-spec.return-types (b* (((mv acl2::?erp ?new-enumspec ?return-types ?new-table) (valid-enum-spec enumspec table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enum-spec.new-table (b* (((mv acl2::?erp ?new-enumspec ?return-types ?new-table) (valid-enum-spec enumspec table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enumer.erp (b* (((mv acl2::?erp ?new-enumer ?return-types ?new-table) (valid-enumer enumer table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enumer.new-enumer (b* (((mv acl2::?erp ?new-enumer ?return-types ?new-table) (valid-enumer enumer table ienv))) (enumerp new-enumer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enumer.return-types (b* (((mv acl2::?erp ?new-enumer ?return-types ?new-table) (valid-enumer enumer table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enumer.new-table (b* (((mv acl2::?erp ?new-enumer ?return-types ?new-table) (valid-enumer enumer table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enumer-list.erp (b* (((mv acl2::?erp ?new-enumers ?return-types ?new-table) (valid-enumer-list enumers table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enumer-list.new-enumers (b* (((mv acl2::?erp ?new-enumers ?return-types ?new-table) (valid-enumer-list enumers table ienv))) (enumer-listp new-enumers)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enumer-list.return-types (b* (((mv acl2::?erp ?new-enumers ?return-types ?new-table) (valid-enumer-list enumers table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-enumer-list.new-table (b* (((mv acl2::?erp ?new-enumers ?return-types ?new-table) (valid-enumer-list enumers table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-statassert.erp (b* (((mv acl2::?erp ?new-statassert ?return-types ?new-table) (valid-statassert statassert table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-statassert.new-statassert (b* (((mv acl2::?erp ?new-statassert ?return-types ?new-table) (valid-statassert statassert table ienv))) (statassertp new-statassert)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-statassert.return-types (b* (((mv acl2::?erp ?new-statassert ?return-types ?new-table) (valid-statassert statassert table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-statassert.new-table (b* (((mv acl2::?erp ?new-statassert ?return-types ?new-table) (valid-statassert statassert table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-init-declor.erp (b* (((mv acl2::?erp ?new-initdeclor ?return-types ?new-table) (valid-init-declor initdeclor type storspecs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-init-declor.new-initdeclor (b* (((mv acl2::?erp ?new-initdeclor ?return-types ?new-table) (valid-init-declor initdeclor type storspecs table ienv))) (init-declorp new-initdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-init-declor.return-types (b* (((mv acl2::?erp ?new-initdeclor ?return-types ?new-table) (valid-init-declor initdeclor type storspecs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-init-declor.new-table (b* (((mv acl2::?erp ?new-initdeclor ?return-types ?new-table) (valid-init-declor initdeclor type storspecs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-init-declor-list.erp (b* (((mv acl2::?erp ?new-initdeclors ?return-types ?new-table) (valid-init-declor-list initdeclors type storspecs table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-init-declor-list.new-initdeclors (b* (((mv acl2::?erp ?new-initdeclors ?return-types ?new-table) (valid-init-declor-list initdeclors type storspecs table ienv))) (init-declor-listp new-initdeclors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-init-declor-list.return-types (b* (((mv acl2::?erp ?new-initdeclors ?return-types ?new-table) (valid-init-declor-list initdeclors type storspecs table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-init-declor-list.new-table (b* (((mv acl2::?erp ?new-initdeclors ?return-types ?new-table) (valid-init-declor-list initdeclors type storspecs table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declon.erp (b* (((mv acl2::?erp ?new-declon ?return-types ?new-table) (valid-declon declon table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declon.new-declon (b* (((mv acl2::?erp ?new-declon ?return-types ?new-table) (valid-declon declon table ienv))) (declonp new-declon)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declon.return-types (b* (((mv acl2::?erp ?new-declon ?return-types ?new-table) (valid-declon declon table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declon.new-table (b* (((mv acl2::?erp ?new-declon ?return-types ?new-table) (valid-declon declon table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declon-list.erp (b* (((mv acl2::?erp ?new-declons ?return-types ?new-table) (valid-declon-list declons table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declon-list.new-declons (b* (((mv acl2::?erp ?new-declons ?return-types ?new-table) (valid-declon-list declons table ienv))) (declon-listp new-declons)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declon-list.return-types (b* (((mv acl2::?erp ?new-declons ?return-types ?new-table) (valid-declon-list declons table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-declon-list.new-table (b* (((mv acl2::?erp ?new-declons ?return-types ?new-table) (valid-declon-list declons table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-label.erp (b* (((mv acl2::?erp ?new-label ?return-types ?new-table) (valid-label label table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-label.new-label (b* (((mv acl2::?erp ?new-label ?return-types ?new-table) (valid-label label table ienv))) (labelp new-label)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-label.return-types (b* (((mv acl2::?erp ?new-label ?return-types ?new-table) (valid-label label table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-label.new-table (b* (((mv acl2::?erp ?new-label ?return-types ?new-table) (valid-label label table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-stmt.erp (b* (((mv acl2::?erp ?new-stmt ?return-types ?last-expr-type? ?new-table) (valid-stmt stmt table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-stmt.new-stmt (b* (((mv acl2::?erp ?new-stmt ?return-types ?last-expr-type? ?new-table) (valid-stmt stmt table ienv))) (stmtp new-stmt)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-stmt.return-types (b* (((mv acl2::?erp ?new-stmt ?return-types ?last-expr-type? ?new-table) (valid-stmt stmt table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-stmt.last-expr-type? (b* (((mv acl2::?erp ?new-stmt ?return-types ?last-expr-type? ?new-table) (valid-stmt stmt table ienv))) (type-optionp last-expr-type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-stmt.new-table (b* (((mv acl2::?erp ?new-stmt ?return-types ?last-expr-type? ?new-table) (valid-stmt stmt table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-comp-stmt.erp (b* (((mv acl2::?erp ?new-cstmt ?return-types ?last-expr-type? ?new-table) (valid-comp-stmt cstmt fundefp table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-comp-stmt.new-cstmt (b* (((mv acl2::?erp ?new-cstmt ?return-types ?last-expr-type? ?new-table) (valid-comp-stmt cstmt fundefp table ienv))) (comp-stmtp new-cstmt)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-comp-stmt.return-types (b* (((mv acl2::?erp ?new-cstmt ?return-types ?last-expr-type? ?new-table) (valid-comp-stmt cstmt fundefp table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-comp-stmt.last-expr-type? (b* (((mv acl2::?erp ?new-cstmt ?return-types ?last-expr-type? ?new-table) (valid-comp-stmt cstmt fundefp table ienv))) (type-optionp last-expr-type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-comp-stmt.new-table (b* (((mv acl2::?erp ?new-cstmt ?return-types ?last-expr-type? ?new-table) (valid-comp-stmt cstmt fundefp table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item.erp (b* (((mv acl2::?erp ?new-item ?return-types ?last-expr-type? ?new-table) (valid-block-item item table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item.new-item (b* (((mv acl2::?erp ?new-item ?return-types ?last-expr-type? ?new-table) (valid-block-item item table ienv))) (block-itemp new-item)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item.return-types (b* (((mv acl2::?erp ?new-item ?return-types ?last-expr-type? ?new-table) (valid-block-item item table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item.last-expr-type? (b* (((mv acl2::?erp ?new-item ?return-types ?last-expr-type? ?new-table) (valid-block-item item table ienv))) (type-optionp last-expr-type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item.new-table (b* (((mv acl2::?erp ?new-item ?return-types ?last-expr-type? ?new-table) (valid-block-item item table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item-list.erp (b* (((mv acl2::?erp ?new-items ?return-types ?last-expr-type? ?new-table) (valid-block-item-list items table ienv))) (maybe-msgp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item-list.new-items (b* (((mv acl2::?erp ?new-items ?return-types ?last-expr-type? ?new-table) (valid-block-item-list items table ienv))) (block-item-listp new-items)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item-list.return-types (b* (((mv acl2::?erp ?new-items ?return-types ?last-expr-type? ?new-table) (valid-block-item-list items table ienv))) (type-setp return-types)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item-list.last-expr-type? (b* (((mv acl2::?erp ?new-items ?return-types ?last-expr-type? ?new-table) (valid-block-item-list items table ienv))) (type-optionp last-expr-type?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-valid-block-item-list.new-table (b* (((mv acl2::?erp ?new-items ?return-types ?last-expr-type? ?new-table) (valid-block-item-list items table ienv))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm len-of-valid-expr-list.types (b* (((mv acl2::?erp ?new-exprs ?types ?return-types ?new-table) (valid-expr-list exprs table ienv))) (implies (not erp) (equal (len types) (len exprs)))))
Theorem:
(defthm alistp-of-valid-genassoc-list.type-alist (b* (((mv acl2::?erp ?new-genassocs ?type-alist ?return-types ?new-table) (valid-genassoc-list genassocs table ienv))) (alistp type-alist)))
Theorem:
(defthm type-spec-list-unambp-of-valid-type-spec (implies (type-spec-list-unambp tyspecs) (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (type-spec-list-unambp new-tyspecs))))
Theorem:
(defthm not-type-and-type-specs-of-valid-type-spec (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (not (and new-type? new-tyspecs))))
Theorem:
(defthm type-spec-list-unambp-of-valid-spec/qual (implies (type-spec-list-unambp tyspecs) (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (type-spec-list-unambp new-tyspecs))))
Theorem:
(defthm not-type-and-type-specs-of-valid-spec/qual (implies (not (and type? tyspecs)) (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (not (and new-type? new-tyspecs)))))
Theorem:
(defthm not-type-specs-of-valid-spec/qual-when-type (implies (not (and type? tyspecs)) (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (implies new-type? (not new-tyspecs)))))
Theorem:
(defthm type-spec-list-unambp-of-valid-decl-spec (implies (type-spec-list-unambp tyspecs) (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (type-spec-list-unambp new-tyspecs))))
Theorem:
(defthm not-type-and-type-specs-of-valid-decl-spec (implies (not (and type? tyspecs)) (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (not (and new-type? new-tyspecs)))))
Theorem:
(defthm not-type-specs-of-valid-decl-spec-when-type (implies (not (and type? tyspecs)) (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (implies new-type? (not new-tyspecs)))))
Theorem:
(defthm valid-decl-spec.new-storspecs-type-prescription (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (true-listp new-storspecs)) :rule-classes :type-prescription)
Theorem:
(defthm valid-decl-spec-list.all-storspecs-type-prescription (b* (((mv acl2::?erp ?new-declspecs ?type ?all-storspecs ?return-types ?new-table) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv))) (true-listp all-storspecs)) :rule-classes :type-prescription)
Theorem:
(defthm valid-designor.new-target-type-not-function (b* (((mv acl2::?erp ?new-designor ?new-target-type ?return-types ?new-table) (valid-designor designor target-type table ienv))) (implies (not erp) (not (equal (type-kind new-target-type) :function)))))
Theorem:
(defthm valid-designor.new-target-type-not-void (b* (((mv acl2::?erp ?new-designor ?new-target-type ?return-types ?new-table) (valid-designor designor target-type table ienv))) (implies (not erp) (not (equal (type-kind new-target-type) :void)))))
Theorem:
(defthm valid-designor-list.new-target-type-not-function (b* (((mv acl2::?erp ?new-designors ?new-target-type ?return-types ?new-table) (valid-designor-list designors target-type table ienv))) (implies (not erp) (not (equal (type-kind new-target-type) :function)))))
Theorem:
(defthm valid-designor-list.new-target-type-not-void (b* (((mv acl2::?erp ?new-designors ?new-target-type ?return-types ?new-table) (valid-designor-list designors target-type table ienv))) (implies (not erp) (not (equal (type-kind new-target-type) :void)))))
Theorem:
(defthm valid-param-declor.uid?-under-iff (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (implies (not erp) (iff uid? ident?))))
Theorem:
(defthm valid-expr-of-expr-fix-expr (equal (valid-expr (expr-fix expr) table ienv) (valid-expr expr table ienv)))
Theorem:
(defthm valid-expr-of-valid-table-fix-table (equal (valid-expr expr (valid-table-fix table) ienv) (valid-expr expr table ienv)))
Theorem:
(defthm valid-expr-of-ienv-fix-ienv (equal (valid-expr expr table (ienv-fix ienv)) (valid-expr expr table ienv)))
Theorem:
(defthm valid-expr-list-of-expr-list-fix-exprs (equal (valid-expr-list (expr-list-fix exprs) table ienv) (valid-expr-list exprs table ienv)))
Theorem:
(defthm valid-expr-list-of-valid-table-fix-table (equal (valid-expr-list exprs (valid-table-fix table) ienv) (valid-expr-list exprs table ienv)))
Theorem:
(defthm valid-expr-list-of-ienv-fix-ienv (equal (valid-expr-list exprs table (ienv-fix ienv)) (valid-expr-list exprs table ienv)))
Theorem:
(defthm valid-expr-option-of-expr-option-fix-expr? (equal (valid-expr-option (expr-option-fix expr?) table ienv) (valid-expr-option expr? table ienv)))
Theorem:
(defthm valid-expr-option-of-valid-table-fix-table (equal (valid-expr-option expr? (valid-table-fix table) ienv) (valid-expr-option expr? table ienv)))
Theorem:
(defthm valid-expr-option-of-ienv-fix-ienv (equal (valid-expr-option expr? table (ienv-fix ienv)) (valid-expr-option expr? table ienv)))
Theorem:
(defthm valid-const-expr-of-const-expr-fix-cexpr (equal (valid-const-expr (const-expr-fix cexpr) table ienv) (valid-const-expr cexpr table ienv)))
Theorem:
(defthm valid-const-expr-of-valid-table-fix-table (equal (valid-const-expr cexpr (valid-table-fix table) ienv) (valid-const-expr cexpr table ienv)))
Theorem:
(defthm valid-const-expr-of-ienv-fix-ienv (equal (valid-const-expr cexpr table (ienv-fix ienv)) (valid-const-expr cexpr table ienv)))
Theorem:
(defthm valid-const-expr-option-of-const-expr-option-fix-cexpr? (equal (valid-const-expr-option (const-expr-option-fix cexpr?) table ienv) (valid-const-expr-option cexpr? table ienv)))
Theorem:
(defthm valid-const-expr-option-of-valid-table-fix-table (equal (valid-const-expr-option cexpr? (valid-table-fix table) ienv) (valid-const-expr-option cexpr? table ienv)))
Theorem:
(defthm valid-const-expr-option-of-ienv-fix-ienv (equal (valid-const-expr-option cexpr? table (ienv-fix ienv)) (valid-const-expr-option cexpr? table ienv)))
Theorem:
(defthm valid-genassoc-of-genassoc-fix-genassoc (equal (valid-genassoc (genassoc-fix genassoc) table ienv) (valid-genassoc genassoc table ienv)))
Theorem:
(defthm valid-genassoc-of-valid-table-fix-table (equal (valid-genassoc genassoc (valid-table-fix table) ienv) (valid-genassoc genassoc table ienv)))
Theorem:
(defthm valid-genassoc-of-ienv-fix-ienv (equal (valid-genassoc genassoc table (ienv-fix ienv)) (valid-genassoc genassoc table ienv)))
Theorem:
(defthm valid-genassoc-list-of-genassoc-list-fix-genassocs (equal (valid-genassoc-list (genassoc-list-fix genassocs) table ienv) (valid-genassoc-list genassocs table ienv)))
Theorem:
(defthm valid-genassoc-list-of-valid-table-fix-table (equal (valid-genassoc-list genassocs (valid-table-fix table) ienv) (valid-genassoc-list genassocs table ienv)))
Theorem:
(defthm valid-genassoc-list-of-ienv-fix-ienv (equal (valid-genassoc-list genassocs table (ienv-fix ienv)) (valid-genassoc-list genassocs table ienv)))
Theorem:
(defthm valid-member-designor-of-member-designor-fix-memdesign (equal (valid-member-designor (member-designor-fix memdesign) table ienv) (valid-member-designor memdesign table ienv)))
Theorem:
(defthm valid-member-designor-of-valid-table-fix-table (equal (valid-member-designor memdesign (valid-table-fix table) ienv) (valid-member-designor memdesign table ienv)))
Theorem:
(defthm valid-member-designor-of-ienv-fix-ienv (equal (valid-member-designor memdesign table (ienv-fix ienv)) (valid-member-designor memdesign table ienv)))
Theorem:
(defthm valid-type-spec-of-type-spec-fix-tyspec (equal (valid-type-spec (type-spec-fix tyspec) type? tyspecs table ienv) (valid-type-spec tyspec type? tyspecs table ienv)))
Theorem:
(defthm valid-type-spec-of-type-option-fix-type? (equal (valid-type-spec tyspec (type-option-fix type?) tyspecs table ienv) (valid-type-spec tyspec type? tyspecs table ienv)))
Theorem:
(defthm valid-type-spec-of-type-spec-list-fix-tyspecs (equal (valid-type-spec tyspec type? (type-spec-list-fix tyspecs) table ienv) (valid-type-spec tyspec type? tyspecs table ienv)))
Theorem:
(defthm valid-type-spec-of-valid-table-fix-table (equal (valid-type-spec tyspec type? tyspecs (valid-table-fix table) ienv) (valid-type-spec tyspec type? tyspecs table ienv)))
Theorem:
(defthm valid-type-spec-of-ienv-fix-ienv (equal (valid-type-spec tyspec type? tyspecs table (ienv-fix ienv)) (valid-type-spec tyspec type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-of-spec/qual-fix-specqual (equal (valid-spec/qual (spec/qual-fix specqual) type? tyspecs table ienv) (valid-spec/qual specqual type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-of-type-option-fix-type? (equal (valid-spec/qual specqual (type-option-fix type?) tyspecs table ienv) (valid-spec/qual specqual type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-of-type-spec-list-fix-tyspecs (equal (valid-spec/qual specqual type? (type-spec-list-fix tyspecs) table ienv) (valid-spec/qual specqual type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-of-valid-table-fix-table (equal (valid-spec/qual specqual type? tyspecs (valid-table-fix table) ienv) (valid-spec/qual specqual type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-of-ienv-fix-ienv (equal (valid-spec/qual specqual type? tyspecs table (ienv-fix ienv)) (valid-spec/qual specqual type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-list-of-spec/qual-list-fix-specquals (equal (valid-spec/qual-list (spec/qual-list-fix specquals) type? tyspecs table ienv) (valid-spec/qual-list specquals type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-list-of-type-option-fix-type? (equal (valid-spec/qual-list specquals (type-option-fix type?) tyspecs table ienv) (valid-spec/qual-list specquals type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-list-of-type-spec-list-fix-tyspecs (equal (valid-spec/qual-list specquals type? (type-spec-list-fix tyspecs) table ienv) (valid-spec/qual-list specquals type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-list-of-valid-table-fix-table (equal (valid-spec/qual-list specquals type? tyspecs (valid-table-fix table) ienv) (valid-spec/qual-list specquals type? tyspecs table ienv)))
Theorem:
(defthm valid-spec/qual-list-of-ienv-fix-ienv (equal (valid-spec/qual-list specquals type? tyspecs table (ienv-fix ienv)) (valid-spec/qual-list specquals type? tyspecs table ienv)))
Theorem:
(defthm valid-align-spec-of-align-spec-fix-align (equal (valid-align-spec (align-spec-fix align) table ienv) (valid-align-spec align table ienv)))
Theorem:
(defthm valid-align-spec-of-valid-table-fix-table (equal (valid-align-spec align (valid-table-fix table) ienv) (valid-align-spec align table ienv)))
Theorem:
(defthm valid-align-spec-of-ienv-fix-ienv (equal (valid-align-spec align table (ienv-fix ienv)) (valid-align-spec align table ienv)))
Theorem:
(defthm valid-decl-spec-of-decl-spec-fix-declspec (equal (valid-decl-spec (decl-spec-fix declspec) type? tyspecs storspecs table ienv) (valid-decl-spec declspec type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-of-type-option-fix-type? (equal (valid-decl-spec declspec (type-option-fix type?) tyspecs storspecs table ienv) (valid-decl-spec declspec type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-of-type-spec-list-fix-tyspecs (equal (valid-decl-spec declspec type? (type-spec-list-fix tyspecs) storspecs table ienv) (valid-decl-spec declspec type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-of-stor-spec-list-fix-storspecs (equal (valid-decl-spec declspec type? tyspecs (stor-spec-list-fix storspecs) table ienv) (valid-decl-spec declspec type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-of-valid-table-fix-table (equal (valid-decl-spec declspec type? tyspecs storspecs (valid-table-fix table) ienv) (valid-decl-spec declspec type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-of-ienv-fix-ienv (equal (valid-decl-spec declspec type? tyspecs storspecs table (ienv-fix ienv)) (valid-decl-spec declspec type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-list-of-decl-spec-list-fix-declspecs (equal (valid-decl-spec-list (decl-spec-list-fix declspecs) type? tyspecs storspecs table ienv) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-list-of-type-option-fix-type? (equal (valid-decl-spec-list declspecs (type-option-fix type?) tyspecs storspecs table ienv) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-list-of-type-spec-list-fix-tyspecs (equal (valid-decl-spec-list declspecs type? (type-spec-list-fix tyspecs) storspecs table ienv) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-list-of-stor-spec-list-fix-storspecs (equal (valid-decl-spec-list declspecs type? tyspecs (stor-spec-list-fix storspecs) table ienv) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-list-of-valid-table-fix-table (equal (valid-decl-spec-list declspecs type? tyspecs storspecs (valid-table-fix table) ienv) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-decl-spec-list-of-ienv-fix-ienv (equal (valid-decl-spec-list declspecs type? tyspecs storspecs table (ienv-fix ienv)) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv)))
Theorem:
(defthm valid-initer-of-initer-fix-initer (equal (valid-initer (initer-fix initer) target-type lifetime table ienv) (valid-initer initer target-type lifetime table ienv)))
Theorem:
(defthm valid-initer-of-type-fix-target-type (equal (valid-initer initer (type-fix target-type) lifetime table ienv) (valid-initer initer target-type lifetime table ienv)))
Theorem:
(defthm valid-initer-of-lifetime-fix-lifetime (equal (valid-initer initer target-type (lifetime-fix lifetime) table ienv) (valid-initer initer target-type lifetime table ienv)))
Theorem:
(defthm valid-initer-of-valid-table-fix-table (equal (valid-initer initer target-type lifetime (valid-table-fix table) ienv) (valid-initer initer target-type lifetime table ienv)))
Theorem:
(defthm valid-initer-of-ienv-fix-ienv (equal (valid-initer initer target-type lifetime table (ienv-fix ienv)) (valid-initer initer target-type lifetime table ienv)))
Theorem:
(defthm valid-initer-option-of-initer-option-fix-initer? (equal (valid-initer-option (initer-option-fix initer?) target-type lifetime? table ienv) (valid-initer-option initer? target-type lifetime? table ienv)))
Theorem:
(defthm valid-initer-option-of-type-fix-target-type (equal (valid-initer-option initer? (type-fix target-type) lifetime? table ienv) (valid-initer-option initer? target-type lifetime? table ienv)))
Theorem:
(defthm valid-initer-option-of-lifetime-option-fix-lifetime? (equal (valid-initer-option initer? target-type (lifetime-option-fix lifetime?) table ienv) (valid-initer-option initer? target-type lifetime? table ienv)))
Theorem:
(defthm valid-initer-option-of-valid-table-fix-table (equal (valid-initer-option initer? target-type lifetime? (valid-table-fix table) ienv) (valid-initer-option initer? target-type lifetime? table ienv)))
Theorem:
(defthm valid-initer-option-of-ienv-fix-ienv (equal (valid-initer-option initer? target-type lifetime? table (ienv-fix ienv)) (valid-initer-option initer? target-type lifetime? table ienv)))
Theorem:
(defthm valid-desiniter-of-desiniter-fix-desiniter (equal (valid-desiniter (desiniter-fix desiniter) target-type lifetime table ienv) (valid-desiniter desiniter target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-of-type-fix-target-type (equal (valid-desiniter desiniter (type-fix target-type) lifetime table ienv) (valid-desiniter desiniter target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-of-lifetime-fix-lifetime (equal (valid-desiniter desiniter target-type (lifetime-fix lifetime) table ienv) (valid-desiniter desiniter target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-of-valid-table-fix-table (equal (valid-desiniter desiniter target-type lifetime (valid-table-fix table) ienv) (valid-desiniter desiniter target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-of-ienv-fix-ienv (equal (valid-desiniter desiniter target-type lifetime table (ienv-fix ienv)) (valid-desiniter desiniter target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-list-of-desiniter-list-fix-desiniters (equal (valid-desiniter-list (desiniter-list-fix desiniters) target-type lifetime table ienv) (valid-desiniter-list desiniters target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-list-of-type-fix-target-type (equal (valid-desiniter-list desiniters (type-fix target-type) lifetime table ienv) (valid-desiniter-list desiniters target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-list-of-lifetime-fix-lifetime (equal (valid-desiniter-list desiniters target-type (lifetime-fix lifetime) table ienv) (valid-desiniter-list desiniters target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-list-of-valid-table-fix-table (equal (valid-desiniter-list desiniters target-type lifetime (valid-table-fix table) ienv) (valid-desiniter-list desiniters target-type lifetime table ienv)))
Theorem:
(defthm valid-desiniter-list-of-ienv-fix-ienv (equal (valid-desiniter-list desiniters target-type lifetime table (ienv-fix ienv)) (valid-desiniter-list desiniters target-type lifetime table ienv)))
Theorem:
(defthm valid-designor-of-designor-fix-designor (equal (valid-designor (designor-fix designor) target-type table ienv) (valid-designor designor target-type table ienv)))
Theorem:
(defthm valid-designor-of-type-fix-target-type (equal (valid-designor designor (type-fix target-type) table ienv) (valid-designor designor target-type table ienv)))
Theorem:
(defthm valid-designor-of-valid-table-fix-table (equal (valid-designor designor target-type (valid-table-fix table) ienv) (valid-designor designor target-type table ienv)))
Theorem:
(defthm valid-designor-of-ienv-fix-ienv (equal (valid-designor designor target-type table (ienv-fix ienv)) (valid-designor designor target-type table ienv)))
Theorem:
(defthm valid-designor-list-of-designor-list-fix-designors (equal (valid-designor-list (designor-list-fix designors) target-type table ienv) (valid-designor-list designors target-type table ienv)))
Theorem:
(defthm valid-designor-list-of-type-fix-target-type (equal (valid-designor-list designors (type-fix target-type) table ienv) (valid-designor-list designors target-type table ienv)))
Theorem:
(defthm valid-designor-list-of-valid-table-fix-table (equal (valid-designor-list designors target-type (valid-table-fix table) ienv) (valid-designor-list designors target-type table ienv)))
Theorem:
(defthm valid-designor-list-of-ienv-fix-ienv (equal (valid-designor-list designors target-type table (ienv-fix ienv)) (valid-designor-list designors target-type table ienv)))
Theorem:
(defthm valid-declor-of-declor-fix-declor (equal (valid-declor (declor-fix declor) fundef-params-p type table ienv) (valid-declor declor fundef-params-p type table ienv)))
Theorem:
(defthm valid-declor-of-bool-fix-fundef-params-p (equal (valid-declor declor (bool-fix fundef-params-p) type table ienv) (valid-declor declor fundef-params-p type table ienv)))
Theorem:
(defthm valid-declor-of-type-fix-type (equal (valid-declor declor fundef-params-p (type-fix type) table ienv) (valid-declor declor fundef-params-p type table ienv)))
Theorem:
(defthm valid-declor-of-valid-table-fix-table (equal (valid-declor declor fundef-params-p type (valid-table-fix table) ienv) (valid-declor declor fundef-params-p type table ienv)))
Theorem:
(defthm valid-declor-of-ienv-fix-ienv (equal (valid-declor declor fundef-params-p type table (ienv-fix ienv)) (valid-declor declor fundef-params-p type table ienv)))
Theorem:
(defthm valid-declor-option-of-declor-option-fix-declor? (equal (valid-declor-option (declor-option-fix declor?) type table ienv) (valid-declor-option declor? type table ienv)))
Theorem:
(defthm valid-declor-option-of-type-fix-type (equal (valid-declor-option declor? (type-fix type) table ienv) (valid-declor-option declor? type table ienv)))
Theorem:
(defthm valid-declor-option-of-valid-table-fix-table (equal (valid-declor-option declor? type (valid-table-fix table) ienv) (valid-declor-option declor? type table ienv)))
Theorem:
(defthm valid-declor-option-of-ienv-fix-ienv (equal (valid-declor-option declor? type table (ienv-fix ienv)) (valid-declor-option declor? type table ienv)))
Theorem:
(defthm valid-dirdeclor-of-dirdeclor-fix-dirdeclor (equal (valid-dirdeclor (dirdeclor-fix dirdeclor) fundef-params-p type table ienv) (valid-dirdeclor dirdeclor fundef-params-p type table ienv)))
Theorem:
(defthm valid-dirdeclor-of-bool-fix-fundef-params-p (equal (valid-dirdeclor dirdeclor (bool-fix fundef-params-p) type table ienv) (valid-dirdeclor dirdeclor fundef-params-p type table ienv)))
Theorem:
(defthm valid-dirdeclor-of-type-fix-type (equal (valid-dirdeclor dirdeclor fundef-params-p (type-fix type) table ienv) (valid-dirdeclor dirdeclor fundef-params-p type table ienv)))
Theorem:
(defthm valid-dirdeclor-of-valid-table-fix-table (equal (valid-dirdeclor dirdeclor fundef-params-p type (valid-table-fix table) ienv) (valid-dirdeclor dirdeclor fundef-params-p type table ienv)))
Theorem:
(defthm valid-dirdeclor-of-ienv-fix-ienv (equal (valid-dirdeclor dirdeclor fundef-params-p type table (ienv-fix ienv)) (valid-dirdeclor dirdeclor fundef-params-p type table ienv)))
Theorem:
(defthm valid-absdeclor-of-absdeclor-fix-absdeclor (equal (valid-absdeclor (absdeclor-fix absdeclor) type table ienv) (valid-absdeclor absdeclor type table ienv)))
Theorem:
(defthm valid-absdeclor-of-type-fix-type (equal (valid-absdeclor absdeclor (type-fix type) table ienv) (valid-absdeclor absdeclor type table ienv)))
Theorem:
(defthm valid-absdeclor-of-valid-table-fix-table (equal (valid-absdeclor absdeclor type (valid-table-fix table) ienv) (valid-absdeclor absdeclor type table ienv)))
Theorem:
(defthm valid-absdeclor-of-ienv-fix-ienv (equal (valid-absdeclor absdeclor type table (ienv-fix ienv)) (valid-absdeclor absdeclor type table ienv)))
Theorem:
(defthm valid-absdeclor-option-of-absdeclor-option-fix-absdeclor? (equal (valid-absdeclor-option (absdeclor-option-fix absdeclor?) type table ienv) (valid-absdeclor-option absdeclor? type table ienv)))
Theorem:
(defthm valid-absdeclor-option-of-type-fix-type (equal (valid-absdeclor-option absdeclor? (type-fix type) table ienv) (valid-absdeclor-option absdeclor? type table ienv)))
Theorem:
(defthm valid-absdeclor-option-of-valid-table-fix-table (equal (valid-absdeclor-option absdeclor? type (valid-table-fix table) ienv) (valid-absdeclor-option absdeclor? type table ienv)))
Theorem:
(defthm valid-absdeclor-option-of-ienv-fix-ienv (equal (valid-absdeclor-option absdeclor? type table (ienv-fix ienv)) (valid-absdeclor-option absdeclor? type table ienv)))
Theorem:
(defthm valid-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor (equal (valid-dirabsdeclor (dirabsdeclor-fix dirabsdeclor) type table ienv) (valid-dirabsdeclor dirabsdeclor type table ienv)))
Theorem:
(defthm valid-dirabsdeclor-of-type-fix-type (equal (valid-dirabsdeclor dirabsdeclor (type-fix type) table ienv) (valid-dirabsdeclor dirabsdeclor type table ienv)))
Theorem:
(defthm valid-dirabsdeclor-of-valid-table-fix-table (equal (valid-dirabsdeclor dirabsdeclor type (valid-table-fix table) ienv) (valid-dirabsdeclor dirabsdeclor type table ienv)))
Theorem:
(defthm valid-dirabsdeclor-of-ienv-fix-ienv (equal (valid-dirabsdeclor dirabsdeclor type table (ienv-fix ienv)) (valid-dirabsdeclor dirabsdeclor type table ienv)))
Theorem:
(defthm valid-dirabsdeclor-option-of-dirabsdeclor-option-fix-dirabsdeclor? (equal (valid-dirabsdeclor-option (dirabsdeclor-option-fix dirabsdeclor?) type table ienv) (valid-dirabsdeclor-option dirabsdeclor? type table ienv)))
Theorem:
(defthm valid-dirabsdeclor-option-of-type-fix-type (equal (valid-dirabsdeclor-option dirabsdeclor? (type-fix type) table ienv) (valid-dirabsdeclor-option dirabsdeclor? type table ienv)))
Theorem:
(defthm valid-dirabsdeclor-option-of-valid-table-fix-table (equal (valid-dirabsdeclor-option dirabsdeclor? type (valid-table-fix table) ienv) (valid-dirabsdeclor-option dirabsdeclor? type table ienv)))
Theorem:
(defthm valid-dirabsdeclor-option-of-ienv-fix-ienv (equal (valid-dirabsdeclor-option dirabsdeclor? type table (ienv-fix ienv)) (valid-dirabsdeclor-option dirabsdeclor? type table ienv)))
Theorem:
(defthm valid-param-declon-of-param-declon-fix-paramdecl (equal (valid-param-declon (param-declon-fix paramdecl) fundef-params-p table ienv) (valid-param-declon paramdecl fundef-params-p table ienv)))
Theorem:
(defthm valid-param-declon-of-bool-fix-fundef-params-p (equal (valid-param-declon paramdecl (bool-fix fundef-params-p) table ienv) (valid-param-declon paramdecl fundef-params-p table ienv)))
Theorem:
(defthm valid-param-declon-of-valid-table-fix-table (equal (valid-param-declon paramdecl fundef-params-p (valid-table-fix table) ienv) (valid-param-declon paramdecl fundef-params-p table ienv)))
Theorem:
(defthm valid-param-declon-of-ienv-fix-ienv (equal (valid-param-declon paramdecl fundef-params-p table (ienv-fix ienv)) (valid-param-declon paramdecl fundef-params-p table ienv)))
Theorem:
(defthm valid-param-declon-list-of-param-declon-list-fix-paramdecls (equal (valid-param-declon-list (param-declon-list-fix paramdecls) fundef-params-p table ienv) (valid-param-declon-list paramdecls fundef-params-p table ienv)))
Theorem:
(defthm valid-param-declon-list-of-bool-fix-fundef-params-p (equal (valid-param-declon-list paramdecls (bool-fix fundef-params-p) table ienv) (valid-param-declon-list paramdecls fundef-params-p table ienv)))
Theorem:
(defthm valid-param-declon-list-of-valid-table-fix-table (equal (valid-param-declon-list paramdecls fundef-params-p (valid-table-fix table) ienv) (valid-param-declon-list paramdecls fundef-params-p table ienv)))
Theorem:
(defthm valid-param-declon-list-of-ienv-fix-ienv (equal (valid-param-declon-list paramdecls fundef-params-p table (ienv-fix ienv)) (valid-param-declon-list paramdecls fundef-params-p table ienv)))
Theorem:
(defthm valid-param-declor-of-param-declor-fix-paramdeclor (equal (valid-param-declor (param-declor-fix paramdeclor) type table ienv) (valid-param-declor paramdeclor type table ienv)))
Theorem:
(defthm valid-param-declor-of-type-fix-type (equal (valid-param-declor paramdeclor (type-fix type) table ienv) (valid-param-declor paramdeclor type table ienv)))
Theorem:
(defthm valid-param-declor-of-valid-table-fix-table (equal (valid-param-declor paramdeclor type (valid-table-fix table) ienv) (valid-param-declor paramdeclor type table ienv)))
Theorem:
(defthm valid-param-declor-of-ienv-fix-ienv (equal (valid-param-declor paramdeclor type table (ienv-fix ienv)) (valid-param-declor paramdeclor type table ienv)))
Theorem:
(defthm valid-tyname-of-tyname-fix-tyname (equal (valid-tyname (tyname-fix tyname) table ienv) (valid-tyname tyname table ienv)))
Theorem:
(defthm valid-tyname-of-valid-table-fix-table (equal (valid-tyname tyname (valid-table-fix table) ienv) (valid-tyname tyname table ienv)))
Theorem:
(defthm valid-tyname-of-ienv-fix-ienv (equal (valid-tyname tyname table (ienv-fix ienv)) (valid-tyname tyname table ienv)))
Theorem:
(defthm valid-struni-spec-of-struni-spec-fix-struni-spec (equal (valid-struni-spec (struni-spec-fix struni-spec) table ienv) (valid-struni-spec struni-spec table ienv)))
Theorem:
(defthm valid-struni-spec-of-valid-table-fix-table (equal (valid-struni-spec struni-spec (valid-table-fix table) ienv) (valid-struni-spec struni-spec table ienv)))
Theorem:
(defthm valid-struni-spec-of-ienv-fix-ienv (equal (valid-struni-spec struni-spec table (ienv-fix ienv)) (valid-struni-spec struni-spec table ienv)))
Theorem:
(defthm valid-struct-declon-of-struct-declon-fix-structdeclon (equal (valid-struct-declon (struct-declon-fix structdeclon) previous table ienv) (valid-struct-declon structdeclon previous table ienv)))
Theorem:
(defthm valid-struct-declon-of-ident-list-fix-previous (equal (valid-struct-declon structdeclon (ident-list-fix previous) table ienv) (valid-struct-declon structdeclon previous table ienv)))
Theorem:
(defthm valid-struct-declon-of-valid-table-fix-table (equal (valid-struct-declon structdeclon previous (valid-table-fix table) ienv) (valid-struct-declon structdeclon previous table ienv)))
Theorem:
(defthm valid-struct-declon-of-ienv-fix-ienv (equal (valid-struct-declon structdeclon previous table (ienv-fix ienv)) (valid-struct-declon structdeclon previous table ienv)))
Theorem:
(defthm valid-struct-declon-list-of-struct-declon-list-fix-structdeclons (equal (valid-struct-declon-list (struct-declon-list-fix structdeclons) previous table ienv) (valid-struct-declon-list structdeclons previous table ienv)))
Theorem:
(defthm valid-struct-declon-list-of-ident-list-fix-previous (equal (valid-struct-declon-list structdeclons (ident-list-fix previous) table ienv) (valid-struct-declon-list structdeclons previous table ienv)))
Theorem:
(defthm valid-struct-declon-list-of-valid-table-fix-table (equal (valid-struct-declon-list structdeclons previous (valid-table-fix table) ienv) (valid-struct-declon-list structdeclons previous table ienv)))
Theorem:
(defthm valid-struct-declon-list-of-ienv-fix-ienv (equal (valid-struct-declon-list structdeclons previous table (ienv-fix ienv)) (valid-struct-declon-list structdeclons previous table ienv)))
Theorem:
(defthm valid-struct-declor-of-struct-declor-fix-structdeclor (equal (valid-struct-declor (struct-declor-fix structdeclor) previous type table ienv) (valid-struct-declor structdeclor previous type table ienv)))
Theorem:
(defthm valid-struct-declor-of-ident-list-fix-previous (equal (valid-struct-declor structdeclor (ident-list-fix previous) type table ienv) (valid-struct-declor structdeclor previous type table ienv)))
Theorem:
(defthm valid-struct-declor-of-type-fix-type (equal (valid-struct-declor structdeclor previous (type-fix type) table ienv) (valid-struct-declor structdeclor previous type table ienv)))
Theorem:
(defthm valid-struct-declor-of-valid-table-fix-table (equal (valid-struct-declor structdeclor previous type (valid-table-fix table) ienv) (valid-struct-declor structdeclor previous type table ienv)))
Theorem:
(defthm valid-struct-declor-of-ienv-fix-ienv (equal (valid-struct-declor structdeclor previous type table (ienv-fix ienv)) (valid-struct-declor structdeclor previous type table ienv)))
Theorem:
(defthm valid-struct-declor-list-of-struct-declor-list-fix-structdeclors (equal (valid-struct-declor-list (struct-declor-list-fix structdeclors) previous type table ienv) (valid-struct-declor-list structdeclors previous type table ienv)))
Theorem:
(defthm valid-struct-declor-list-of-ident-list-fix-previous (equal (valid-struct-declor-list structdeclors (ident-list-fix previous) type table ienv) (valid-struct-declor-list structdeclors previous type table ienv)))
Theorem:
(defthm valid-struct-declor-list-of-type-fix-type (equal (valid-struct-declor-list structdeclors previous (type-fix type) table ienv) (valid-struct-declor-list structdeclors previous type table ienv)))
Theorem:
(defthm valid-struct-declor-list-of-valid-table-fix-table (equal (valid-struct-declor-list structdeclors previous type (valid-table-fix table) ienv) (valid-struct-declor-list structdeclors previous type table ienv)))
Theorem:
(defthm valid-struct-declor-list-of-ienv-fix-ienv (equal (valid-struct-declor-list structdeclors previous type table (ienv-fix ienv)) (valid-struct-declor-list structdeclors previous type table ienv)))
Theorem:
(defthm valid-enum-spec-of-enum-spec-fix-enumspec (equal (valid-enum-spec (enum-spec-fix enumspec) table ienv) (valid-enum-spec enumspec table ienv)))
Theorem:
(defthm valid-enum-spec-of-valid-table-fix-table (equal (valid-enum-spec enumspec (valid-table-fix table) ienv) (valid-enum-spec enumspec table ienv)))
Theorem:
(defthm valid-enum-spec-of-ienv-fix-ienv (equal (valid-enum-spec enumspec table (ienv-fix ienv)) (valid-enum-spec enumspec table ienv)))
Theorem:
(defthm valid-enumer-of-enumer-fix-enumer (equal (valid-enumer (enumer-fix enumer) table ienv) (valid-enumer enumer table ienv)))
Theorem:
(defthm valid-enumer-of-valid-table-fix-table (equal (valid-enumer enumer (valid-table-fix table) ienv) (valid-enumer enumer table ienv)))
Theorem:
(defthm valid-enumer-of-ienv-fix-ienv (equal (valid-enumer enumer table (ienv-fix ienv)) (valid-enumer enumer table ienv)))
Theorem:
(defthm valid-enumer-list-of-enumer-list-fix-enumers (equal (valid-enumer-list (enumer-list-fix enumers) table ienv) (valid-enumer-list enumers table ienv)))
Theorem:
(defthm valid-enumer-list-of-valid-table-fix-table (equal (valid-enumer-list enumers (valid-table-fix table) ienv) (valid-enumer-list enumers table ienv)))
Theorem:
(defthm valid-enumer-list-of-ienv-fix-ienv (equal (valid-enumer-list enumers table (ienv-fix ienv)) (valid-enumer-list enumers table ienv)))
Theorem:
(defthm valid-statassert-of-statassert-fix-statassert (equal (valid-statassert (statassert-fix statassert) table ienv) (valid-statassert statassert table ienv)))
Theorem:
(defthm valid-statassert-of-valid-table-fix-table (equal (valid-statassert statassert (valid-table-fix table) ienv) (valid-statassert statassert table ienv)))
Theorem:
(defthm valid-statassert-of-ienv-fix-ienv (equal (valid-statassert statassert table (ienv-fix ienv)) (valid-statassert statassert table ienv)))
Theorem:
(defthm valid-init-declor-of-init-declor-fix-initdeclor (equal (valid-init-declor (init-declor-fix initdeclor) type storspecs table ienv) (valid-init-declor initdeclor type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-of-type-fix-type (equal (valid-init-declor initdeclor (type-fix type) storspecs table ienv) (valid-init-declor initdeclor type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-of-stor-spec-list-fix-storspecs (equal (valid-init-declor initdeclor type (stor-spec-list-fix storspecs) table ienv) (valid-init-declor initdeclor type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-of-valid-table-fix-table (equal (valid-init-declor initdeclor type storspecs (valid-table-fix table) ienv) (valid-init-declor initdeclor type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-of-ienv-fix-ienv (equal (valid-init-declor initdeclor type storspecs table (ienv-fix ienv)) (valid-init-declor initdeclor type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-list-of-init-declor-list-fix-initdeclors (equal (valid-init-declor-list (init-declor-list-fix initdeclors) type storspecs table ienv) (valid-init-declor-list initdeclors type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-list-of-type-fix-type (equal (valid-init-declor-list initdeclors (type-fix type) storspecs table ienv) (valid-init-declor-list initdeclors type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-list-of-stor-spec-list-fix-storspecs (equal (valid-init-declor-list initdeclors type (stor-spec-list-fix storspecs) table ienv) (valid-init-declor-list initdeclors type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-list-of-valid-table-fix-table (equal (valid-init-declor-list initdeclors type storspecs (valid-table-fix table) ienv) (valid-init-declor-list initdeclors type storspecs table ienv)))
Theorem:
(defthm valid-init-declor-list-of-ienv-fix-ienv (equal (valid-init-declor-list initdeclors type storspecs table (ienv-fix ienv)) (valid-init-declor-list initdeclors type storspecs table ienv)))
Theorem:
(defthm valid-declon-of-declon-fix-declon (equal (valid-declon (declon-fix declon) table ienv) (valid-declon declon table ienv)))
Theorem:
(defthm valid-declon-of-valid-table-fix-table (equal (valid-declon declon (valid-table-fix table) ienv) (valid-declon declon table ienv)))
Theorem:
(defthm valid-declon-of-ienv-fix-ienv (equal (valid-declon declon table (ienv-fix ienv)) (valid-declon declon table ienv)))
Theorem:
(defthm valid-declon-list-of-declon-list-fix-declons (equal (valid-declon-list (declon-list-fix declons) table ienv) (valid-declon-list declons table ienv)))
Theorem:
(defthm valid-declon-list-of-valid-table-fix-table (equal (valid-declon-list declons (valid-table-fix table) ienv) (valid-declon-list declons table ienv)))
Theorem:
(defthm valid-declon-list-of-ienv-fix-ienv (equal (valid-declon-list declons table (ienv-fix ienv)) (valid-declon-list declons table ienv)))
Theorem:
(defthm valid-label-of-label-fix-label (equal (valid-label (label-fix label) table ienv) (valid-label label table ienv)))
Theorem:
(defthm valid-label-of-valid-table-fix-table (equal (valid-label label (valid-table-fix table) ienv) (valid-label label table ienv)))
Theorem:
(defthm valid-label-of-ienv-fix-ienv (equal (valid-label label table (ienv-fix ienv)) (valid-label label table ienv)))
Theorem:
(defthm valid-stmt-of-stmt-fix-stmt (equal (valid-stmt (stmt-fix stmt) table ienv) (valid-stmt stmt table ienv)))
Theorem:
(defthm valid-stmt-of-valid-table-fix-table (equal (valid-stmt stmt (valid-table-fix table) ienv) (valid-stmt stmt table ienv)))
Theorem:
(defthm valid-stmt-of-ienv-fix-ienv (equal (valid-stmt stmt table (ienv-fix ienv)) (valid-stmt stmt table ienv)))
Theorem:
(defthm valid-comp-stmt-of-comp-stmt-fix-cstmt (equal (valid-comp-stmt (comp-stmt-fix cstmt) fundefp table ienv) (valid-comp-stmt cstmt fundefp table ienv)))
Theorem:
(defthm valid-comp-stmt-of-bool-fix-fundefp (equal (valid-comp-stmt cstmt (bool-fix fundefp) table ienv) (valid-comp-stmt cstmt fundefp table ienv)))
Theorem:
(defthm valid-comp-stmt-of-valid-table-fix-table (equal (valid-comp-stmt cstmt fundefp (valid-table-fix table) ienv) (valid-comp-stmt cstmt fundefp table ienv)))
Theorem:
(defthm valid-comp-stmt-of-ienv-fix-ienv (equal (valid-comp-stmt cstmt fundefp table (ienv-fix ienv)) (valid-comp-stmt cstmt fundefp table ienv)))
Theorem:
(defthm valid-block-item-of-block-item-fix-item (equal (valid-block-item (block-item-fix item) table ienv) (valid-block-item item table ienv)))
Theorem:
(defthm valid-block-item-of-valid-table-fix-table (equal (valid-block-item item (valid-table-fix table) ienv) (valid-block-item item table ienv)))
Theorem:
(defthm valid-block-item-of-ienv-fix-ienv (equal (valid-block-item item table (ienv-fix ienv)) (valid-block-item item table ienv)))
Theorem:
(defthm valid-block-item-list-of-block-item-list-fix-items (equal (valid-block-item-list (block-item-list-fix items) table ienv) (valid-block-item-list items table ienv)))
Theorem:
(defthm valid-block-item-list-of-valid-table-fix-table (equal (valid-block-item-list items (valid-table-fix table) ienv) (valid-block-item-list items table ienv)))
Theorem:
(defthm valid-block-item-list-of-ienv-fix-ienv (equal (valid-block-item-list items table (ienv-fix ienv)) (valid-block-item-list items table ienv)))
Theorem:
(defthm valid-expr-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (valid-expr expr table ienv) (valid-expr expr-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-expr-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-expr expr table ienv) (valid-expr expr table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-expr-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-expr expr table ienv) (valid-expr expr table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-expr-list-expr-list-equiv-congruence-on-exprs (implies (expr-list-equiv exprs exprs-equiv) (equal (valid-expr-list exprs table ienv) (valid-expr-list exprs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-expr-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-expr-list exprs table ienv) (valid-expr-list exprs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-expr-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-expr-list exprs table ienv) (valid-expr-list exprs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-expr-option-expr-option-equiv-congruence-on-expr? (implies (expr-option-equiv expr? expr?-equiv) (equal (valid-expr-option expr? table ienv) (valid-expr-option expr?-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-expr-option-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-expr-option expr? table ienv) (valid-expr-option expr? table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-expr-option-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-expr-option expr? table ienv) (valid-expr-option expr? table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-const-expr-const-expr-equiv-congruence-on-cexpr (implies (const-expr-equiv cexpr cexpr-equiv) (equal (valid-const-expr cexpr table ienv) (valid-const-expr cexpr-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-const-expr-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-const-expr cexpr table ienv) (valid-const-expr cexpr table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-const-expr-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-const-expr cexpr table ienv) (valid-const-expr cexpr table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-const-expr-option-const-expr-option-equiv-congruence-on-cexpr? (implies (const-expr-option-equiv cexpr? cexpr?-equiv) (equal (valid-const-expr-option cexpr? table ienv) (valid-const-expr-option cexpr?-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-const-expr-option-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-const-expr-option cexpr? table ienv) (valid-const-expr-option cexpr? table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-const-expr-option-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-const-expr-option cexpr? table ienv) (valid-const-expr-option cexpr? table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-genassoc-genassoc-equiv-congruence-on-genassoc (implies (genassoc-equiv genassoc genassoc-equiv) (equal (valid-genassoc genassoc table ienv) (valid-genassoc genassoc-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-genassoc-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-genassoc genassoc table ienv) (valid-genassoc genassoc table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-genassoc-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-genassoc genassoc table ienv) (valid-genassoc genassoc table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-genassoc-list-genassoc-list-equiv-congruence-on-genassocs (implies (genassoc-list-equiv genassocs genassocs-equiv) (equal (valid-genassoc-list genassocs table ienv) (valid-genassoc-list genassocs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-genassoc-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-genassoc-list genassocs table ienv) (valid-genassoc-list genassocs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-genassoc-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-genassoc-list genassocs table ienv) (valid-genassoc-list genassocs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-member-designor-member-designor-equiv-congruence-on-memdesign (implies (member-designor-equiv memdesign memdesign-equiv) (equal (valid-member-designor memdesign table ienv) (valid-member-designor memdesign-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-member-designor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-member-designor memdesign table ienv) (valid-member-designor memdesign table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-member-designor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-member-designor memdesign table ienv) (valid-member-designor memdesign table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-type-spec-type-spec-equiv-congruence-on-tyspec (implies (type-spec-equiv tyspec tyspec-equiv) (equal (valid-type-spec tyspec type? tyspecs table ienv) (valid-type-spec tyspec-equiv type? tyspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-type-spec-type-option-equiv-congruence-on-type? (implies (type-option-equiv type? type?-equiv) (equal (valid-type-spec tyspec type? tyspecs table ienv) (valid-type-spec tyspec type?-equiv tyspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-type-spec-type-spec-list-equiv-congruence-on-tyspecs (implies (type-spec-list-equiv tyspecs tyspecs-equiv) (equal (valid-type-spec tyspec type? tyspecs table ienv) (valid-type-spec tyspec type? tyspecs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-type-spec-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-type-spec tyspec type? tyspecs table ienv) (valid-type-spec tyspec type? tyspecs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-type-spec-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-type-spec tyspec type? tyspecs table ienv) (valid-type-spec tyspec type? tyspecs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-spec/qual-equiv-congruence-on-specqual (implies (spec/qual-equiv specqual specqual-equiv) (equal (valid-spec/qual specqual type? tyspecs table ienv) (valid-spec/qual specqual-equiv type? tyspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-type-option-equiv-congruence-on-type? (implies (type-option-equiv type? type?-equiv) (equal (valid-spec/qual specqual type? tyspecs table ienv) (valid-spec/qual specqual type?-equiv tyspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-type-spec-list-equiv-congruence-on-tyspecs (implies (type-spec-list-equiv tyspecs tyspecs-equiv) (equal (valid-spec/qual specqual type? tyspecs table ienv) (valid-spec/qual specqual type? tyspecs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-spec/qual specqual type? tyspecs table ienv) (valid-spec/qual specqual type? tyspecs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-spec/qual specqual type? tyspecs table ienv) (valid-spec/qual specqual type? tyspecs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-list-spec/qual-list-equiv-congruence-on-specquals (implies (spec/qual-list-equiv specquals specquals-equiv) (equal (valid-spec/qual-list specquals type? tyspecs table ienv) (valid-spec/qual-list specquals-equiv type? tyspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-list-type-option-equiv-congruence-on-type? (implies (type-option-equiv type? type?-equiv) (equal (valid-spec/qual-list specquals type? tyspecs table ienv) (valid-spec/qual-list specquals type?-equiv tyspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-list-type-spec-list-equiv-congruence-on-tyspecs (implies (type-spec-list-equiv tyspecs tyspecs-equiv) (equal (valid-spec/qual-list specquals type? tyspecs table ienv) (valid-spec/qual-list specquals type? tyspecs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-spec/qual-list specquals type? tyspecs table ienv) (valid-spec/qual-list specquals type? tyspecs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-spec/qual-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-spec/qual-list specquals type? tyspecs table ienv) (valid-spec/qual-list specquals type? tyspecs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-align-spec-align-spec-equiv-congruence-on-align (implies (align-spec-equiv align align-equiv) (equal (valid-align-spec align table ienv) (valid-align-spec align-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-align-spec-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-align-spec align table ienv) (valid-align-spec align table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-align-spec-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-align-spec align table ienv) (valid-align-spec align table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-decl-spec-equiv-congruence-on-declspec (implies (decl-spec-equiv declspec declspec-equiv) (equal (valid-decl-spec declspec type? tyspecs storspecs table ienv) (valid-decl-spec declspec-equiv type? tyspecs storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-type-option-equiv-congruence-on-type? (implies (type-option-equiv type? type?-equiv) (equal (valid-decl-spec declspec type? tyspecs storspecs table ienv) (valid-decl-spec declspec type?-equiv tyspecs storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-type-spec-list-equiv-congruence-on-tyspecs (implies (type-spec-list-equiv tyspecs tyspecs-equiv) (equal (valid-decl-spec declspec type? tyspecs storspecs table ienv) (valid-decl-spec declspec type? tyspecs-equiv storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-stor-spec-list-equiv-congruence-on-storspecs (implies (stor-spec-list-equiv storspecs storspecs-equiv) (equal (valid-decl-spec declspec type? tyspecs storspecs table ienv) (valid-decl-spec declspec type? tyspecs storspecs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-decl-spec declspec type? tyspecs storspecs table ienv) (valid-decl-spec declspec type? tyspecs storspecs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-decl-spec declspec type? tyspecs storspecs table ienv) (valid-decl-spec declspec type? tyspecs storspecs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-list-decl-spec-list-equiv-congruence-on-declspecs (implies (decl-spec-list-equiv declspecs declspecs-equiv) (equal (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv) (valid-decl-spec-list declspecs-equiv type? tyspecs storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-list-type-option-equiv-congruence-on-type? (implies (type-option-equiv type? type?-equiv) (equal (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv) (valid-decl-spec-list declspecs type?-equiv tyspecs storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-list-type-spec-list-equiv-congruence-on-tyspecs (implies (type-spec-list-equiv tyspecs tyspecs-equiv) (equal (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv) (valid-decl-spec-list declspecs type? tyspecs-equiv storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-list-stor-spec-list-equiv-congruence-on-storspecs (implies (stor-spec-list-equiv storspecs storspecs-equiv) (equal (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv) (valid-decl-spec-list declspecs type? tyspecs storspecs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv) (valid-decl-spec-list declspecs type? tyspecs storspecs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-decl-spec-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-initer-equiv-congruence-on-initer (implies (initer-equiv initer initer-equiv) (equal (valid-initer initer target-type lifetime table ienv) (valid-initer initer-equiv target-type lifetime table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-type-equiv-congruence-on-target-type (implies (type-equiv target-type target-type-equiv) (equal (valid-initer initer target-type lifetime table ienv) (valid-initer initer target-type-equiv lifetime table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-lifetime-equiv-congruence-on-lifetime (implies (lifetime-equiv lifetime lifetime-equiv) (equal (valid-initer initer target-type lifetime table ienv) (valid-initer initer target-type lifetime-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-initer initer target-type lifetime table ienv) (valid-initer initer target-type lifetime table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-initer initer target-type lifetime table ienv) (valid-initer initer target-type lifetime table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-option-initer-option-equiv-congruence-on-initer? (implies (initer-option-equiv initer? initer?-equiv) (equal (valid-initer-option initer? target-type lifetime? table ienv) (valid-initer-option initer?-equiv target-type lifetime? table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-option-type-equiv-congruence-on-target-type (implies (type-equiv target-type target-type-equiv) (equal (valid-initer-option initer? target-type lifetime? table ienv) (valid-initer-option initer? target-type-equiv lifetime? table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-option-lifetime-option-equiv-congruence-on-lifetime? (implies (lifetime-option-equiv lifetime? lifetime?-equiv) (equal (valid-initer-option initer? target-type lifetime? table ienv) (valid-initer-option initer? target-type lifetime?-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-option-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-initer-option initer? target-type lifetime? table ienv) (valid-initer-option initer? target-type lifetime? table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-initer-option-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-initer-option initer? target-type lifetime? table ienv) (valid-initer-option initer? target-type lifetime? table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-desiniter-equiv-congruence-on-desiniter (implies (desiniter-equiv desiniter desiniter-equiv) (equal (valid-desiniter desiniter target-type lifetime table ienv) (valid-desiniter desiniter-equiv target-type lifetime table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-type-equiv-congruence-on-target-type (implies (type-equiv target-type target-type-equiv) (equal (valid-desiniter desiniter target-type lifetime table ienv) (valid-desiniter desiniter target-type-equiv lifetime table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-lifetime-equiv-congruence-on-lifetime (implies (lifetime-equiv lifetime lifetime-equiv) (equal (valid-desiniter desiniter target-type lifetime table ienv) (valid-desiniter desiniter target-type lifetime-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-desiniter desiniter target-type lifetime table ienv) (valid-desiniter desiniter target-type lifetime table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-desiniter desiniter target-type lifetime table ienv) (valid-desiniter desiniter target-type lifetime table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-list-desiniter-list-equiv-congruence-on-desiniters (implies (desiniter-list-equiv desiniters desiniters-equiv) (equal (valid-desiniter-list desiniters target-type lifetime table ienv) (valid-desiniter-list desiniters-equiv target-type lifetime table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-list-type-equiv-congruence-on-target-type (implies (type-equiv target-type target-type-equiv) (equal (valid-desiniter-list desiniters target-type lifetime table ienv) (valid-desiniter-list desiniters target-type-equiv lifetime table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-list-lifetime-equiv-congruence-on-lifetime (implies (lifetime-equiv lifetime lifetime-equiv) (equal (valid-desiniter-list desiniters target-type lifetime table ienv) (valid-desiniter-list desiniters target-type lifetime-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-desiniter-list desiniters target-type lifetime table ienv) (valid-desiniter-list desiniters target-type lifetime table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-desiniter-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-desiniter-list desiniters target-type lifetime table ienv) (valid-desiniter-list desiniters target-type lifetime table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-designor-designor-equiv-congruence-on-designor (implies (designor-equiv designor designor-equiv) (equal (valid-designor designor target-type table ienv) (valid-designor designor-equiv target-type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-designor-type-equiv-congruence-on-target-type (implies (type-equiv target-type target-type-equiv) (equal (valid-designor designor target-type table ienv) (valid-designor designor target-type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-designor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-designor designor target-type table ienv) (valid-designor designor target-type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-designor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-designor designor target-type table ienv) (valid-designor designor target-type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-designor-list-designor-list-equiv-congruence-on-designors (implies (designor-list-equiv designors designors-equiv) (equal (valid-designor-list designors target-type table ienv) (valid-designor-list designors-equiv target-type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-designor-list-type-equiv-congruence-on-target-type (implies (type-equiv target-type target-type-equiv) (equal (valid-designor-list designors target-type table ienv) (valid-designor-list designors target-type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-designor-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-designor-list designors target-type table ienv) (valid-designor-list designors target-type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-designor-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-designor-list designors target-type table ienv) (valid-designor-list designors target-type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-declor-equiv-congruence-on-declor (implies (declor-equiv declor declor-equiv) (equal (valid-declor declor fundef-params-p type table ienv) (valid-declor declor-equiv fundef-params-p type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-iff-congruence-on-fundef-params-p (implies (iff fundef-params-p fundef-params-p-equiv) (equal (valid-declor declor fundef-params-p type table ienv) (valid-declor declor fundef-params-p-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-declor declor fundef-params-p type table ienv) (valid-declor declor fundef-params-p type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-declor declor fundef-params-p type table ienv) (valid-declor declor fundef-params-p type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-declor declor fundef-params-p type table ienv) (valid-declor declor fundef-params-p type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-option-declor-option-equiv-congruence-on-declor? (implies (declor-option-equiv declor? declor?-equiv) (equal (valid-declor-option declor? type table ienv) (valid-declor-option declor?-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-option-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-declor-option declor? type table ienv) (valid-declor-option declor? type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-option-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-declor-option declor? type table ienv) (valid-declor-option declor? type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declor-option-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-declor-option declor? type table ienv) (valid-declor-option declor? type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor (implies (dirdeclor-equiv dirdeclor dirdeclor-equiv) (equal (valid-dirdeclor dirdeclor fundef-params-p type table ienv) (valid-dirdeclor dirdeclor-equiv fundef-params-p type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirdeclor-iff-congruence-on-fundef-params-p (implies (iff fundef-params-p fundef-params-p-equiv) (equal (valid-dirdeclor dirdeclor fundef-params-p type table ienv) (valid-dirdeclor dirdeclor fundef-params-p-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirdeclor-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-dirdeclor dirdeclor fundef-params-p type table ienv) (valid-dirdeclor dirdeclor fundef-params-p type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirdeclor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-dirdeclor dirdeclor fundef-params-p type table ienv) (valid-dirdeclor dirdeclor fundef-params-p type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirdeclor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-dirdeclor dirdeclor fundef-params-p type table ienv) (valid-dirdeclor dirdeclor fundef-params-p type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-absdeclor-absdeclor-equiv-congruence-on-absdeclor (implies (absdeclor-equiv absdeclor absdeclor-equiv) (equal (valid-absdeclor absdeclor type table ienv) (valid-absdeclor absdeclor-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-absdeclor-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-absdeclor absdeclor type table ienv) (valid-absdeclor absdeclor type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-absdeclor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-absdeclor absdeclor type table ienv) (valid-absdeclor absdeclor type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-absdeclor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-absdeclor absdeclor type table ienv) (valid-absdeclor absdeclor type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-absdeclor-option-absdeclor-option-equiv-congruence-on-absdeclor? (implies (absdeclor-option-equiv absdeclor? absdeclor?-equiv) (equal (valid-absdeclor-option absdeclor? type table ienv) (valid-absdeclor-option absdeclor?-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-absdeclor-option-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-absdeclor-option absdeclor? type table ienv) (valid-absdeclor-option absdeclor? type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-absdeclor-option-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-absdeclor-option absdeclor? type table ienv) (valid-absdeclor-option absdeclor? type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-absdeclor-option-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-absdeclor-option absdeclor? type table ienv) (valid-absdeclor-option absdeclor? type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor (implies (dirabsdeclor-equiv dirabsdeclor dirabsdeclor-equiv) (equal (valid-dirabsdeclor dirabsdeclor type table ienv) (valid-dirabsdeclor dirabsdeclor-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirabsdeclor-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-dirabsdeclor dirabsdeclor type table ienv) (valid-dirabsdeclor dirabsdeclor type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirabsdeclor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-dirabsdeclor dirabsdeclor type table ienv) (valid-dirabsdeclor dirabsdeclor type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirabsdeclor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-dirabsdeclor dirabsdeclor type table ienv) (valid-dirabsdeclor dirabsdeclor type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirabsdeclor-option-dirabsdeclor-option-equiv-congruence-on-dirabsdeclor? (implies (dirabsdeclor-option-equiv dirabsdeclor? dirabsdeclor?-equiv) (equal (valid-dirabsdeclor-option dirabsdeclor? type table ienv) (valid-dirabsdeclor-option dirabsdeclor?-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirabsdeclor-option-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-dirabsdeclor-option dirabsdeclor? type table ienv) (valid-dirabsdeclor-option dirabsdeclor? type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirabsdeclor-option-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-dirabsdeclor-option dirabsdeclor? type table ienv) (valid-dirabsdeclor-option dirabsdeclor? type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-dirabsdeclor-option-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-dirabsdeclor-option dirabsdeclor? type table ienv) (valid-dirabsdeclor-option dirabsdeclor? type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declon-param-declon-equiv-congruence-on-paramdecl (implies (param-declon-equiv paramdecl paramdecl-equiv) (equal (valid-param-declon paramdecl fundef-params-p table ienv) (valid-param-declon paramdecl-equiv fundef-params-p table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declon-iff-congruence-on-fundef-params-p (implies (iff fundef-params-p fundef-params-p-equiv) (equal (valid-param-declon paramdecl fundef-params-p table ienv) (valid-param-declon paramdecl fundef-params-p-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declon-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-param-declon paramdecl fundef-params-p table ienv) (valid-param-declon paramdecl fundef-params-p table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declon-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-param-declon paramdecl fundef-params-p table ienv) (valid-param-declon paramdecl fundef-params-p table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declon-list-param-declon-list-equiv-congruence-on-paramdecls (implies (param-declon-list-equiv paramdecls paramdecls-equiv) (equal (valid-param-declon-list paramdecls fundef-params-p table ienv) (valid-param-declon-list paramdecls-equiv fundef-params-p table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declon-list-iff-congruence-on-fundef-params-p (implies (iff fundef-params-p fundef-params-p-equiv) (equal (valid-param-declon-list paramdecls fundef-params-p table ienv) (valid-param-declon-list paramdecls fundef-params-p-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declon-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-param-declon-list paramdecls fundef-params-p table ienv) (valid-param-declon-list paramdecls fundef-params-p table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declon-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-param-declon-list paramdecls fundef-params-p table ienv) (valid-param-declon-list paramdecls fundef-params-p table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declor-param-declor-equiv-congruence-on-paramdeclor (implies (param-declor-equiv paramdeclor paramdeclor-equiv) (equal (valid-param-declor paramdeclor type table ienv) (valid-param-declor paramdeclor-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declor-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-param-declor paramdeclor type table ienv) (valid-param-declor paramdeclor type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-param-declor paramdeclor type table ienv) (valid-param-declor paramdeclor type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-param-declor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-param-declor paramdeclor type table ienv) (valid-param-declor paramdeclor type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-tyname-tyname-equiv-congruence-on-tyname (implies (tyname-equiv tyname tyname-equiv) (equal (valid-tyname tyname table ienv) (valid-tyname tyname-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-tyname-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-tyname tyname table ienv) (valid-tyname tyname table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-tyname-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-tyname tyname table ienv) (valid-tyname tyname table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-struni-spec-struni-spec-equiv-congruence-on-struni-spec (implies (struni-spec-equiv struni-spec struni-spec-equiv) (equal (valid-struni-spec struni-spec table ienv) (valid-struni-spec struni-spec-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struni-spec-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-struni-spec struni-spec table ienv) (valid-struni-spec struni-spec table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struni-spec-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-struni-spec struni-spec table ienv) (valid-struni-spec struni-spec table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declon-struct-declon-equiv-congruence-on-structdeclon (implies (struct-declon-equiv structdeclon structdeclon-equiv) (equal (valid-struct-declon structdeclon previous table ienv) (valid-struct-declon structdeclon-equiv previous table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declon-ident-list-equiv-congruence-on-previous (implies (ident-list-equiv previous previous-equiv) (equal (valid-struct-declon structdeclon previous table ienv) (valid-struct-declon structdeclon previous-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declon-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-struct-declon structdeclon previous table ienv) (valid-struct-declon structdeclon previous table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declon-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-struct-declon structdeclon previous table ienv) (valid-struct-declon structdeclon previous table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declon-list-struct-declon-list-equiv-congruence-on-structdeclons (implies (struct-declon-list-equiv structdeclons structdeclons-equiv) (equal (valid-struct-declon-list structdeclons previous table ienv) (valid-struct-declon-list structdeclons-equiv previous table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declon-list-ident-list-equiv-congruence-on-previous (implies (ident-list-equiv previous previous-equiv) (equal (valid-struct-declon-list structdeclons previous table ienv) (valid-struct-declon-list structdeclons previous-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declon-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-struct-declon-list structdeclons previous table ienv) (valid-struct-declon-list structdeclons previous table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declon-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-struct-declon-list structdeclons previous table ienv) (valid-struct-declon-list structdeclons previous table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-struct-declor-equiv-congruence-on-structdeclor (implies (struct-declor-equiv structdeclor structdeclor-equiv) (equal (valid-struct-declor structdeclor previous type table ienv) (valid-struct-declor structdeclor-equiv previous type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-ident-list-equiv-congruence-on-previous (implies (ident-list-equiv previous previous-equiv) (equal (valid-struct-declor structdeclor previous type table ienv) (valid-struct-declor structdeclor previous-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-struct-declor structdeclor previous type table ienv) (valid-struct-declor structdeclor previous type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-struct-declor structdeclor previous type table ienv) (valid-struct-declor structdeclor previous type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-struct-declor structdeclor previous type table ienv) (valid-struct-declor structdeclor previous type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-list-struct-declor-list-equiv-congruence-on-structdeclors (implies (struct-declor-list-equiv structdeclors structdeclors-equiv) (equal (valid-struct-declor-list structdeclors previous type table ienv) (valid-struct-declor-list structdeclors-equiv previous type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-list-ident-list-equiv-congruence-on-previous (implies (ident-list-equiv previous previous-equiv) (equal (valid-struct-declor-list structdeclors previous type table ienv) (valid-struct-declor-list structdeclors previous-equiv type table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-list-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-struct-declor-list structdeclors previous type table ienv) (valid-struct-declor-list structdeclors previous type-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-struct-declor-list structdeclors previous type table ienv) (valid-struct-declor-list structdeclors previous type table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-struct-declor-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-struct-declor-list structdeclors previous type table ienv) (valid-struct-declor-list structdeclors previous type table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-enum-spec-enum-spec-equiv-congruence-on-enumspec (implies (enum-spec-equiv enumspec enumspec-equiv) (equal (valid-enum-spec enumspec table ienv) (valid-enum-spec enumspec-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-enum-spec-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-enum-spec enumspec table ienv) (valid-enum-spec enumspec table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-enum-spec-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-enum-spec enumspec table ienv) (valid-enum-spec enumspec table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-enumer-enumer-equiv-congruence-on-enumer (implies (enumer-equiv enumer enumer-equiv) (equal (valid-enumer enumer table ienv) (valid-enumer enumer-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-enumer-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-enumer enumer table ienv) (valid-enumer enumer table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-enumer-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-enumer enumer table ienv) (valid-enumer enumer table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-enumer-list-enumer-list-equiv-congruence-on-enumers (implies (enumer-list-equiv enumers enumers-equiv) (equal (valid-enumer-list enumers table ienv) (valid-enumer-list enumers-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-enumer-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-enumer-list enumers table ienv) (valid-enumer-list enumers table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-enumer-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-enumer-list enumers table ienv) (valid-enumer-list enumers table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-statassert-statassert-equiv-congruence-on-statassert (implies (statassert-equiv statassert statassert-equiv) (equal (valid-statassert statassert table ienv) (valid-statassert statassert-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-statassert-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-statassert statassert table ienv) (valid-statassert statassert table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-statassert-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-statassert statassert table ienv) (valid-statassert statassert table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-init-declor-equiv-congruence-on-initdeclor (implies (init-declor-equiv initdeclor initdeclor-equiv) (equal (valid-init-declor initdeclor type storspecs table ienv) (valid-init-declor initdeclor-equiv type storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-init-declor initdeclor type storspecs table ienv) (valid-init-declor initdeclor type-equiv storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-stor-spec-list-equiv-congruence-on-storspecs (implies (stor-spec-list-equiv storspecs storspecs-equiv) (equal (valid-init-declor initdeclor type storspecs table ienv) (valid-init-declor initdeclor type storspecs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-init-declor initdeclor type storspecs table ienv) (valid-init-declor initdeclor type storspecs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-init-declor initdeclor type storspecs table ienv) (valid-init-declor initdeclor type storspecs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-list-init-declor-list-equiv-congruence-on-initdeclors (implies (init-declor-list-equiv initdeclors initdeclors-equiv) (equal (valid-init-declor-list initdeclors type storspecs table ienv) (valid-init-declor-list initdeclors-equiv type storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-list-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (valid-init-declor-list initdeclors type storspecs table ienv) (valid-init-declor-list initdeclors type-equiv storspecs table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-list-stor-spec-list-equiv-congruence-on-storspecs (implies (stor-spec-list-equiv storspecs storspecs-equiv) (equal (valid-init-declor-list initdeclors type storspecs table ienv) (valid-init-declor-list initdeclors type storspecs-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-init-declor-list initdeclors type storspecs table ienv) (valid-init-declor-list initdeclors type storspecs table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-init-declor-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-init-declor-list initdeclors type storspecs table ienv) (valid-init-declor-list initdeclors type storspecs table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-declon-declon-equiv-congruence-on-declon (implies (declon-equiv declon declon-equiv) (equal (valid-declon declon table ienv) (valid-declon declon-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declon-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-declon declon table ienv) (valid-declon declon table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declon-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-declon declon table ienv) (valid-declon declon table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-declon-list-declon-list-equiv-congruence-on-declons (implies (declon-list-equiv declons declons-equiv) (equal (valid-declon-list declons table ienv) (valid-declon-list declons-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declon-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-declon-list declons table ienv) (valid-declon-list declons table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-declon-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-declon-list declons table ienv) (valid-declon-list declons table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-label-label-equiv-congruence-on-label (implies (label-equiv label label-equiv) (equal (valid-label label table ienv) (valid-label label-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-label-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-label label table ienv) (valid-label label table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-label-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-label label table ienv) (valid-label label table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-stmt-stmt-equiv-congruence-on-stmt (implies (stmt-equiv stmt stmt-equiv) (equal (valid-stmt stmt table ienv) (valid-stmt stmt-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-stmt-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-stmt stmt table ienv) (valid-stmt stmt table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-stmt-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-stmt stmt table ienv) (valid-stmt stmt table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-comp-stmt-comp-stmt-equiv-congruence-on-cstmt (implies (comp-stmt-equiv cstmt cstmt-equiv) (equal (valid-comp-stmt cstmt fundefp table ienv) (valid-comp-stmt cstmt-equiv fundefp table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-comp-stmt-iff-congruence-on-fundefp (implies (iff fundefp fundefp-equiv) (equal (valid-comp-stmt cstmt fundefp table ienv) (valid-comp-stmt cstmt fundefp-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-comp-stmt-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-comp-stmt cstmt fundefp table ienv) (valid-comp-stmt cstmt fundefp table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-comp-stmt-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-comp-stmt cstmt fundefp table ienv) (valid-comp-stmt cstmt fundefp table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-block-item-block-item-equiv-congruence-on-item (implies (block-item-equiv item item-equiv) (equal (valid-block-item item table ienv) (valid-block-item item-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-block-item-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-block-item item table ienv) (valid-block-item item table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-block-item-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-block-item item table ienv) (valid-block-item item table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm valid-block-item-list-block-item-list-equiv-congruence-on-items (implies (block-item-list-equiv items items-equiv) (equal (valid-block-item-list items table ienv) (valid-block-item-list items-equiv table ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-block-item-list-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-block-item-list items table ienv) (valid-block-item-list items table-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-block-item-list-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-block-item-list items table ienv) (valid-block-item-list items table ienv-equiv))) :rule-classes :congruence)
Theorem:
(defthm expr-unambp-of-valid-expr (implies (expr-unambp expr) (b* (((mv acl2::?erp ?new-expr ?type ?return-types ?new-table) (valid-expr expr table ienv))) (implies (not erp) (expr-unambp new-expr)))))
Theorem:
(defthm expr-list-unambp-of-valid-expr-list (implies (expr-list-unambp exprs) (b* (((mv acl2::?erp ?new-exprs ?types ?return-types ?new-table) (valid-expr-list exprs table ienv))) (implies (not erp) (expr-list-unambp new-exprs)))))
Theorem:
(defthm expr-option-unambp-of-valid-expr-option (implies (expr-option-unambp expr?) (b* (((mv acl2::?erp ?new-expr? ?type? ?return-types ?new-table) (valid-expr-option expr? table ienv))) (implies (not erp) (expr-option-unambp new-expr?)))))
Theorem:
(defthm const-expr-unambp-of-valid-const-expr (implies (const-expr-unambp cexpr) (b* (((mv acl2::?erp ?new-cexpr ?type ?return-types ?new-table) (valid-const-expr cexpr table ienv))) (implies (not erp) (const-expr-unambp new-cexpr)))))
Theorem:
(defthm const-expr-option-unambp-of-valid-const-expr-option (implies (const-expr-option-unambp cexpr?) (b* (((mv acl2::?erp ?new-cexpr? ?type? ?return-types ?new-table) (valid-const-expr-option cexpr? table ienv))) (implies (not erp) (const-expr-option-unambp new-cexpr?)))))
Theorem:
(defthm genassoc-unambp-of-valid-genassoc (implies (genassoc-unambp genassoc) (b* (((mv acl2::?erp ?new-genassoc ?tyname-type ?expr-type ?return-types ?new-table) (valid-genassoc genassoc table ienv))) (implies (not erp) (genassoc-unambp new-genassoc)))))
Theorem:
(defthm genassoc-list-unambp-of-valid-genassoc-list (implies (genassoc-list-unambp genassocs) (b* (((mv acl2::?erp ?new-genassocs ?type-alist ?return-types ?new-table) (valid-genassoc-list genassocs table ienv))) (implies (not erp) (genassoc-list-unambp new-genassocs)))))
Theorem:
(defthm member-designor-unambp-of-valid-member-designor (implies (member-designor-unambp memdesign) (b* (((mv acl2::?erp ?new-memdesign ?return-types ?new-table) (valid-member-designor memdesign table ienv))) (implies (not erp) (member-designor-unambp new-memdesign)))))
Theorem:
(defthm type-spec-unambp-of-valid-type-spec (implies (and (type-spec-unambp tyspec) (type-spec-list-unambp tyspecs)) (b* (((mv acl2::?erp ?new-tyspec ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-type-spec tyspec type? tyspecs table ienv))) (implies (not erp) (and (type-spec-unambp new-tyspec) (type-spec-list-unambp new-tyspecs))))))
Theorem:
(defthm spec/qual-unambp-of-valid-spec/qual (implies (and (spec/qual-unambp specqual) (type-spec-list-unambp tyspecs)) (b* (((mv acl2::?erp ?new-specqual ?new-type? ?new-tyspecs ?return-types ?new-table) (valid-spec/qual specqual type? tyspecs table ienv))) (implies (not erp) (and (spec/qual-unambp new-specqual) (type-spec-list-unambp new-tyspecs))))))
Theorem:
(defthm spec/qual-list-unambp-of-valid-spec/qual-list (implies (and (spec/qual-list-unambp specquals) (type-spec-list-unambp tyspecs)) (b* (((mv acl2::?erp ?new-specquals ?type ?return-types ?new-table) (valid-spec/qual-list specquals type? tyspecs table ienv))) (implies (not erp) (spec/qual-list-unambp new-specquals)))))
Theorem:
(defthm align-spec-unambp-of-valid-align-spec (implies (align-spec-unambp align) (b* (((mv acl2::?erp ?new-align ?return-types ?new-table) (valid-align-spec align table ienv))) (implies (not erp) (align-spec-unambp new-align)))))
Theorem:
(defthm decl-spec-unambp-of-valid-decl-spec (implies (and (decl-spec-unambp declspec) (type-spec-list-unambp tyspecs)) (b* (((mv acl2::?erp ?new-declspec ?new-type? ?new-tyspecs ?new-storspecs ?return-types ?new-table) (valid-decl-spec declspec type? tyspecs storspecs table ienv))) (implies (not erp) (and (decl-spec-unambp new-declspec) (type-spec-list-unambp new-tyspecs))))))
Theorem:
(defthm decl-spec-list-unambp-of-valid-decl-spec-list (implies (and (decl-spec-list-unambp declspecs) (type-spec-list-unambp tyspecs)) (b* (((mv acl2::?erp ?new-declspecs ?type ?all-storspecs ?return-types ?new-table) (valid-decl-spec-list declspecs type? tyspecs storspecs table ienv))) (implies (not erp) (decl-spec-list-unambp new-declspecs)))))
Theorem:
(defthm initer-unambp-of-valid-initer (implies (initer-unambp initer) (b* (((mv acl2::?erp ?new-initer ?return-types ?new-table) (valid-initer initer target-type lifetime table ienv))) (implies (not erp) (initer-unambp new-initer)))))
Theorem:
(defthm initer-option-unambp-of-valid-initer-option (implies (initer-option-unambp initer?) (b* (((mv acl2::?erp ?new-initer? ?return-types ?new-table) (valid-initer-option initer? target-type lifetime? table ienv))) (implies (not erp) (initer-option-unambp new-initer?)))))
Theorem:
(defthm desiniter-unambp-of-valid-desiniter (implies (desiniter-unambp desiniter) (b* (((mv acl2::?erp ?new-desiniter ?return-types ?new-table) (valid-desiniter desiniter target-type lifetime table ienv))) (implies (not erp) (desiniter-unambp new-desiniter)))))
Theorem:
(defthm desiniter-list-unambp-of-valid-desiniter-list (implies (desiniter-list-unambp desiniters) (b* (((mv acl2::?erp ?new-desiniters ?return-types ?new-table) (valid-desiniter-list desiniters target-type lifetime table ienv))) (implies (not erp) (desiniter-list-unambp new-desiniters)))))
Theorem:
(defthm designor-unambp-of-valid-designor (implies (designor-unambp designor) (b* (((mv acl2::?erp ?new-designor ?new-target-type ?return-types ?new-table) (valid-designor designor target-type table ienv))) (implies (not erp) (designor-unambp new-designor)))))
Theorem:
(defthm designor-list-unambp-of-valid-designor-list (implies (designor-list-unambp designors) (b* (((mv acl2::?erp ?new-designors ?new-target-type ?return-types ?new-table) (valid-designor-list designors target-type table ienv))) (implies (not erp) (designor-list-unambp new-designors)))))
Theorem:
(defthm declor-unambp-of-valid-declor (implies (declor-unambp declor) (b* (((mv acl2::?erp ?new-declor ?new-type ?ident ?return-types ?new-table) (valid-declor declor fundef-params-p type table ienv))) (implies (not erp) (declor-unambp new-declor)))))
Theorem:
(defthm declor-option-unambp-of-valid-declor-option (implies (declor-option-unambp declor?) (b* (((mv acl2::?erp ?new-declor? ?new-type ?ident? ?return-types ?new-table) (valid-declor-option declor? type table ienv))) (implies (not erp) (declor-option-unambp new-declor?)))))
Theorem:
(defthm dirdeclor-unambp-of-valid-dirdeclor (implies (dirdeclor-unambp dirdeclor) (b* (((mv acl2::?erp ?new-dirdeclor ?new-type ?ident ?return-types ?new-table) (valid-dirdeclor dirdeclor fundef-params-p type table ienv))) (implies (not erp) (dirdeclor-unambp new-dirdeclor)))))
Theorem:
(defthm absdeclor-unambp-of-valid-absdeclor (implies (absdeclor-unambp absdeclor) (b* (((mv acl2::?erp ?new-absdeclor ?new-type ?return-types ?new-table) (valid-absdeclor absdeclor type table ienv))) (implies (not erp) (absdeclor-unambp new-absdeclor)))))
Theorem:
(defthm absdeclor-option-unambp-of-valid-absdeclor-option (implies (absdeclor-option-unambp absdeclor?) (b* (((mv acl2::?erp ?new-absdeclor? ?new-type ?return-types ?new-table) (valid-absdeclor-option absdeclor? type table ienv))) (implies (not erp) (absdeclor-option-unambp new-absdeclor?)))))
Theorem:
(defthm dirabsdeclor-unambp-of-valid-dirabsdeclor (implies (dirabsdeclor-unambp dirabsdeclor) (b* (((mv acl2::?erp ?new-dirabsdeclor ?new-type ?return-types ?new-table) (valid-dirabsdeclor dirabsdeclor type table ienv))) (implies (not erp) (dirabsdeclor-unambp new-dirabsdeclor)))))
Theorem:
(defthm dirabsdeclor-option-unambp-of-valid-dirabsdeclor-option (implies (dirabsdeclor-option-unambp dirabsdeclor?) (b* (((mv acl2::?erp ?new-dirabsdeclor? ?new-type ?return-types ?new-table) (valid-dirabsdeclor-option dirabsdeclor? type table ienv))) (implies (not erp) (dirabsdeclor-option-unambp new-dirabsdeclor?)))))
Theorem:
(defthm param-declon-unambp-of-valid-param-declon (implies (param-declon-unambp paramdecl) (b* (((mv acl2::?erp ?new-paramdecl ?type ?return-types ?new-table) (valid-param-declon paramdecl fundef-params-p table ienv))) (implies (not erp) (param-declon-unambp new-paramdecl)))))
Theorem:
(defthm param-declon-list-unambp-of-valid-param-declon-list (implies (param-declon-list-unambp paramdecls) (b* (((mv acl2::?erp ?new-paramdecls ?types ?return-types ?new-table) (valid-param-declon-list paramdecls fundef-params-p table ienv))) (implies (not erp) (param-declon-list-unambp new-paramdecls)))))
Theorem:
(defthm param-declor-unambp-of-valid-param-declor (implies (param-declor-unambp paramdeclor) (b* (((mv acl2::?erp ?new-paramdeclor ?new-type ?ident? ?return-types ?uid? ?new-table) (valid-param-declor paramdeclor type table ienv))) (implies (not erp) (param-declor-unambp new-paramdeclor)))))
Theorem:
(defthm tyname-unambp-of-valid-tyname (implies (tyname-unambp tyname) (b* (((mv acl2::?erp ?new-tyname ?type ?return-types ?new-table) (valid-tyname tyname table ienv))) (implies (not erp) (tyname-unambp new-tyname)))))
Theorem:
(defthm struni-spec-unambp-of-valid-struni-spec (implies (struni-spec-unambp struni-spec) (b* (((mv acl2::?erp ?new-struni-spec ?return-types ?new-table) (valid-struni-spec struni-spec table ienv))) (implies (not erp) (struni-spec-unambp new-struni-spec)))))
Theorem:
(defthm struct-declon-unambp-of-valid-struct-declon (implies (struct-declon-unambp structdeclon) (b* (((mv acl2::?erp ?new-structdeclon ?new-previous ?return-types ?new-table) (valid-struct-declon structdeclon previous table ienv))) (implies (not erp) (struct-declon-unambp new-structdeclon)))))
Theorem:
(defthm struct-declon-list-unambp-of-valid-struct-declon-list (implies (struct-declon-list-unambp structdeclons) (b* (((mv acl2::?erp ?new-structdeclons ?return-types ?new-table) (valid-struct-declon-list structdeclons previous table ienv))) (implies (not erp) (struct-declon-list-unambp new-structdeclons)))))
Theorem:
(defthm struct-declor-unambp-of-valid-struct-declor (implies (struct-declor-unambp structdeclor) (b* (((mv acl2::?erp ?new-structdeclor ?new-previous ?return-types ?new-table) (valid-struct-declor structdeclor previous type table ienv))) (implies (not erp) (struct-declor-unambp new-structdeclor)))))
Theorem:
(defthm struct-declor-list-unambp-of-valid-struct-declor-list (implies (struct-declor-list-unambp structdeclors) (b* (((mv acl2::?erp ?new-structdeclors ?new-previous ?return-types ?new-table) (valid-struct-declor-list structdeclors previous type table ienv))) (implies (not erp) (struct-declor-list-unambp new-structdeclors)))))
Theorem:
(defthm enum-spec-unambp-of-valid-enum-spec (implies (enum-spec-unambp enumspec) (b* (((mv acl2::?erp ?new-enumspec ?return-types ?new-table) (valid-enum-spec enumspec table ienv))) (implies (not erp) (enum-spec-unambp new-enumspec)))))
Theorem:
(defthm enumer-unambp-of-valid-enumer (implies (enumer-unambp enumer) (b* (((mv acl2::?erp ?new-enumer ?return-types ?new-table) (valid-enumer enumer table ienv))) (implies (not erp) (enumer-unambp new-enumer)))))
Theorem:
(defthm enumer-list-unambp-of-valid-enumer-list (implies (enumer-list-unambp enumers) (b* (((mv acl2::?erp ?new-enumers ?return-types ?new-table) (valid-enumer-list enumers table ienv))) (implies (not erp) (enumer-list-unambp new-enumers)))))
Theorem:
(defthm statassert-unambp-of-valid-statassert (implies (statassert-unambp statassert) (b* (((mv acl2::?erp ?new-statassert ?return-types ?new-table) (valid-statassert statassert table ienv))) (implies (not erp) (statassert-unambp new-statassert)))))
Theorem:
(defthm init-declor-unambp-of-valid-init-declor (implies (init-declor-unambp initdeclor) (b* (((mv acl2::?erp ?new-initdeclor ?return-types ?new-table) (valid-init-declor initdeclor type storspecs table ienv))) (implies (not erp) (init-declor-unambp new-initdeclor)))))
Theorem:
(defthm init-declor-list-unambp-of-valid-init-declor-list (implies (init-declor-list-unambp initdeclors) (b* (((mv acl2::?erp ?new-initdeclors ?return-types ?new-table) (valid-init-declor-list initdeclors type storspecs table ienv))) (implies (not erp) (init-declor-list-unambp new-initdeclors)))))
Theorem:
(defthm declon-unambp-of-valid-declon (implies (declon-unambp declon) (b* (((mv acl2::?erp ?new-declon ?return-types ?new-table) (valid-declon declon table ienv))) (implies (not erp) (declon-unambp new-declon)))))
Theorem:
(defthm declon-list-unambp-of-valid-declon-list (implies (declon-list-unambp declons) (b* (((mv acl2::?erp ?new-declons ?return-types ?new-table) (valid-declon-list declons table ienv))) (implies (not erp) (declon-list-unambp new-declons)))))
Theorem:
(defthm label-unambp-of-valid-label (implies (label-unambp label) (b* (((mv acl2::?erp ?new-label ?return-types ?new-table) (valid-label label table ienv))) (implies (not erp) (label-unambp new-label)))))
Theorem:
(defthm stmt-unambp-of-valid-stmt (implies (stmt-unambp stmt) (b* (((mv acl2::?erp ?new-stmt ?return-types ?last-expr-type? ?new-table) (valid-stmt stmt table ienv))) (implies (not erp) (stmt-unambp new-stmt)))))
Theorem:
(defthm comp-stmt-unambp-of-valid-comp-stmt (implies (comp-stmt-unambp cstmt) (b* (((mv acl2::?erp ?new-cstmt ?return-types ?last-expr-type? ?new-table) (valid-comp-stmt cstmt fundefp table ienv))) (implies (not erp) (comp-stmt-unambp new-cstmt)))))
Theorem:
(defthm block-item-unambp-of-valid-block-item (implies (block-item-unambp item) (b* (((mv acl2::?erp ?new-item ?return-types ?last-expr-type? ?new-table) (valid-block-item item table ienv))) (implies (not erp) (block-item-unambp new-item)))))
Theorem:
(defthm block-item-list-unambp-of-valid-block-item-list (implies (block-item-list-unambp items) (b* (((mv acl2::?erp ?new-items ?return-types ?last-expr-type? ?new-table) (valid-block-item-list items table ienv))) (implies (not erp) (block-item-list-unambp new-items)))))