Print a list of zero or more increment or decrement operators.
(print-inc/dec-op-list ops pstate) → new-pstate
We separate any two consecutive ones with a space.
Function:
(defun print-inc/dec-op-list (ops pstate) (declare (xargs :guard (and (inc/dec-op-listp ops) (pristatep pstate)))) (let ((__function__ 'print-inc/dec-op-list)) (declare (ignorable __function__)) (b* (((when (endp ops)) (pristate-fix pstate)) (pstate (print-inc/dec-op (car ops) pstate)) ((when (endp (cdr ops))) pstate) (pstate (print-astring " " pstate))) (print-inc/dec-op-list (cdr ops) pstate))))
Theorem:
(defthm pristatep-of-print-inc/dec-op-list (b* ((new-pstate (print-inc/dec-op-list ops pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-inc/dec-op-list-of-inc/dec-op-list-fix-ops (equal (print-inc/dec-op-list (inc/dec-op-list-fix ops) pstate) (print-inc/dec-op-list ops pstate)))
Theorem:
(defthm print-inc/dec-op-list-inc/dec-op-list-equiv-congruence-on-ops (implies (inc/dec-op-list-equiv ops ops-equiv) (equal (print-inc/dec-op-list ops pstate) (print-inc/dec-op-list ops-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-inc/dec-op-list-of-pristate-fix-pstate (equal (print-inc/dec-op-list ops (pristate-fix pstate)) (print-inc/dec-op-list ops pstate)))
Theorem:
(defthm print-inc/dec-op-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-inc/dec-op-list ops pstate) (print-inc/dec-op-list ops pstate-equiv))) :rule-classes :congruence)