		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Concatenation-alternation-disjointp

Notion of disjoint concatenation-alternation pairs.

A concatenation is disjoint from an alternation iff the concatenation and the alternation are matched by disjoint sets of lists of lists of trees. That is, there is no list of lists of trees that matches both the concatenation and the alternation.

The empty alternation is disjoint from the empty concatenation.

Definitions and Theorems

Theorem: concatenation-alternation-disjointp-necc

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

Theorem: booleanp-of-concatenation-alternation-disjointp

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

Theorem: concatenation-alternation-disjointp-of-nil

(defthm concatenation-alternation-disjointp-of-nil
  (concatenation-alternation-disjointp concatenation nil rules))