		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Alternation-unambiguousp

Notion of unambiguous alternations.

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

An empty alternation is always unambiguous.

Definitions and Theorems

Theorem: alternation-unambiguousp-necc

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

Theorem: booleanp-of-alternation-unambiguousp

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

Theorem: alternation-unambiguousp-rewrite

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

Theorem: alternation-unambiguousp-of-nil

(defthm alternation-unambiguousp-of-nil
  (alternation-unambiguousp nil rules))