Some theorems about str::nat-to-dec-chars and the functions it calls.
Theorem:
(defthm car-of-last-of-basic-nat-to-dec-chars-not-0 (not (equal (car (last (str::basic-nat-to-dec-chars n))) #\0)))
Theorem:
(defthm car-of-nat-to-dec-chars-aux-not-0 (implies (not (equal (car acc) #\0)) (not (equal (car (str::nat-to-dec-chars-aux n acc)) #\0))))
Theorem:
(defthm len-of-nat-to-dec-chars-is-1-iff-value-below-10 (equal (equal (len (str::nat-to-dec-chars value)) 1) (< (nfix value) 10)))
Theorem:
(defthm nat-to-dec-chars-aux-iff (iff (str::nat-to-dec-chars-aux n acc) (or acc (not (zp n)))))
Theorem:
(defthm car-of-nat-to-dec-chars-is-0-iff-arg-0 (equal (equal (car (str::nat-to-dec-chars n)) #\0) (zp n)))