		Search-engine friendly clone of the ACL2 documentation.

Core-rules

Core-rules-validation

Validation of the core rules.

We show that the core rules:

Are well-formed.
Are closed.
Generate only strings of octets.
Without the OCTET rule, generate only strings of ASCII codes.

These validation theorems depend on some grammar operations. Thus, we put them in a separate file, avoiding a dependency of the file that defines the core rules on the grammar operations.

Definitions and Theorems

Theorem: rulelist-wfp-of-*core-rules*

(defthm rulelist-wfp-of-*core-rules*
  (rulelist-wfp *core-rules*))

Theorem: rulelist-closedp-of-*core-rules*

(defthm rulelist-closedp-of-*core-rules*
  (rulelist-closedp *core-rules*))

Theorem: octet-only-*core-rules*

(defthm octet-only-*core-rules*
  (rulelist-in-termset-p *core-rules* (integers-from-to 0 255)))

Theorem: ascii-only-*core-rules*-without-*octet*

(defthm ascii-only-*core-rules*-without-*octet*
  (rulelist-in-termset-p (remove-equal *rule_octet* *core-rules*)
                         (integers-from-to 0 127)))