Widening and narrowing conversion
from
(byte-to-char operand) → result
Function:
(defun byte-to-char (operand) (declare (xargs :guard (byte-valuep operand))) (b* ((x (byte-value->int operand))) (char-value (loghead 16 x))))
Theorem:
(defthm char-valuep-of-byte-to-char (b* ((result (byte-to-char operand))) (char-valuep result)) :rule-classes :rewrite)
Theorem:
(defthm byte-to-char-of-byte-value-fix-operand (equal (byte-to-char (byte-value-fix operand)) (byte-to-char operand)))
Theorem:
(defthm byte-to-char-byte-value-equiv-congruence-on-operand (implies (byte-value-equiv operand operand-equiv) (equal (byte-to-char operand) (byte-to-char operand-equiv))) :rule-classes :congruence)