Theorems about results of std/strings functions that return lists of octal digit characters.
Those std/strings are accompanied by theorems that they return oct-digit-char-list*p, but they in fact return true lists, so here we add theorems that they return oct-digit-char-listp.
Theorem:
(defthm oct-digit-char-listp-of-basic-nat-to-oct-chars (oct-digit-char-listp (basic-nat-to-oct-chars nat)))
Theorem:
(defthm oct-digit-char-listp-of-nat-to-oct-chars-aux (implies (oct-digit-char-listp acc) (oct-digit-char-listp (nat-to-oct-chars-aux nat acc))))
Theorem:
(defthm oct-digit-char-listp-of-nat-to-oct-chars (oct-digit-char-listp (nat-to-oct-chars nat)))