Tree matching theorem for parse-bin-val-rest.
Theorem:
(defthm tree-match-of-parse-bin-val-rest (b* (((mv & tree &) (parse-bin-val-rest input))) (implies (equal element (?_ (/_ (1*_ (!_ (/_ "." (1*_ *bit*))))) (/_ (!_ (/_ "-" (1*_ *bit*)))))) (tree-match-element-p tree element *grammar*))))