		Search-engine friendly clone of the ACL2 documentation.

Code-char-injectivity-theorem

code-char is injective on natural numbers below 256.

Note that the injectivity of char-code over characters is expressed by the theorem equal-of-char-code.

Definitions and Theorems

Theorem: equal-of-code-chars

(defthm equal-of-code-chars
  (equal (equal (code-char x) (code-char y))
         (equal (unsigned-byte-fix 8 x)
                (unsigned-byte-fix 8 y))))