Print expressions, declarations, and related entities.
Since expressions and declarations are mutually recursive in our abstract syntax (as in the grammar), their printing functions are mutually recursive. Termination is easily proved, based on the sizes of the fixtypes.
Function:
(defun print-expr (expr expected-prio pstate) (declare (xargs :guard (and (exprp expr) (expr-priorityp expected-prio) (pristatep pstate)))) (declare (xargs :guard (expr-unambp expr))) (let ((__function__ 'print-expr)) (declare (ignorable __function__)) (b* ((actual-prio (expr->priority expr)) (parenp (not (expr-priority-<= expected-prio actual-prio))) (pstate (if parenp (print-astring "(" pstate) pstate)) (pstate (expr-case expr :ident (print-ident expr.unwrap pstate) :const (print-const expr.unwrap pstate) :string (print-stringlit expr.unwrap pstate) :paren (b* ((pstate (print-astring "(" pstate)) (pstate (print-expr expr.unwrap (expr-priority-expr) pstate)) (pstate (print-astring ")" pstate))) pstate) :gensel (b* ((pstate (print-astring "_Generic(" pstate)) (pstate (print-expr expr.control (expr-priority-asg) pstate)) (pstate (print-astring ", " pstate)) ((unless expr.assoc) (raise "Misusage error: ~ empty generic association list.") pstate) (pstate (print-genassoc-list expr.assoc pstate)) (pstate (print-astring ")" pstate))) pstate) :arrsub (b* ((pstate (print-expr expr.arg1 (expr-priority-postfix) pstate)) (pstate (print-astring "[" pstate)) (pstate (print-expr expr.arg2 (expr-priority-expr) pstate)) (pstate (print-astring "]" pstate))) pstate) :funcall (b* ((pstate (print-expr expr.fun (expr-priority-postfix) pstate)) (pstate (print-astring "(" pstate)) (pstate (if expr.args (print-expr-list expr.args pstate) pstate)) (pstate (print-astring ")" pstate))) pstate) :member (b* ((pstate (print-expr expr.arg (expr-priority-postfix) pstate)) (pstate (print-astring "." pstate)) (pstate (print-ident expr.name pstate))) pstate) :memberp (b* ((pstate (print-expr expr.arg (expr-priority-postfix) pstate)) (pstate (print-astring "->" pstate)) (pstate (print-ident expr.name pstate))) pstate) :complit (b* ((pstate (print-astring "(" pstate)) (pstate (print-tyname expr.type pstate)) (pstate (print-astring ") {" pstate)) ((unless expr.elems) (raise "Misusage error: ~ empty initializer list.") (pristate-fix pstate)) (pstate (print-desiniter-list expr.elems pstate)) (pstate (if expr.final-comma (print-astring ", }" pstate) (print-astring "}" pstate)))) pstate) :unary (if (or (unop-case expr.op :postinc) (unop-case expr.op :postdec)) (b* ((pstate (print-expr expr.arg (expr-priority-postfix) pstate)) (pstate (print-unop expr.op pstate))) pstate) (b* ((pstate (print-unop expr.op pstate)) (spacep (or (and (unop-case expr.op :sizeof) (not (expr-case expr.arg :paren))) (and (unop-case expr.op :plus) (expr-case expr.arg :unary) (unop-case (expr-unary->op expr.arg) :preinc)) (and (unop-case expr.op :minus) (expr-case expr.arg :unary) (unop-case (expr-unary->op expr.arg) :predec)))) (pstate (if spacep (print-astring " " pstate) pstate)) (arg-priority (if (or (unop-case expr.op :preinc) (unop-case expr.op :predec) (unop-case expr.op :sizeof)) (expr-priority-unary) (expr-priority-cast))) (pstate (print-expr expr.arg arg-priority pstate))) pstate)) :sizeof (b* ((pstate (print-astring "sizeof(" pstate)) (pstate (print-tyname expr.type pstate)) (pstate (print-astring ")" pstate))) pstate) :sizeof-ambig (prog2$ (impossible) (pristate-fix pstate)) :alignof (b* ((pstate (if expr.uscores (print-astring "__alignof__(" pstate) (print-astring "_Alignof(" pstate))) (pstate (print-tyname expr.type pstate)) (pstate (print-astring ")" pstate))) pstate) :cast (b* ((pstate (print-astring "(" pstate)) (pstate (print-tyname expr.type pstate)) (pstate (print-astring ") " pstate)) (pstate (print-expr expr.arg (expr-priority-cast) pstate))) pstate) :binary (b* (((mv expected-arg1-prio expected-arg2-prio) (binop-expected-priorities expr.op)) (pstate (print-expr expr.arg1 expected-arg1-prio pstate)) (pstate (print-astring " " pstate)) (pstate (print-binop expr.op pstate)) (pstate (print-astring " " pstate)) (pstate (print-expr expr.arg2 expected-arg2-prio pstate))) pstate) :cond (b* ((raise-prio (priopt->paren-nested-conds (pristate->options pstate))) (pstate (print-expr expr.test (expr-priority-logor) pstate)) (pstate (print-astring " ? " pstate)) (pstate (print-expr expr.then (if raise-prio (expr-priority-logor) (expr-priority-expr)) pstate)) (pstate (print-astring " : " pstate)) (pstate (print-expr expr.else (if raise-prio (expr-priority-logor) (expr-priority-cond)) pstate))) pstate) :comma (b* ((pstate (print-expr expr.first (expr-priority-expr) pstate)) (pstate (print-astring ", " pstate)) (pstate (print-expr expr.next (expr-priority-asg) pstate))) pstate) :cast/call-ambig (prog2$ (impossible) (pristate-fix pstate)) :cast/mul-ambig (prog2$ (impossible) (pristate-fix pstate)) :cast/add-ambig (prog2$ (impossible) (pristate-fix pstate)) :cast/sub-ambig (prog2$ (impossible) (pristate-fix pstate)) :cast/and-ambig (prog2$ (impossible) (pristate-fix pstate)))) (pstate (if parenp (print-astring ")" pstate) pstate))) pstate)))
Function:
(defun print-expr-list (exprs pstate) (declare (xargs :guard (and (expr-listp exprs) (pristatep pstate)))) (declare (xargs :guard (and (consp exprs) (expr-list-unambp exprs)))) (let ((__function__ 'print-expr-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp exprs))) (pristate-fix pstate)) (pstate (print-expr (car exprs) (expr-priority-asg) pstate)) ((when (endp (cdr exprs))) pstate) (pstate (print-astring ", " pstate))) (print-expr-list (cdr exprs) pstate))))
Function:
(defun print-const-expr (cexpr pstate) (declare (xargs :guard (and (const-exprp cexpr) (pristatep pstate)))) (declare (xargs :guard (const-expr-unambp cexpr))) (let ((__function__ 'print-const-expr)) (declare (ignorable __function__)) (print-expr (const-expr->unwrap cexpr) (expr-priority-cond) pstate)))
Function:
(defun print-genassoc (genassoc pstate) (declare (xargs :guard (and (genassocp genassoc) (pristatep pstate)))) (declare (xargs :guard (genassoc-unambp genassoc))) (let ((__function__ 'print-genassoc)) (declare (ignorable __function__)) (genassoc-case genassoc :type (b* ((pstate (print-tyname genassoc.type pstate)) (pstate (print-astring ": " pstate)) (pstate (print-expr genassoc.expr (expr-priority-asg) pstate))) pstate) :default (b* ((pstate (print-astring "default: " pstate)) (pstate (print-expr genassoc.expr (expr-priority-asg) pstate))) pstate))))
Function:
(defun print-genassoc-list (genassocs pstate) (declare (xargs :guard (and (genassoc-listp genassocs) (pristatep pstate)))) (declare (xargs :guard (and (consp genassocs) (genassoc-list-unambp genassocs)))) (let ((__function__ 'print-genassoc-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp genassocs))) (pristate-fix pstate)) (pstate (print-genassoc (car genassocs) pstate)) ((when (endp (cdr genassocs))) pstate) (pstate (print-astring ", " pstate))) (print-genassoc-list (cdr genassocs) pstate))))
Function:
(defun print-type-spec (tyspec pstate) (declare (xargs :guard (and (type-specp tyspec) (pristatep pstate)))) (declare (xargs :guard (type-spec-unambp tyspec))) (let ((__function__ 'print-type-spec)) (declare (ignorable __function__)) (type-spec-case tyspec :void (print-astring "void" pstate) :char (print-astring "char" pstate) :short (print-astring "short" pstate) :int (print-astring "int" pstate) :long (print-astring "long" pstate) :float (print-astring "float" pstate) :double (print-astring "double" pstate) :signed (print-astring "signed" pstate) :unsigned (print-astring "unsigned" pstate) :bool (print-astring "_Bool" pstate) :complex (print-astring "_Complex" pstate) :atomic (b* ((pstate (print-astring "_Atomic(" pstate)) (pstate (print-tyname tyspec.type pstate)) (pstate (print-astring ")" pstate))) pstate) :struct (b* ((pstate (print-astring "struct " pstate)) (pstate (print-strunispec tyspec.unwrap pstate))) pstate) :union (b* ((pstate (print-astring "union " pstate)) (pstate (print-strunispec tyspec.unwrap pstate))) pstate) :enum (b* ((pstate (print-astring "enum " pstate)) (pstate (print-enumspec tyspec.unwrap pstate))) pstate) :typedef (print-ident tyspec.name pstate))))
Function:
(defun print-spec/qual (specqual pstate) (declare (xargs :guard (and (spec/qual-p specqual) (pristatep pstate)))) (declare (xargs :guard (spec/qual-unambp specqual))) (let ((__function__ 'print-spec/qual)) (declare (ignorable __function__)) (spec/qual-case specqual :tyspec (print-type-spec specqual.unwrap pstate) :tyqual (print-type-qual specqual.unwrap pstate) :align (print-align-spec specqual.unwrap pstate))))
Function:
(defun print-spec/qual-list (specquals pstate) (declare (xargs :guard (and (spec/qual-listp specquals) (pristatep pstate)))) (declare (xargs :guard (and (consp specquals) (spec/qual-list-unambp specquals)))) (let ((__function__ 'print-spec/qual-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp specquals))) (pristate-fix pstate)) (pstate (print-spec/qual (car specquals) pstate)) ((when (endp (cdr specquals))) pstate) (pstate (print-astring " " pstate))) (print-spec/qual-list (cdr specquals) pstate))))
Function:
(defun print-align-spec (alignspec pstate) (declare (xargs :guard (and (align-specp alignspec) (pristatep pstate)))) (declare (xargs :guard (align-spec-unambp alignspec))) (let ((__function__ 'print-align-spec)) (declare (ignorable __function__)) (b* ((pstate (print-astring "_Alignas(" pstate)) (pstate (align-spec-case alignspec :alignas-type (print-tyname alignspec.type pstate) :alignas-expr (print-const-expr alignspec.arg pstate) :alignas-ambig (prog2$ (impossible) (pristate-fix pstate)))) (pstate (print-astring ")" pstate))) pstate)))
Function:
(defun print-declspec (declspec pstate) (declare (xargs :guard (and (declspecp declspec) (pristatep pstate)))) (declare (xargs :guard (declspec-unambp declspec))) (let ((__function__ 'print-declspec)) (declare (ignorable __function__)) (declspec-case declspec :stocla (print-stor-spec declspec.unwrap pstate) :tyspec (print-type-spec declspec.unwrap pstate) :tyqual (print-type-qual declspec.unwrap pstate) :funspec (print-fun-spec declspec.unwrap pstate) :align (print-align-spec declspec.unwrap pstate))))
Function:
(defun print-declspec-list (declspecs pstate) (declare (xargs :guard (and (declspec-listp declspecs) (pristatep pstate)))) (declare (xargs :guard (and (consp declspecs) (declspec-list-unambp declspecs)))) (let ((__function__ 'print-declspec-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp declspecs))) (pristate-fix pstate)) (pstate (print-declspec (car declspecs) pstate)) ((when (endp (cdr declspecs))) pstate) (pstate (print-astring " " pstate))) (print-declspec-list (cdr declspecs) pstate))))
Function:
(defun print-initer (initer pstate) (declare (xargs :guard (and (initerp initer) (pristatep pstate)))) (declare (xargs :guard (initer-unambp initer))) (let ((__function__ 'print-initer)) (declare (ignorable __function__)) (initer-case initer :single (print-expr initer.expr (expr-priority-asg) pstate) :list (b* ((pstate (print-astring "{" pstate)) ((unless initer.elems) (raise "Misusage error: ~ empty list of initializers.") pstate) (pstate (print-desiniter-list initer.elems pstate)) (pstate (if initer.final-comma (print-astring ", }" pstate) (print-astring "}" pstate)))) pstate))))
Function:
(defun print-desiniter (desiniter pstate) (declare (xargs :guard (and (desiniterp desiniter) (pristatep pstate)))) (declare (xargs :guard (desiniter-unambp desiniter))) (let ((__function__ 'print-desiniter)) (declare (ignorable __function__)) (b* (((desiniter desiniter) desiniter) (pstate (if desiniter.design (b* ((pstate (print-designor-list desiniter.design pstate)) (pstate (print-astring " = " pstate))) pstate) pstate)) (pstate (print-initer desiniter.init pstate))) pstate)))
Function:
(defun print-desiniter-list (desiniters pstate) (declare (xargs :guard (and (desiniter-listp desiniters) (pristatep pstate)))) (declare (xargs :guard (and (consp desiniters) (desiniter-list-unambp desiniters)))) (let ((__function__ 'print-desiniter-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp desiniters))) (pristate-fix pstate)) (pstate (print-desiniter (car desiniters) pstate)) ((when (endp (cdr desiniters))) pstate) (pstate (print-astring ", " pstate))) (print-desiniter-list (cdr desiniters) pstate))))
Function:
(defun print-designor (designor pstate) (declare (xargs :guard (and (designorp designor) (pristatep pstate)))) (declare (xargs :guard (designor-unambp designor))) (let ((__function__ 'print-designor)) (declare (ignorable __function__)) (designor-case designor :sub (b* ((pstate (print-astring "[" pstate)) (pstate (print-const-expr designor.index pstate)) (pstate (print-astring "]" pstate))) pstate) :dot (b* ((pstate (print-astring "." pstate)) (pstate (print-ident designor.name pstate))) pstate))))
Function:
(defun print-designor-list (designors pstate) (declare (xargs :guard (and (designor-listp designors) (pristatep pstate)))) (declare (xargs :guard (and (consp designors) (designor-list-unambp designors)))) (let ((__function__ 'print-designor-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp designors))) (pristate-fix pstate)) (pstate (print-designor (car designors) pstate)) ((when (endp (cdr designors))) pstate)) (print-designor-list (cdr designors) pstate))))
Function:
(defun print-declor (declor pstate) (declare (xargs :guard (and (declorp declor) (pristatep pstate)))) (declare (xargs :guard (declor-unambp declor))) (let ((__function__ 'print-declor)) (declare (ignorable __function__)) (b* (((declor declor) declor) (pstate (if (consp declor.pointers) (print-type-qual-list-list declor.pointers pstate) pstate)) (pstate (print-dirdeclor declor.decl pstate))) pstate)))
Function:
(defun print-dirdeclor (dirdeclor pstate) (declare (xargs :guard (and (dirdeclorp dirdeclor) (pristatep pstate)))) (declare (xargs :guard (dirdeclor-unambp dirdeclor))) (let ((__function__ 'print-dirdeclor)) (declare (ignorable __function__)) (dirdeclor-case dirdeclor :ident (print-ident dirdeclor.unwrap pstate) :paren (b* ((pstate (print-astring "(" pstate)) (pstate (print-declor dirdeclor.unwrap pstate)) (pstate (print-astring ")" pstate))) pstate) :array (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "[" pstate)) (pstate (if dirdeclor.tyquals (print-type-qual-list dirdeclor.tyquals pstate) pstate)) (pstate (if (and dirdeclor.tyquals dirdeclor.expr?) (print-astring " " pstate) pstate)) (pstate (if (expr-option-case dirdeclor.expr? :some) (print-expr (expr-option-some->val dirdeclor.expr?) (expr-priority-asg) pstate) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-static1 (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "static " pstate)) (pstate (if dirdeclor.tyquals (b* ((pstate (print-type-qual-list dirdeclor.tyquals pstate)) (pstate (print-astring " " pstate))) pstate) pstate)) (pstate (print-expr dirdeclor.expr (expr-priority-asg) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-static2 (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) ((unless dirdeclor.tyquals) (raise "Misusage error: ~ empty list of type qualifiers.") pstate) (pstate (print-type-qual-list dirdeclor.tyquals pstate)) (pstate (print-astring " static " pstate)) (pstate (print-expr dirdeclor.expr (expr-priority-asg) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-star (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "[" pstate)) (pstate (if dirdeclor.tyquals (b* ((pstate (print-type-qual-list dirdeclor.tyquals pstate)) (pstate (print-astring " " pstate))) pstate) pstate)) (pstate (print-astring "*]" pstate))) pstate) :function-params (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "(" pstate)) (pstate (if dirdeclor.params (print-paramdecl-list dirdeclor.params pstate) pstate)) (pstate (if dirdeclor.ellipsis (print-astring ", ...)" pstate) (print-astring ")" pstate)))) pstate) :function-names (b* ((pstate (print-dirdeclor dirdeclor.decl pstate)) (pstate (print-astring "(" pstate)) (pstate (if dirdeclor.names (print-ident-list dirdeclor.names pstate) pstate)) (pstate (print-astring ")" pstate))) pstate))))
Function:
(defun print-absdeclor (absdeclor pstate) (declare (xargs :guard (and (absdeclorp absdeclor) (pristatep pstate)))) (declare (xargs :guard (absdeclor-unambp absdeclor))) (let ((__function__ 'print-absdeclor)) (declare (ignorable __function__)) (b* (((absdeclor absdeclor) absdeclor) ((unless (or absdeclor.pointers absdeclor.decl?)) (raise "Misusage error: ~ empty abstract declarator.") (pristate-fix pstate)) (pstate (if absdeclor.pointers (print-type-qual-list-list absdeclor.pointers pstate) pstate)) (pstate (if (dirabsdeclor-option-case absdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val absdeclor.decl?) pstate) pstate))) pstate)))
Function:
(defun print-dirabsdeclor (dirabsdeclor pstate) (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor) (pristatep pstate)))) (declare (xargs :guard (dirabsdeclor-unambp dirabsdeclor))) (let ((__function__ 'print-dirabsdeclor)) (declare (ignorable __function__)) (dirabsdeclor-case dirabsdeclor :dummy-base (prog2$ (raise "Misusage error: ~ dummy base case of direct abstract declarator.") (pristate-fix pstate)) :paren (b* ((pstate (print-astring "(" pstate)) (pstate (print-absdeclor dirabsdeclor.unwrap pstate)) (pstate (print-astring ")" pstate))) pstate) :array (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) (pstate (print-astring "[" pstate)) (pstate (if dirabsdeclor.tyquals (print-type-qual-list dirabsdeclor.tyquals pstate) pstate)) (pstate (if (and dirabsdeclor.tyquals dirabsdeclor.expr?) (print-astring " " pstate) pstate)) (pstate (if (expr-option-case dirabsdeclor.expr? :some) (print-expr (expr-option-some->val dirabsdeclor.expr?) (expr-priority-asg) pstate) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-static1 (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) (pstate (print-astring "static " pstate)) (pstate (if dirabsdeclor.tyquals (b* ((pstate (print-type-qual-list dirabsdeclor.tyquals pstate)) (pstate (print-astring " " pstate))) pstate) pstate)) (pstate (print-expr dirabsdeclor.expr (expr-priority-asg) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-static2 (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) ((unless dirabsdeclor.tyquals) (raise "Misusage error: ~ empty list of type qualifiers.") (pristate-fix pstate)) (pstate (print-type-qual-list dirabsdeclor.tyquals pstate)) (pstate (print-astring " static " pstate)) (pstate (print-expr dirabsdeclor.expr (expr-priority-asg) pstate)) (pstate (print-astring "]" pstate))) pstate) :array-star (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) (pstate (print-astring "[*]" pstate))) pstate) :function (b* ((pstate (if (dirabsdeclor-option-case dirabsdeclor.decl? :some) (print-dirabsdeclor (dirabsdeclor-option-some->val dirabsdeclor.decl?) pstate) pstate)) (pstate (print-astring "(" pstate)) (pstate (if dirabsdeclor.params (b* ((pstate (print-paramdecl-list dirabsdeclor.params pstate)) (pstate (if dirabsdeclor.ellipsis (print-astring ", ..." pstate) pstate))) pstate) pstate)) (pstate (print-astring ")" pstate))) pstate))))
Function:
(defun print-paramdecl (paramdecl pstate) (declare (xargs :guard (and (paramdeclp paramdecl) (pristatep pstate)))) (declare (xargs :guard (paramdecl-unambp paramdecl))) (let ((__function__ 'print-paramdecl)) (declare (ignorable __function__)) (b* (((paramdecl paramdecl) paramdecl) ((unless paramdecl.spec) (raise "Misusage error: no declaration specifiers.") (pristate-fix pstate)) (pstate (print-declspec-list paramdecl.spec pstate)) (pstate (print-paramdeclor paramdecl.decl pstate))) pstate)))
Function:
(defun print-paramdecl-list (paramdecls pstate) (declare (xargs :guard (and (paramdecl-listp paramdecls) (pristatep pstate)))) (declare (xargs :guard (and (consp paramdecls) (paramdecl-list-unambp paramdecls)))) (let ((__function__ 'print-paramdecl-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp paramdecls))) (pristate-fix pstate)) (pstate (print-paramdecl (car paramdecls) pstate)) ((when (endp (cdr paramdecls))) pstate) (pstate (print-astring ", " pstate))) (print-paramdecl-list (cdr paramdecls) pstate))))
Function:
(defun print-paramdeclor (paramdeclor pstate) (declare (xargs :guard (and (paramdeclorp paramdeclor) (pristatep pstate)))) (declare (xargs :guard (paramdeclor-unambp paramdeclor))) (let ((__function__ 'print-paramdeclor)) (declare (ignorable __function__)) (paramdeclor-case paramdeclor :declor (b* ((pstate (print-astring " " pstate)) (pstate (print-declor paramdeclor.unwrap pstate))) pstate) :absdeclor (b* ((pstate (print-astring " " pstate)) (pstate (print-absdeclor paramdeclor.unwrap pstate))) pstate) :none (pristate-fix pstate) :ambig (prog2$ (impossible) (pristate-fix pstate)))))
Function:
(defun print-tyname (tyname pstate) (declare (xargs :guard (and (tynamep tyname) (pristatep pstate)))) (declare (xargs :guard (tyname-unambp tyname))) (let ((__function__ 'print-tyname)) (declare (ignorable __function__)) (b* (((tyname tyname) tyname) ((unless tyname.specqual) (raise "Misusage error: empty list of specifiers and qualifiers.") (pristate-fix pstate)) (pstate (print-spec/qual-list tyname.specqual pstate)) ((unless (absdeclor-option-case tyname.decl? :some)) pstate) (pstate (print-astring " " pstate)) (pstate (print-absdeclor (absdeclor-option-some->val tyname.decl?) pstate))) pstate)))
Function:
(defun print-strunispec (strunispec pstate) (declare (xargs :guard (and (strunispecp strunispec) (pristatep pstate)))) (declare (xargs :guard (strunispec-unambp strunispec))) (let ((__function__ 'print-strunispec)) (declare (ignorable __function__)) (b* (((strunispec strunispec) strunispec) ((unless (or (ident-option-case strunispec.name :some) strunispec.members)) (raise "Misusage error: empty structure or union specifier.") (pristate-fix pstate)) (pstate (ident-option-case strunispec.name :some (print-ident strunispec.name.val pstate) :none pstate)) (pstate (if (and strunispec.name strunispec.members) (print-astring " " pstate) pstate)) ((when (not strunispec.members)) pstate) (pstate (print-astring "{ " pstate)) (pstate (print-structdecl-list strunispec.members pstate)) (pstate (print-astring " }" pstate))) pstate)))
Function:
(defun print-structdecl (structdecl pstate) (declare (xargs :guard (and (structdeclp structdecl) (pristatep pstate)))) (declare (xargs :guard (structdecl-unambp structdecl))) (let ((__function__ 'print-structdecl)) (declare (ignorable __function__)) (structdecl-case structdecl :member (b* ((pstate (if structdecl.extension (print-astring "__extension__ " pstate) (pristate-fix pstate))) ((unless structdecl.specqual) (raise "Misusage error: empty specifier/qualifier list.") pstate) (pstate (print-spec/qual-list structdecl.specqual pstate)) (pstate (if structdecl.declor (b* ((pstate (print-astring " " pstate)) (pstate (print-structdeclor-list structdecl.declor pstate))) pstate) pstate)) (pstate (if structdecl.attrib (b* ((pstate (print-astring " " pstate)) (pstate (print-attrib-spec-list structdecl.attrib pstate))) pstate) pstate)) (pstate (print-astring ";" pstate))) pstate) :statassert (print-statassert structdecl.unwrap pstate))))
Function:
(defun print-structdecl-list (structdecls pstate) (declare (xargs :guard (and (structdecl-listp structdecls) (pristatep pstate)))) (declare (xargs :guard (and (consp structdecls) (structdecl-list-unambp structdecls)))) (let ((__function__ 'print-structdecl-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp structdecls))) (pristate-fix pstate)) (pstate (print-structdecl (car structdecls) pstate)) ((when (endp (cdr structdecls))) pstate) (pstate (print-astring " " pstate))) (print-structdecl-list (cdr structdecls) pstate))))
Function:
(defun print-structdeclor (structdeclor pstate) (declare (xargs :guard (and (structdeclorp structdeclor) (pristatep pstate)))) (declare (xargs :guard (structdeclor-unambp structdeclor))) (let ((__function__ 'print-structdeclor)) (declare (ignorable __function__)) (b* (((structdeclor structdeclor) structdeclor) ((unless (or (declor-option-case structdeclor.declor? :some) (const-expr-option-case structdeclor.expr? :some))) (raise "Misusage error: empty structure declarator.") (pristate-fix pstate)) (pstate (declor-option-case structdeclor.declor? :some (print-declor structdeclor.declor?.val pstate) :none pstate)) (pstate (if (and (declor-option-case structdeclor.declor? :some) (const-expr-option-case structdeclor.expr? :some)) (print-astring " " pstate) pstate)) (pstate (const-expr-option-case structdeclor.expr? :some (b* ((pstate (print-astring ": " pstate)) (pstate (print-const-expr structdeclor.expr?.val pstate))) pstate) :none pstate))) pstate)))
Function:
(defun print-structdeclor-list (structdeclors pstate) (declare (xargs :guard (and (structdeclor-listp structdeclors) (pristatep pstate)))) (declare (xargs :guard (and (consp structdeclors) (structdeclor-list-unambp structdeclors)))) (let ((__function__ 'print-structdeclor-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp structdeclors))) (pristate-fix pstate)) (pstate (print-structdeclor (car structdeclors) pstate)) ((when (endp (cdr structdeclors))) pstate) (pstate (print-astring ", " pstate))) (print-structdeclor-list (cdr structdeclors) pstate))))
Function:
(defun print-enumspec (enumspec pstate) (declare (xargs :guard (and (enumspecp enumspec) (pristatep pstate)))) (declare (xargs :guard (enumspec-unambp enumspec))) (let ((__function__ 'print-enumspec)) (declare (ignorable __function__)) (b* (((enumspec enumspec) enumspec) ((unless (or (ident-option-case enumspec.name :some) enumspec.list)) (raise "Misusage error: empty enumeration specifiers.") (pristate-fix pstate)) (pstate (ident-option-case enumspec.name :some (print-ident enumspec.name.val pstate) :none pstate)) (pstate (if (and (ident-option-case enumspec.name :some) enumspec.list) (print-astring " " pstate) pstate)) ((unless enumspec.list) pstate) (pstate (print-astring "{" pstate)) (pstate (print-enumer-list enumspec.list pstate)) (pstate (if enumspec.final-comma (print-astring ", }" pstate) (print-astring "}" pstate)))) pstate)))
Function:
(defun print-enumer (enumer pstate) (declare (xargs :guard (and (enumerp enumer) (pristatep pstate)))) (declare (xargs :guard (enumer-unambp enumer))) (let ((__function__ 'print-enumer)) (declare (ignorable __function__)) (b* (((enumer enumer) enumer) (pstate (print-ident enumer.name pstate)) ((unless (const-expr-option-case enumer.value :some)) pstate) (pstate (print-astring " = " pstate)) (pstate (print-const-expr (const-expr-option-some->val enumer.value) pstate))) pstate)))
Function:
(defun print-enumer-list (enumers pstate) (declare (xargs :guard (and (enumer-listp enumers) (pristatep pstate)))) (declare (xargs :guard (and (consp enumers) (enumer-list-unambp enumers)))) (let ((__function__ 'print-enumer-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp enumers))) (pristate-fix pstate)) (pstate (print-enumer (car enumers) pstate)) ((when (endp (cdr enumers))) pstate) (pstate (print-astring ", " pstate))) (print-enumer-list (cdr enumers) pstate))))
Function:
(defun print-statassert (statassert pstate) (declare (xargs :guard (and (statassertp statassert) (pristatep pstate)))) (declare (xargs :guard (statassert-unambp statassert))) (let ((__function__ 'print-statassert)) (declare (ignorable __function__)) (b* (((statassert statassert) statassert) (pstate (print-astring "_Static_assert(" pstate)) (pstate (print-const-expr statassert.test pstate)) (pstate (print-astring ", " pstate)) (pstate (print-stringlit statassert.message pstate)) (pstate (print-astring ");" pstate))) pstate)))
Function:
(defun print-attrib (attr pstate) (declare (xargs :guard (and (attribp attr) (pristatep pstate)))) (let ((__function__ 'print-attrib)) (declare (ignorable __function__)) (attrib-case attr :name (print-ident attr.name pstate) :name-param (b* ((pstate (print-ident attr.name pstate)) (pstate (print-astring "(" pstate)) ((unless (expr-list-unambp attr.param)) (raise "Internal error: unambiguous expressions in attribute ~x0." (attrib-fix attr)) pstate) (pstate (if attr.param (print-expr-list attr.param pstate) pstate)) (pstate (print-astring ")" pstate))) pstate))))
Function:
(defun print-attrib-list (attrs pstate) (declare (xargs :guard (and (attrib-listp attrs) (pristatep pstate)))) (declare (xargs :guard (consp attrs))) (let ((__function__ 'print-attrib-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp attrs))) (pristate-fix pstate)) (pstate (print-attrib (car attrs) pstate)) ((when (endp (cdr attrs))) pstate) (pstate (print-astring ", " pstate))) (print-attrib-list (cdr attrs) pstate))))
Function:
(defun print-attrib-spec (attrspec pstate) (declare (xargs :guard (and (attrib-specp attrspec) (pristatep pstate)))) (let ((__function__ 'print-attrib-spec)) (declare (ignorable __function__)) (b* ((pstate (print-astring "__attribute__ ((" pstate)) (attrs (attrib-spec->attribs attrspec)) (pstate (if (consp attrs) (print-attrib-list attrs pstate) pstate)) (pstate (print-astring "))" pstate))) pstate)))
Function:
(defun print-attrib-spec-list (attrspecs pstate) (declare (xargs :guard (and (attrib-spec-listp attrspecs) (pristatep pstate)))) (declare (xargs :guard (consp attrspecs))) (let ((__function__ 'print-attrib-spec-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp attrspecs))) (pristate-fix pstate)) (pstate (print-attrib-spec (car attrspecs) pstate)) ((when (endp (cdr attrspecs))) pstate) (pstate (print-astring " " pstate))) (print-attrib-spec-list (cdr attrspecs) pstate))))
Theorem:
(defthm return-type-of-print-expr.new-pstate (b* ((?new-pstate (print-expr expr expected-prio pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-expr-list.new-pstate (b* ((?new-pstate (print-expr-list exprs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-const-expr.new-pstate (b* ((?new-pstate (print-const-expr cexpr pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-genassoc.new-pstate (b* ((?new-pstate (print-genassoc genassoc pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-genassoc-list.new-pstate (b* ((?new-pstate (print-genassoc-list genassocs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-type-spec.new-pstate (b* ((?new-pstate (print-type-spec tyspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-spec/qual.new-pstate (b* ((?new-pstate (print-spec/qual specqual pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-spec/qual-list.new-pstate (b* ((?new-pstate (print-spec/qual-list specquals pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-align-spec.new-pstate (b* ((?new-pstate (print-align-spec alignspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-declspec.new-pstate (b* ((?new-pstate (print-declspec declspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-declspec-list.new-pstate (b* ((?new-pstate (print-declspec-list declspecs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-initer.new-pstate (b* ((?new-pstate (print-initer initer pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-desiniter.new-pstate (b* ((?new-pstate (print-desiniter desiniter pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-desiniter-list.new-pstate (b* ((?new-pstate (print-desiniter-list desiniters pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-designor.new-pstate (b* ((?new-pstate (print-designor designor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-designor-list.new-pstate (b* ((?new-pstate (print-designor-list designors pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-declor.new-pstate (b* ((?new-pstate (print-declor declor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-dirdeclor.new-pstate (b* ((?new-pstate (print-dirdeclor dirdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-absdeclor.new-pstate (b* ((?new-pstate (print-absdeclor absdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-dirabsdeclor.new-pstate (b* ((?new-pstate (print-dirabsdeclor dirabsdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-paramdecl.new-pstate (b* ((?new-pstate (print-paramdecl paramdecl pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-paramdecl-list.new-pstate (b* ((?new-pstate (print-paramdecl-list paramdecls pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-paramdeclor.new-pstate (b* ((?new-pstate (print-paramdeclor paramdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-tyname.new-pstate (b* ((?new-pstate (print-tyname tyname pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-strunispec.new-pstate (b* ((?new-pstate (print-strunispec strunispec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-structdecl.new-pstate (b* ((?new-pstate (print-structdecl structdecl pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-structdecl-list.new-pstate (b* ((?new-pstate (print-structdecl-list structdecls pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-structdeclor.new-pstate (b* ((?new-pstate (print-structdeclor structdeclor pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-structdeclor-list.new-pstate (b* ((?new-pstate (print-structdeclor-list structdeclors pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-enumspec.new-pstate (b* ((?new-pstate (print-enumspec enumspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-enumer.new-pstate (b* ((?new-pstate (print-enumer enumer pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-enumer-list.new-pstate (b* ((?new-pstate (print-enumer-list enumers pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-statassert.new-pstate (b* ((?new-pstate (print-statassert statassert pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-attrib.new-pstate (b* ((?new-pstate (print-attrib attr pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-attrib-list.new-pstate (b* ((?new-pstate (print-attrib-list attrs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-attrib-spec.new-pstate (b* ((?new-pstate (print-attrib-spec attrspec pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-attrib-spec-list.new-pstate (b* ((?new-pstate (print-attrib-spec-list attrspecs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-expr-of-expr-fix-expr (equal (print-expr (expr-fix expr) expected-prio pstate) (print-expr expr expected-prio pstate)))
Theorem:
(defthm print-expr-of-expr-priority-fix-expected-prio (equal (print-expr expr (expr-priority-fix expected-prio) pstate) (print-expr expr expected-prio pstate)))
Theorem:
(defthm print-expr-of-pristate-fix-pstate (equal (print-expr expr expected-prio (pristate-fix pstate)) (print-expr expr expected-prio pstate)))
Theorem:
(defthm print-expr-list-of-expr-list-fix-exprs (equal (print-expr-list (expr-list-fix exprs) pstate) (print-expr-list exprs pstate)))
Theorem:
(defthm print-expr-list-of-pristate-fix-pstate (equal (print-expr-list exprs (pristate-fix pstate)) (print-expr-list exprs pstate)))
Theorem:
(defthm print-const-expr-of-const-expr-fix-cexpr (equal (print-const-expr (const-expr-fix cexpr) pstate) (print-const-expr cexpr pstate)))
Theorem:
(defthm print-const-expr-of-pristate-fix-pstate (equal (print-const-expr cexpr (pristate-fix pstate)) (print-const-expr cexpr pstate)))
Theorem:
(defthm print-genassoc-of-genassoc-fix-genassoc (equal (print-genassoc (genassoc-fix genassoc) pstate) (print-genassoc genassoc pstate)))
Theorem:
(defthm print-genassoc-of-pristate-fix-pstate (equal (print-genassoc genassoc (pristate-fix pstate)) (print-genassoc genassoc pstate)))
Theorem:
(defthm print-genassoc-list-of-genassoc-list-fix-genassocs (equal (print-genassoc-list (genassoc-list-fix genassocs) pstate) (print-genassoc-list genassocs pstate)))
Theorem:
(defthm print-genassoc-list-of-pristate-fix-pstate (equal (print-genassoc-list genassocs (pristate-fix pstate)) (print-genassoc-list genassocs pstate)))
Theorem:
(defthm print-type-spec-of-type-spec-fix-tyspec (equal (print-type-spec (type-spec-fix tyspec) pstate) (print-type-spec tyspec pstate)))
Theorem:
(defthm print-type-spec-of-pristate-fix-pstate (equal (print-type-spec tyspec (pristate-fix pstate)) (print-type-spec tyspec pstate)))
Theorem:
(defthm print-spec/qual-of-spec/qual-fix-specqual (equal (print-spec/qual (spec/qual-fix specqual) pstate) (print-spec/qual specqual pstate)))
Theorem:
(defthm print-spec/qual-of-pristate-fix-pstate (equal (print-spec/qual specqual (pristate-fix pstate)) (print-spec/qual specqual pstate)))
Theorem:
(defthm print-spec/qual-list-of-spec/qual-list-fix-specquals (equal (print-spec/qual-list (spec/qual-list-fix specquals) pstate) (print-spec/qual-list specquals pstate)))
Theorem:
(defthm print-spec/qual-list-of-pristate-fix-pstate (equal (print-spec/qual-list specquals (pristate-fix pstate)) (print-spec/qual-list specquals pstate)))
Theorem:
(defthm print-align-spec-of-align-spec-fix-alignspec (equal (print-align-spec (align-spec-fix alignspec) pstate) (print-align-spec alignspec pstate)))
Theorem:
(defthm print-align-spec-of-pristate-fix-pstate (equal (print-align-spec alignspec (pristate-fix pstate)) (print-align-spec alignspec pstate)))
Theorem:
(defthm print-declspec-of-declspec-fix-declspec (equal (print-declspec (declspec-fix declspec) pstate) (print-declspec declspec pstate)))
Theorem:
(defthm print-declspec-of-pristate-fix-pstate (equal (print-declspec declspec (pristate-fix pstate)) (print-declspec declspec pstate)))
Theorem:
(defthm print-declspec-list-of-declspec-list-fix-declspecs (equal (print-declspec-list (declspec-list-fix declspecs) pstate) (print-declspec-list declspecs pstate)))
Theorem:
(defthm print-declspec-list-of-pristate-fix-pstate (equal (print-declspec-list declspecs (pristate-fix pstate)) (print-declspec-list declspecs pstate)))
Theorem:
(defthm print-initer-of-initer-fix-initer (equal (print-initer (initer-fix initer) pstate) (print-initer initer pstate)))
Theorem:
(defthm print-initer-of-pristate-fix-pstate (equal (print-initer initer (pristate-fix pstate)) (print-initer initer pstate)))
Theorem:
(defthm print-desiniter-of-desiniter-fix-desiniter (equal (print-desiniter (desiniter-fix desiniter) pstate) (print-desiniter desiniter pstate)))
Theorem:
(defthm print-desiniter-of-pristate-fix-pstate (equal (print-desiniter desiniter (pristate-fix pstate)) (print-desiniter desiniter pstate)))
Theorem:
(defthm print-desiniter-list-of-desiniter-list-fix-desiniters (equal (print-desiniter-list (desiniter-list-fix desiniters) pstate) (print-desiniter-list desiniters pstate)))
Theorem:
(defthm print-desiniter-list-of-pristate-fix-pstate (equal (print-desiniter-list desiniters (pristate-fix pstate)) (print-desiniter-list desiniters pstate)))
Theorem:
(defthm print-designor-of-designor-fix-designor (equal (print-designor (designor-fix designor) pstate) (print-designor designor pstate)))
Theorem:
(defthm print-designor-of-pristate-fix-pstate (equal (print-designor designor (pristate-fix pstate)) (print-designor designor pstate)))
Theorem:
(defthm print-designor-list-of-designor-list-fix-designors (equal (print-designor-list (designor-list-fix designors) pstate) (print-designor-list designors pstate)))
Theorem:
(defthm print-designor-list-of-pristate-fix-pstate (equal (print-designor-list designors (pristate-fix pstate)) (print-designor-list designors pstate)))
Theorem:
(defthm print-declor-of-declor-fix-declor (equal (print-declor (declor-fix declor) pstate) (print-declor declor pstate)))
Theorem:
(defthm print-declor-of-pristate-fix-pstate (equal (print-declor declor (pristate-fix pstate)) (print-declor declor pstate)))
Theorem:
(defthm print-dirdeclor-of-dirdeclor-fix-dirdeclor (equal (print-dirdeclor (dirdeclor-fix dirdeclor) pstate) (print-dirdeclor dirdeclor pstate)))
Theorem:
(defthm print-dirdeclor-of-pristate-fix-pstate (equal (print-dirdeclor dirdeclor (pristate-fix pstate)) (print-dirdeclor dirdeclor pstate)))
Theorem:
(defthm print-absdeclor-of-absdeclor-fix-absdeclor (equal (print-absdeclor (absdeclor-fix absdeclor) pstate) (print-absdeclor absdeclor pstate)))
Theorem:
(defthm print-absdeclor-of-pristate-fix-pstate (equal (print-absdeclor absdeclor (pristate-fix pstate)) (print-absdeclor absdeclor pstate)))
Theorem:
(defthm print-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor (equal (print-dirabsdeclor (dirabsdeclor-fix dirabsdeclor) pstate) (print-dirabsdeclor dirabsdeclor pstate)))
Theorem:
(defthm print-dirabsdeclor-of-pristate-fix-pstate (equal (print-dirabsdeclor dirabsdeclor (pristate-fix pstate)) (print-dirabsdeclor dirabsdeclor pstate)))
Theorem:
(defthm print-paramdecl-of-paramdecl-fix-paramdecl (equal (print-paramdecl (paramdecl-fix paramdecl) pstate) (print-paramdecl paramdecl pstate)))
Theorem:
(defthm print-paramdecl-of-pristate-fix-pstate (equal (print-paramdecl paramdecl (pristate-fix pstate)) (print-paramdecl paramdecl pstate)))
Theorem:
(defthm print-paramdecl-list-of-paramdecl-list-fix-paramdecls (equal (print-paramdecl-list (paramdecl-list-fix paramdecls) pstate) (print-paramdecl-list paramdecls pstate)))
Theorem:
(defthm print-paramdecl-list-of-pristate-fix-pstate (equal (print-paramdecl-list paramdecls (pristate-fix pstate)) (print-paramdecl-list paramdecls pstate)))
Theorem:
(defthm print-paramdeclor-of-paramdeclor-fix-paramdeclor (equal (print-paramdeclor (paramdeclor-fix paramdeclor) pstate) (print-paramdeclor paramdeclor pstate)))
Theorem:
(defthm print-paramdeclor-of-pristate-fix-pstate (equal (print-paramdeclor paramdeclor (pristate-fix pstate)) (print-paramdeclor paramdeclor pstate)))
Theorem:
(defthm print-tyname-of-tyname-fix-tyname (equal (print-tyname (tyname-fix tyname) pstate) (print-tyname tyname pstate)))
Theorem:
(defthm print-tyname-of-pristate-fix-pstate (equal (print-tyname tyname (pristate-fix pstate)) (print-tyname tyname pstate)))
Theorem:
(defthm print-strunispec-of-strunispec-fix-strunispec (equal (print-strunispec (strunispec-fix strunispec) pstate) (print-strunispec strunispec pstate)))
Theorem:
(defthm print-strunispec-of-pristate-fix-pstate (equal (print-strunispec strunispec (pristate-fix pstate)) (print-strunispec strunispec pstate)))
Theorem:
(defthm print-structdecl-of-structdecl-fix-structdecl (equal (print-structdecl (structdecl-fix structdecl) pstate) (print-structdecl structdecl pstate)))
Theorem:
(defthm print-structdecl-of-pristate-fix-pstate (equal (print-structdecl structdecl (pristate-fix pstate)) (print-structdecl structdecl pstate)))
Theorem:
(defthm print-structdecl-list-of-structdecl-list-fix-structdecls (equal (print-structdecl-list (structdecl-list-fix structdecls) pstate) (print-structdecl-list structdecls pstate)))
Theorem:
(defthm print-structdecl-list-of-pristate-fix-pstate (equal (print-structdecl-list structdecls (pristate-fix pstate)) (print-structdecl-list structdecls pstate)))
Theorem:
(defthm print-structdeclor-of-structdeclor-fix-structdeclor (equal (print-structdeclor (structdeclor-fix structdeclor) pstate) (print-structdeclor structdeclor pstate)))
Theorem:
(defthm print-structdeclor-of-pristate-fix-pstate (equal (print-structdeclor structdeclor (pristate-fix pstate)) (print-structdeclor structdeclor pstate)))
Theorem:
(defthm print-structdeclor-list-of-structdeclor-list-fix-structdeclors (equal (print-structdeclor-list (structdeclor-list-fix structdeclors) pstate) (print-structdeclor-list structdeclors pstate)))
Theorem:
(defthm print-structdeclor-list-of-pristate-fix-pstate (equal (print-structdeclor-list structdeclors (pristate-fix pstate)) (print-structdeclor-list structdeclors pstate)))
Theorem:
(defthm print-enumspec-of-enumspec-fix-enumspec (equal (print-enumspec (enumspec-fix enumspec) pstate) (print-enumspec enumspec pstate)))
Theorem:
(defthm print-enumspec-of-pristate-fix-pstate (equal (print-enumspec enumspec (pristate-fix pstate)) (print-enumspec enumspec pstate)))
Theorem:
(defthm print-enumer-of-enumer-fix-enumer (equal (print-enumer (enumer-fix enumer) pstate) (print-enumer enumer pstate)))
Theorem:
(defthm print-enumer-of-pristate-fix-pstate (equal (print-enumer enumer (pristate-fix pstate)) (print-enumer enumer pstate)))
Theorem:
(defthm print-enumer-list-of-enumer-list-fix-enumers (equal (print-enumer-list (enumer-list-fix enumers) pstate) (print-enumer-list enumers pstate)))
Theorem:
(defthm print-enumer-list-of-pristate-fix-pstate (equal (print-enumer-list enumers (pristate-fix pstate)) (print-enumer-list enumers pstate)))
Theorem:
(defthm print-statassert-of-statassert-fix-statassert (equal (print-statassert (statassert-fix statassert) pstate) (print-statassert statassert pstate)))
Theorem:
(defthm print-statassert-of-pristate-fix-pstate (equal (print-statassert statassert (pristate-fix pstate)) (print-statassert statassert pstate)))
Theorem:
(defthm print-attrib-of-attrib-fix-attr (equal (print-attrib (attrib-fix attr) pstate) (print-attrib attr pstate)))
Theorem:
(defthm print-attrib-of-pristate-fix-pstate (equal (print-attrib attr (pristate-fix pstate)) (print-attrib attr pstate)))
Theorem:
(defthm print-attrib-list-of-attrib-list-fix-attrs (equal (print-attrib-list (attrib-list-fix attrs) pstate) (print-attrib-list attrs pstate)))
Theorem:
(defthm print-attrib-list-of-pristate-fix-pstate (equal (print-attrib-list attrs (pristate-fix pstate)) (print-attrib-list attrs pstate)))
Theorem:
(defthm print-attrib-spec-of-attrib-spec-fix-attrspec (equal (print-attrib-spec (attrib-spec-fix attrspec) pstate) (print-attrib-spec attrspec pstate)))
Theorem:
(defthm print-attrib-spec-of-pristate-fix-pstate (equal (print-attrib-spec attrspec (pristate-fix pstate)) (print-attrib-spec attrspec pstate)))
Theorem:
(defthm print-attrib-spec-list-of-attrib-spec-list-fix-attrspecs (equal (print-attrib-spec-list (attrib-spec-list-fix attrspecs) pstate) (print-attrib-spec-list attrspecs pstate)))
Theorem:
(defthm print-attrib-spec-list-of-pristate-fix-pstate (equal (print-attrib-spec-list attrspecs (pristate-fix pstate)) (print-attrib-spec-list attrspecs pstate)))
Theorem:
(defthm print-expr-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (print-expr expr expected-prio pstate) (print-expr expr-equiv expected-prio pstate))) :rule-classes :congruence)
Theorem:
(defthm print-expr-expr-priority-equiv-congruence-on-expected-prio (implies (expr-priority-equiv expected-prio expected-prio-equiv) (equal (print-expr expr expected-prio pstate) (print-expr expr expected-prio-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-expr-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-expr expr expected-prio pstate) (print-expr expr expected-prio pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-expr-list-expr-list-equiv-congruence-on-exprs (implies (expr-list-equiv exprs exprs-equiv) (equal (print-expr-list exprs pstate) (print-expr-list exprs-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-expr-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-expr-list exprs pstate) (print-expr-list exprs pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-const-expr-const-expr-equiv-congruence-on-cexpr (implies (const-expr-equiv cexpr cexpr-equiv) (equal (print-const-expr cexpr pstate) (print-const-expr cexpr-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-const-expr-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-const-expr cexpr pstate) (print-const-expr cexpr pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-genassoc-genassoc-equiv-congruence-on-genassoc (implies (genassoc-equiv genassoc genassoc-equiv) (equal (print-genassoc genassoc pstate) (print-genassoc genassoc-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-genassoc-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-genassoc genassoc pstate) (print-genassoc genassoc pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-genassoc-list-genassoc-list-equiv-congruence-on-genassocs (implies (genassoc-list-equiv genassocs genassocs-equiv) (equal (print-genassoc-list genassocs pstate) (print-genassoc-list genassocs-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-genassoc-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-genassoc-list genassocs pstate) (print-genassoc-list genassocs pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-type-spec-type-spec-equiv-congruence-on-tyspec (implies (type-spec-equiv tyspec tyspec-equiv) (equal (print-type-spec tyspec pstate) (print-type-spec tyspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-type-spec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-type-spec tyspec pstate) (print-type-spec tyspec pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-spec/qual-spec/qual-equiv-congruence-on-specqual (implies (spec/qual-equiv specqual specqual-equiv) (equal (print-spec/qual specqual pstate) (print-spec/qual specqual-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-spec/qual-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-spec/qual specqual pstate) (print-spec/qual specqual pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-spec/qual-list-spec/qual-list-equiv-congruence-on-specquals (implies (spec/qual-list-equiv specquals specquals-equiv) (equal (print-spec/qual-list specquals pstate) (print-spec/qual-list specquals-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-spec/qual-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-spec/qual-list specquals pstate) (print-spec/qual-list specquals pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-align-spec-align-spec-equiv-congruence-on-alignspec (implies (align-spec-equiv alignspec alignspec-equiv) (equal (print-align-spec alignspec pstate) (print-align-spec alignspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-align-spec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-align-spec alignspec pstate) (print-align-spec alignspec pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-declspec-declspec-equiv-congruence-on-declspec (implies (declspec-equiv declspec declspec-equiv) (equal (print-declspec declspec pstate) (print-declspec declspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-declspec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-declspec declspec pstate) (print-declspec declspec pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-declspec-list-declspec-list-equiv-congruence-on-declspecs (implies (declspec-list-equiv declspecs declspecs-equiv) (equal (print-declspec-list declspecs pstate) (print-declspec-list declspecs-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-declspec-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-declspec-list declspecs pstate) (print-declspec-list declspecs pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-initer-initer-equiv-congruence-on-initer (implies (initer-equiv initer initer-equiv) (equal (print-initer initer pstate) (print-initer initer-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-initer-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-initer initer pstate) (print-initer initer pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-desiniter-desiniter-equiv-congruence-on-desiniter (implies (desiniter-equiv desiniter desiniter-equiv) (equal (print-desiniter desiniter pstate) (print-desiniter desiniter-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-desiniter-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-desiniter desiniter pstate) (print-desiniter desiniter pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-desiniter-list-desiniter-list-equiv-congruence-on-desiniters (implies (desiniter-list-equiv desiniters desiniters-equiv) (equal (print-desiniter-list desiniters pstate) (print-desiniter-list desiniters-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-desiniter-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-desiniter-list desiniters pstate) (print-desiniter-list desiniters pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-designor-designor-equiv-congruence-on-designor (implies (designor-equiv designor designor-equiv) (equal (print-designor designor pstate) (print-designor designor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-designor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-designor designor pstate) (print-designor designor pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-designor-list-designor-list-equiv-congruence-on-designors (implies (designor-list-equiv designors designors-equiv) (equal (print-designor-list designors pstate) (print-designor-list designors-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-designor-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-designor-list designors pstate) (print-designor-list designors pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-declor-declor-equiv-congruence-on-declor (implies (declor-equiv declor declor-equiv) (equal (print-declor declor pstate) (print-declor declor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-declor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-declor declor pstate) (print-declor declor pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-dirdeclor-dirdeclor-equiv-congruence-on-dirdeclor (implies (dirdeclor-equiv dirdeclor dirdeclor-equiv) (equal (print-dirdeclor dirdeclor pstate) (print-dirdeclor dirdeclor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-dirdeclor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-dirdeclor dirdeclor pstate) (print-dirdeclor dirdeclor pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-absdeclor-absdeclor-equiv-congruence-on-absdeclor (implies (absdeclor-equiv absdeclor absdeclor-equiv) (equal (print-absdeclor absdeclor pstate) (print-absdeclor absdeclor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-absdeclor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-absdeclor absdeclor pstate) (print-absdeclor absdeclor pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor (implies (dirabsdeclor-equiv dirabsdeclor dirabsdeclor-equiv) (equal (print-dirabsdeclor dirabsdeclor pstate) (print-dirabsdeclor dirabsdeclor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-dirabsdeclor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-dirabsdeclor dirabsdeclor pstate) (print-dirabsdeclor dirabsdeclor pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-paramdecl-paramdecl-equiv-congruence-on-paramdecl (implies (paramdecl-equiv paramdecl paramdecl-equiv) (equal (print-paramdecl paramdecl pstate) (print-paramdecl paramdecl-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-paramdecl-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-paramdecl paramdecl pstate) (print-paramdecl paramdecl pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-paramdecl-list-paramdecl-list-equiv-congruence-on-paramdecls (implies (paramdecl-list-equiv paramdecls paramdecls-equiv) (equal (print-paramdecl-list paramdecls pstate) (print-paramdecl-list paramdecls-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-paramdecl-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-paramdecl-list paramdecls pstate) (print-paramdecl-list paramdecls pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-paramdeclor-paramdeclor-equiv-congruence-on-paramdeclor (implies (paramdeclor-equiv paramdeclor paramdeclor-equiv) (equal (print-paramdeclor paramdeclor pstate) (print-paramdeclor paramdeclor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-paramdeclor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-paramdeclor paramdeclor pstate) (print-paramdeclor paramdeclor pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-tyname-tyname-equiv-congruence-on-tyname (implies (tyname-equiv tyname tyname-equiv) (equal (print-tyname tyname pstate) (print-tyname tyname-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-tyname-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-tyname tyname pstate) (print-tyname tyname pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-strunispec-strunispec-equiv-congruence-on-strunispec (implies (strunispec-equiv strunispec strunispec-equiv) (equal (print-strunispec strunispec pstate) (print-strunispec strunispec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-strunispec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-strunispec strunispec pstate) (print-strunispec strunispec pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-structdecl-structdecl-equiv-congruence-on-structdecl (implies (structdecl-equiv structdecl structdecl-equiv) (equal (print-structdecl structdecl pstate) (print-structdecl structdecl-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-structdecl-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-structdecl structdecl pstate) (print-structdecl structdecl pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-structdecl-list-structdecl-list-equiv-congruence-on-structdecls (implies (structdecl-list-equiv structdecls structdecls-equiv) (equal (print-structdecl-list structdecls pstate) (print-structdecl-list structdecls-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-structdecl-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-structdecl-list structdecls pstate) (print-structdecl-list structdecls pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-structdeclor-structdeclor-equiv-congruence-on-structdeclor (implies (structdeclor-equiv structdeclor structdeclor-equiv) (equal (print-structdeclor structdeclor pstate) (print-structdeclor structdeclor-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-structdeclor-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-structdeclor structdeclor pstate) (print-structdeclor structdeclor pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-structdeclor-list-structdeclor-list-equiv-congruence-on-structdeclors (implies (structdeclor-list-equiv structdeclors structdeclors-equiv) (equal (print-structdeclor-list structdeclors pstate) (print-structdeclor-list structdeclors-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-structdeclor-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-structdeclor-list structdeclors pstate) (print-structdeclor-list structdeclors pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-enumspec-enumspec-equiv-congruence-on-enumspec (implies (enumspec-equiv enumspec enumspec-equiv) (equal (print-enumspec enumspec pstate) (print-enumspec enumspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-enumspec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-enumspec enumspec pstate) (print-enumspec enumspec pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-enumer-enumer-equiv-congruence-on-enumer (implies (enumer-equiv enumer enumer-equiv) (equal (print-enumer enumer pstate) (print-enumer enumer-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-enumer-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-enumer enumer pstate) (print-enumer enumer pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-enumer-list-enumer-list-equiv-congruence-on-enumers (implies (enumer-list-equiv enumers enumers-equiv) (equal (print-enumer-list enumers pstate) (print-enumer-list enumers-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-enumer-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-enumer-list enumers pstate) (print-enumer-list enumers pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-statassert-statassert-equiv-congruence-on-statassert (implies (statassert-equiv statassert statassert-equiv) (equal (print-statassert statassert pstate) (print-statassert statassert-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-statassert-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-statassert statassert pstate) (print-statassert statassert pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-attrib-equiv-congruence-on-attr (implies (attrib-equiv attr attr-equiv) (equal (print-attrib attr pstate) (print-attrib attr-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-attrib attr pstate) (print-attrib attr pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-list-attrib-list-equiv-congruence-on-attrs (implies (attrib-list-equiv attrs attrs-equiv) (equal (print-attrib-list attrs pstate) (print-attrib-list attrs-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-attrib-list attrs pstate) (print-attrib-list attrs pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-spec-attrib-spec-equiv-congruence-on-attrspec (implies (attrib-spec-equiv attrspec attrspec-equiv) (equal (print-attrib-spec attrspec pstate) (print-attrib-spec attrspec-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-spec-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-attrib-spec attrspec pstate) (print-attrib-spec attrspec pstate-equiv))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-spec-list-attrib-spec-list-equiv-congruence-on-attrspecs (implies (attrib-spec-list-equiv attrspecs attrspecs-equiv) (equal (print-attrib-spec-list attrspecs pstate) (print-attrib-spec-list attrspecs-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-attrib-spec-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-attrib-spec-list attrspecs pstate) (print-attrib-spec-list attrspecs pstate-equiv))) :rule-classes :congruence)