Number of the basic execution character corresponding to an ASCII character.
(ascii-to-exec-char-number x) → number
Function:
(defun ascii-to-exec-char-number (x) (declare (xargs :guard (ascii-basic-exec-charp x))) (let ((__function__ 'ascii-to-exec-char-number)) (declare (ignorable __function__)) (exec-char-to-number (ascii-to-exec-char x))))
Theorem:
(defthm natp-of-ascii-to-exec-char-number (b* ((number (ascii-to-exec-char-number x))) (natp number)) :rule-classes :type-prescription)
Theorem:
(defthm ascii-to-exec-char-number-of-ascii-basic-exec-char-fix-x (equal (ascii-to-exec-char-number (ascii-basic-exec-char-fix x)) (ascii-to-exec-char-number x)))
Theorem:
(defthm ascii-to-exec-char-number-ascii-basic-exec-char-equiv-congruence-on-x (implies (ascii-basic-exec-char-equiv x x-equiv) (equal (ascii-to-exec-char-number x) (ascii-to-exec-char-number x-equiv))) :rule-classes :congruence)