		Search-engine friendly clone of the ACL2 documentation.

Semantics

Terminal-string-for-rules-p

Recognize terminal strings generated by a grammar.

This predicate recognizes all the sequences of natural numbers that form parsable strings, for any rule names. This is equivalent to languagep when all the rule names are passed as second argument of that predicates.

Note that the condition that the existentially quantified rulename be defined by rules would be superfluous, because if rulename is not defined then no parse trees with only terminal leaves can originate from it.

Definitions and Theorems

Theorem: terminal-string-for-rules-p-suff

(defthm terminal-string-for-rules-p-suff
  (implies (and (nat-listp nats)
                (rulenamep rulename)
                (string-parsablep nats rulename rules))
           (terminal-string-for-rules-p nats rules)))

Theorem: booleanp-of-terminal-string-for-rules-p

(defthm booleanp-of-terminal-string-for-rules-p
  (b* ((yes/no (terminal-string-for-rules-p nats rules)))
    (booleanp yes/no))
  :rule-classes :rewrite)