Disambiguation between any two distinct elements among
Theorem:
(defthm fail-a/b/c/d/e/f-when-match-other-a/b/c/d/e/f (implies (and (tree-match-element-p tree element *grammar*) (elementp element) (equal (element-kind element) :char-val) (equal (char-val-kind (element-char-val->get element)) :insensitive) (equal (char-val-insensitive->iprefix (element-char-val->get element)) nil) (member-equal (char-val-insensitive->get (element-char-val->get element)) '("A" "B" "C" "D" "E" "F")) (member-equal char '(#\A #\B #\C #\D #\E #\F)) (not (equal (explode (char-val-insensitive->get (element-char-val->get element))) (list char)))) (mv-nth 0 (parse-ichar char (append (tree->string tree) rest-input)))))