Print an increment or decrement operator.
(print-inc/dec-op op pstate) → new-pstate
Function:
(defun print-inc/dec-op (op pstate) (declare (xargs :guard (and (inc/dec-opp op) (pristatep pstate)))) (let ((__function__ 'print-inc/dec-op)) (declare (ignorable __function__)) (inc/dec-op-case op :inc (print-astring "++" pstate) :dec (print-astring "--" pstate))))
Theorem:
(defthm pristatep-of-print-inc/dec-op (b* ((new-pstate (print-inc/dec-op op pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-inc/dec-op-of-inc/dec-op-fix-op (equal (print-inc/dec-op (inc/dec-op-fix op) pstate) (print-inc/dec-op op pstate)))
Theorem:
(defthm print-inc/dec-op-inc/dec-op-equiv-congruence-on-op (implies (inc/dec-op-equiv op op-equiv) (equal (print-inc/dec-op op pstate) (print-inc/dec-op op-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-inc/dec-op-of-pristate-fix-pstate (equal (print-inc/dec-op op (pristate-fix pstate)) (print-inc/dec-op op pstate)))
Theorem:
(defthm print-inc/dec-op-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-inc/dec-op op pstate) (print-inc/dec-op op pstate-equiv))) :rule-classes :congruence)