		Search-engine friendly clone of the ACL2 documentation.

Ambiguity

Char-val-unambiguous

Character value notations are never ambiguous.

Any two trees that match a character value notation and that have the same string at the leaves are the same tree.

Definitions and Theorems

Theorem: char-val-unambiguous

(defthm char-val-unambiguous
  (implies (and (tree-match-char-val-p tree1 char-val)
                (tree-match-char-val-p tree2 char-val))
           (equal (equal (tree->string tree1)
                         (tree->string tree2))
                  (tree-equiv tree1 tree2))))