		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Element-unambiguousp

Notion of unambiguous elements.

An element is unambiguous iff any two trees that match the element and have the same string at the leaves are the same tree.

Definitions and Theorems

Theorem: element-unambiguousp-necc

(defthm element-unambiguousp-necc
  (implies (element-unambiguousp element rules)
           (implies (and (treep tree1)
                         (treep tree2)
                         (tree-match-element-p tree1 element rules)
                         (tree-match-element-p tree2 element rules))
                    (equal (equal (tree->string tree1)
                                  (tree->string tree2))
                           (equal tree1 tree2)))))

Theorem: booleanp-of-element-unambiguousp

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

Theorem: element-ambiguousp-rewrite

(defthm element-ambiguousp-rewrite
  (implies (and (element-unambiguousp element rules)
                (tree-match-element-p tree1 element rules)
                (tree-match-element-p tree2 element rules))
           (equal (equal (tree->string tree1)
                         (tree->string tree2))
                  (tree-equiv tree1 tree2))))