		Search-engine friendly clone of the ACL2 documentation.

Exec-character-set

Basic-exec-charp

Recognize the basic execution characters.

These are the characters in the image of the injection from the ASCII characters.

Definitions and Theorems

Theorem: basic-exec-charp-suff

(defthm basic-exec-charp-suff
  (implies (and (ascii-basic-exec-charp ascii)
                (equal x (ascii-to-exec-char ascii)))
           (basic-exec-charp x)))

Theorem: booleanp-of-basic-exec-charp

(defthm booleanp-of-basic-exec-charp
  (b* ((yes/no (basic-exec-charp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: exec-charp-when-basic-exec-charp

(defthm exec-charp-when-basic-exec-charp
  (implies (basic-exec-charp x)
           (exec-charp x)))