Print a list of one or more attribute specifiers, separated by single spaces.
(print-attrib-spec-list attrspecs pstate) → new-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)) (print-attrib-spec-list (cdr attrspecs) pstate))))
Theorem:
(defthm pristatep-of-print-attrib-spec-list (b* ((new-pstate (print-attrib-spec-list attrspecs pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
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-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-of-pristate-fix-pstate (equal (print-attrib-spec-list attrspecs (pristate-fix pstate)) (print-attrib-spec-list attrspecs pstate)))
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)