Check if a decimal numeral is well-formed.
(decdig/uscore-list-wfp dus) → yes/no
A
Function:
(defun decdig/uscore-list-wfp (dus) (declare (xargs :guard (decdig/uscore-listp dus))) (let ((__function__ 'decdig/uscore-list-wfp)) (declare (ignorable __function__)) (and (consp dus) (decdig/uscore-case (car dus) :digit) (decdig/uscore-case (car (last dus)) :digit) (implies (equal (decdig/uscore-fix (car dus)) (decdig/uscore-digit (char-code #\0))) (= (len dus) 1)))))
Theorem:
(defthm booleanp-of-decdig/uscore-list-wfp (b* ((yes/no (decdig/uscore-list-wfp dus))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm decdig/uscore-list-wfp-of-decdig/uscore-list-fix-dus (equal (decdig/uscore-list-wfp (decdig/uscore-list-fix dus)) (decdig/uscore-list-wfp dus)))
Theorem:
(defthm decdig/uscore-list-wfp-decdig/uscore-list-equiv-congruence-on-dus (implies (decdig/uscore-list-equiv dus dus-equiv) (equal (decdig/uscore-list-wfp dus) (decdig/uscore-list-wfp dus-equiv))) :rule-classes :congruence)