A
(abstract-alpha/digit/dash tree) → char
Function:
(defun abstract-alpha/digit/dash (tree) (declare (xargs :guard (treep tree))) (b* (((fun (fail)) (prog2$ (abstract-fail) (code-char 0))) ((unless (tree-case tree :nonleaf)) (fail)) (treess (tree-nonleaf->branches tree)) ((unless (consp treess)) (fail)) (trees (car treess)) ((unless (consp trees)) (fail)) (subtree (car trees)) ((when (equal subtree (tree-leafterm (list (char-code #\-))))) #\-) ((unless (tree-case subtree :nonleaf)) (fail)) (rulename? (tree-nonleaf->rulename? subtree)) ((when (equal rulename? (rulename "alpha"))) (abstract-alpha subtree)) (digit (abstract-digit subtree)) ((unless (< digit 10)) (fail))) (code-char (+ (char-code #\0) digit))))
Theorem:
(defthm characterp-of-abstract-alpha/digit/dash (b* ((char (abstract-alpha/digit/dash tree))) (characterp char)) :rule-classes :rewrite)