Recognizer for non-zero octal digit characters: 1-7.
(nonzero-oct-digit-char-p x) → bool
Function:
(defun nonzero-oct-digit-char-p$inline (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'nonzero-oct-digit-char-p)) (declare (ignorable acl2::__function__)) (mbe :logic (let ((code (char-code (char-fix x)))) (and (<= (char-code #\1) code) (<= code (char-code #\7)))) :exec (and (characterp x) (b* (((the (unsigned-byte 8) code) (char-code (the character x)))) (and (<= code 55) (<= 49 code)))))))
Theorem:
(defthm ichareqv-implies-equal-nonzero-oct-digit-char-p-1 (implies (ichareqv x x-equiv) (equal (nonzero-oct-digit-char-p x) (nonzero-oct-digit-char-p x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm oct-digit-char-p-when-nonzero-oct-digit-char-p (implies (nonzero-oct-digit-char-p x) (oct-digit-char-p x)))