Print zero or more ACL2 decimal digit characters.
(print-dec-digit-achars achars pstate) → new-pstate
Function:
(defun print-dec-digit-achars (achars pstate) (declare (xargs :guard (and (dec-digit-char-listp achars) (pristatep pstate)))) (let ((__function__ 'print-dec-digit-achars)) (declare (ignorable __function__)) (b* (((when (endp achars)) (pristate-fix pstate)) (pstate (print-dec-digit-achar (car achars) pstate))) (print-dec-digit-achars (cdr achars) pstate))))
Theorem:
(defthm pristatep-of-print-dec-digit-achars (b* ((new-pstate (print-dec-digit-achars achars pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-dec-digit-achars-of-pristate-fix-pstate (equal (print-dec-digit-achars achars (pristate-fix pstate)) (print-dec-digit-achars achars pstate)))
Theorem:
(defthm print-dec-digit-achars-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-dec-digit-achars achars pstate) (print-dec-digit-achars achars pstate-equiv))) :rule-classes :congruence)