Basic theorems about dec-digit-char-list*p, generated by std::deflist.
Theorem:
(defthm dec-digit-char-list*p-of-cons (equal (dec-digit-char-list*p (cons a x)) (and (dec-digit-char-p a) (dec-digit-char-list*p x))) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-list*p-of-cdr-when-dec-digit-char-list*p (implies (dec-digit-char-list*p (double-rewrite x)) (dec-digit-char-list*p (cdr x))) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-list*p-when-not-consp (implies (not (consp x)) (dec-digit-char-list*p x)) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-p-of-car-when-dec-digit-char-list*p (implies (dec-digit-char-list*p x) (iff (dec-digit-char-p (car x)) (or (consp x) (dec-digit-char-p nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-list*p-of-append (equal (dec-digit-char-list*p (append a b)) (and (dec-digit-char-list*p a) (dec-digit-char-list*p b))) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-list*p-of-list-fix (equal (dec-digit-char-list*p (list-fix x)) (dec-digit-char-list*p x)) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-list*p-of-rev (equal (dec-digit-char-list*p (rev x)) (dec-digit-char-list*p (list-fix x))) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-list*p-of-take (implies (dec-digit-char-list*p (double-rewrite x)) (iff (dec-digit-char-list*p (take n x)) (or (dec-digit-char-p nil) (<= (nfix n) (len x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-list*p-of-nthcdr (implies (dec-digit-char-list*p (double-rewrite x)) (dec-digit-char-list*p (nthcdr n x))) :rule-classes ((:rewrite)))
Theorem:
(defthm dec-digit-char-list*p-of-repeat (iff (dec-digit-char-list*p (repeat n x)) (or (dec-digit-char-p x) (zp n))) :rule-classes ((:rewrite)))