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