nats=>string and string=>nats are mutual inverses.
Theorem:
(defthm nats=>string-of-string=>nats (equal (nats=>string (string=>nats string)) (str-fix string)))
Theorem:
(defthm string=>nats-of-nats=>string (implies (unsigned-byte-listp 8 (true-list-fix nats)) (equal (string=>nats (nats=>string nats)) (true-list-fix nats))) :rule-classes ((:rewrite :corollary (implies (unsigned-byte-listp 8 nats) (equal (string=>nats (nats=>string nats)) nats)))))