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
Theorem:
(defthm rules-ambiguousp-suff (implies (and (stringp string) (rulenamep rulename) (string-ambiguousp string rulename rules)) (rules-ambiguousp rules)))
Theorem:
(defthm booleanp-of-rules-ambiguousp (b* ((yes/no (rules-ambiguousp rules))) (booleanp yes/no)) :rule-classes :rewrite)