Recognizes lists of oct-digit-char-p characters.
(oct-digit-char-list*p x) → std::bool
This is an ordinary std::deflist. It is
"loose" in that it does not care whether
Function:
(defun oct-digit-char-list*p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'oct-digit-char-list*p)) (declare (ignorable acl2::__function__)) (if (consp x) (and (oct-digit-char-p (car x)) (oct-digit-char-list*p (cdr x))) t)))
Theorem:
(defthm icharlisteqv-implies-equal-oct-digit-char-list*p-1 (implies (icharlisteqv x x-equiv) (equal (oct-digit-char-list*p x) (oct-digit-char-list*p x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm character-listp-when-oct-digit-char-list*p (implies (oct-digit-char-list*p x) (equal (character-listp x) (true-listp x))) :rule-classes ((:rewrite :backchain-limit-lst 1)))