		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Prose-val-ambiguous

Prose value notations are always ambiguous.

We can always construct two different trees with the same string at the leaves that match any prose value notation. Recall that a prose value notation is matched by any tree.

Definitions and Theorems

Theorem: prose-val-ambiguous

(defthm prose-val-ambiguous
 (implies
  (and (equal tree1
              (make-tree-nonleaf
                   :rulename? nil
                   :branches (list (list (tree-leafterm '(1))
                                         (tree-leafterm '(2))))))
       (equal tree2
              (make-tree-nonleaf
                   :rulename? nil
                   :branches (list (list (tree-leafterm '(1 2)))))))
  (and (treep tree1)
       (treep tree2)
       (not (equal tree1 tree2))
       (equal (tree->string tree1)
              (tree->string tree2))
       (tree-match-prose-val-p tree1 prose-val)
       (tree-match-prose-val-p tree2 prose-val))))