Print a quadruple of hexadecimal digits.
(print-hex-quad quad pstate) → new-pstate
Function:
(defun print-hex-quad (quad pstate) (declare (xargs :guard (and (hex-quad-p quad) (pristatep pstate)))) (let ((__function__ 'print-hex-quad)) (declare (ignorable __function__)) (b* (((hex-quad quad) quad) (pstate (print-hex-digit-achar quad.1st pstate)) (pstate (print-hex-digit-achar quad.2nd pstate)) (pstate (print-hex-digit-achar quad.3rd pstate)) (pstate (print-hex-digit-achar quad.4th pstate))) pstate)))
Theorem:
(defthm pristatep-of-print-hex-quad (b* ((new-pstate (print-hex-quad quad pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-hex-quad-of-hex-quad-fix-quad (equal (print-hex-quad (hex-quad-fix quad) pstate) (print-hex-quad quad pstate)))
Theorem:
(defthm print-hex-quad-hex-quad-equiv-congruence-on-quad (implies (hex-quad-equiv quad quad-equiv) (equal (print-hex-quad quad pstate) (print-hex-quad quad-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-hex-quad-of-pristate-fix-pstate (equal (print-hex-quad quad (pristate-fix pstate)) (print-hex-quad quad pstate)))
Theorem:
(defthm print-hex-quad-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-hex-quad quad pstate) (print-hex-quad quad pstate-equiv))) :rule-classes :congruence)