Apply a sequence of post-increment and post-decrement operators to an expression.
(apply-post-inc/dec-ops expr ops) → new-expr
The first one in the list will be the innermost, and the last one in the list will be the outermost.
Function:
(defun apply-post-inc/dec-ops (expr ops) (declare (xargs :guard (and (exprp expr) (inc/dec-op-listp ops)))) (let ((__function__ 'apply-post-inc/dec-ops)) (declare (ignorable __function__)) (b* (((when (endp ops)) (expr-fix expr)) (op (car ops)) (expr (inc/dec-op-case op :inc (make-expr-unary :op (unop-postinc) :arg expr) :dec (make-expr-unary :op (unop-postdec) :arg expr)))) (apply-post-inc/dec-ops expr (cdr ops)))))
Theorem:
(defthm exprp-of-apply-post-inc/dec-ops (b* ((new-expr (apply-post-inc/dec-ops expr ops))) (exprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm apply-post-inc/dec-ops-of-expr-fix-expr (equal (apply-post-inc/dec-ops (expr-fix expr) ops) (apply-post-inc/dec-ops expr ops)))
Theorem:
(defthm apply-post-inc/dec-ops-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (apply-post-inc/dec-ops expr ops) (apply-post-inc/dec-ops expr-equiv ops))) :rule-classes :congruence)
Theorem:
(defthm apply-post-inc/dec-ops-of-inc/dec-op-list-fix-ops (equal (apply-post-inc/dec-ops expr (inc/dec-op-list-fix ops)) (apply-post-inc/dec-ops expr ops)))
Theorem:
(defthm apply-post-inc/dec-ops-inc/dec-op-list-equiv-congruence-on-ops (implies (inc/dec-op-list-equiv ops ops-equiv) (equal (apply-post-inc/dec-ops expr ops) (apply-post-inc/dec-ops expr ops-equiv))) :rule-classes :congruence)