explode-atom

(defthm true-listp-of-explode-atom
  (true-listp (explode-atom x base))
  :rule-classes :type-prescription)

(defthm consp-of-explode-atom-when-integerp
  (implies (integerp n) (consp (explode-atom n base)))
  :rule-classes :type-prescription)

(defthm equal-of-explode-atoms-when-natps
  (implies (and (natp n) (natp m) (force (print-base-p base)))
    (equal (equal (explode-atom n base) (explode-atom m base))
      (equal n m))))

(defthm nonzeroness-of-explode-atom-when-not-zp
  (implies (and (not (zp n)) (force (print-base-p base)))
    (not (equal (explode-atom n base) '(#\0)))))

(defthm dec-digit-char-list*p-of-explode-atom
  (implies (natp n)
    (dec-digit-char-list*p (explode-atom n 10))))

(defthm character-listp-of-explode-atom
  (character-listp (explode-atom x base))
  :hints (("Goal" :in-theory (disable explode-nonnegative-integer))))

(defthm character-listp-explode-atom+
  (character-listp (explode-atom+ x base radix)))