explode-atom

(in-package "ACL2")

(local (include-book "explode-nonnegative-integer"))

(in-theory (disable explode-atom))

(defthm character-listp-of-explode-atom
  (character-listp (explode-atom x print-base))
  :hints (("Goal" :in-theory (enable explode-atom))))