		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Repetition-unambiguousp

Notion of unambiguous repetitions.

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

A repetition of 0 elements is always unambiguous.

Definitions and Theorems

Theorem: repetition-unambiguousp-necc

(defthm repetition-unambiguousp-necc
 (implies
   (repetition-unambiguousp repetition rules)
   (implies
        (and (tree-listp trees1)
             (tree-listp trees2)
             (tree-list-match-repetition-p trees1 repetition rules)
             (tree-list-match-repetition-p trees2 repetition rules))
        (equal (equal (tree-list->string trees1)
                      (tree-list->string trees2))
               (equal trees1 trees2)))))

Theorem: booleanp-of-repetition-unambiguousp

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

Theorem: repetition-unambiguousp-rewrite

(defthm repetition-unambiguousp-rewrite
  (implies
       (and (repetition-unambiguousp repetition rules)
            (tree-list-match-repetition-p trees1 repetition rules)
            (tree-list-match-repetition-p trees2 repetition rules))
       (equal (equal (tree-list->string trees1)
                     (tree-list->string trees2))
              (tree-list-equiv trees1 trees2))))

Theorem: empty-repetition-umabiguous

(defthm empty-repetition-umabiguous
  (implies (equal (repetition->range repetition)
                  (repeat-range 0 (nati-finite 0)))
           (repetition-unambiguousp repetition rules)))