		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Rules-ambiguousp

Notion of ambiguous lists of rules.

A list of rules is ambiguous iff it includes some ambiguous string. 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 can originate from it.

Definitions and Theorems

Theorem: rules-ambiguousp-suff

(defthm rules-ambiguousp-suff
  (implies (and (stringp string)
                (rulenamep rulename)
                (string-ambiguousp string rulename rules))
           (rules-ambiguousp rules)))

Theorem: booleanp-of-rules-ambiguousp

(defthm booleanp-of-rules-ambiguousp
  (b* ((yes/no (rules-ambiguousp rules)))
    (booleanp yes/no))
  :rule-classes :rewrite)