		Search-engine friendly clone of the ACL2 documentation.

Semantics

String-ambiguousp

Notion of ambiguous string.

A string is ambiguous iff it has at least two distinct parse trees.

Definitions and Theorems

Theorem: string-ambiguousp-suff

(defthm string-ambiguousp-suff
  (implies (and (not (equal tree1 tree2))
                (parse-treep tree1 string rulename rules)
                (parse-treep tree2 string rulename rules))
           (string-ambiguousp string rulename rules)))

Theorem: booleanp-of-string-ambiguousp

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

Theorem: string-ambiguousp-of-string-fix-string

(defthm string-ambiguousp-of-string-fix-string
  (equal (string-ambiguousp (string-fix string)
                            rulename rules)
         (string-ambiguousp string rulename rules)))

Theorem: string-ambiguousp-string-equiv-congruence-on-string

(defthm string-ambiguousp-string-equiv-congruence-on-string
  (implies (string-equiv string string-equiv)
           (equal (string-ambiguousp string rulename rules)
                  (string-ambiguousp string-equiv rulename rules)))
  :rule-classes :congruence)

Theorem: string-ambiguousp-of-rulename-fix-rulename

(defthm string-ambiguousp-of-rulename-fix-rulename
  (equal (string-ambiguousp string (rulename-fix rulename)
                            rules)
         (string-ambiguousp string rulename rules)))

Theorem: string-ambiguousp-rulename-equiv-congruence-on-rulename

(defthm string-ambiguousp-rulename-equiv-congruence-on-rulename
  (implies (rulename-equiv rulename rulename-equiv)
           (equal (string-ambiguousp string rulename rules)
                  (string-ambiguousp string rulename-equiv rules)))
  :rule-classes :congruence)

Theorem: string-ambiguousp-of-rulelist-fix-rules

(defthm string-ambiguousp-of-rulelist-fix-rules
  (equal (string-ambiguousp string rulename (rulelist-fix rules))
         (string-ambiguousp string rulename rules)))

Theorem: string-ambiguousp-rulelist-equiv-congruence-on-rules

(defthm string-ambiguousp-rulelist-equiv-congruence-on-rules
  (implies (rulelist-equiv rules rules-equiv)
           (equal (string-ambiguousp string rulename rules)
                  (string-ambiguousp string rulename rules-equiv)))
  :rule-classes :congruence)

Theorem: string-parsablep-when-string-ambiguousp

(defthm string-parsablep-when-string-ambiguousp
  (implies (string-ambiguousp string rulename rules)
           (string-parsablep string rulename rules)))

Theorem: at-most-one-parse-tree-when-not-string-ambiguousp

(defthm at-most-one-parse-tree-when-not-string-ambiguousp
  (implies (and (not (string-ambiguousp string rulename rules))
                (parse-treep tree1 string rulename rules)
                (parse-treep tree2 string rulename rules))
           (equal tree1 tree2))
  :rule-classes nil)