		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Concatenation-unambiguousp

Notion of unambiguous concatenations.

A concatenation is unambiguous iff any two lists of lists of trees that match the concatenation and have the same string at the leaves are the same list of lists of trees.

An empty concatenation is always unambiguous.

Definitions and Theorems

Theorem: concatenation-unambiguousp-necc

(defthm concatenation-unambiguousp-necc
  (implies (concatenation-unambiguousp concatenation rules)
           (implies (and (tree-list-listp treess1)
                         (tree-list-listp treess2)
                         (tree-list-list-match-concatenation-p
                              treess1 concatenation rules)
                         (tree-list-list-match-concatenation-p
                              treess2 concatenation rules))
                    (equal (equal (tree-list-list->string treess1)
                                  (tree-list-list->string treess2))
                           (equal treess1 treess2)))))

Theorem: booleanp-of-concatenation-unambiguousp

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

Theorem: concatenation-unambiguousp-rewrite

(defthm concatenation-unambiguousp-rewrite
  (implies (and (concatenation-unambiguousp concatenation rules)
                (tree-list-list-match-concatenation-p
                     treess1 concatenation rules)
                (tree-list-list-match-concatenation-p
                     treess2 concatenation rules))
           (equal (equal (tree-list-list->string treess1)
                         (tree-list-list->string treess2))
                  (tree-list-list-equiv treess1 treess2))))

Theorem: empty-concatenation-unambiguous

(defthm empty-concatenation-unambiguous
  (concatenation-unambiguousp nil rules))