Parse a repetition
(parse-*-alpha/digit/dash input) → (mv error? trees rest-input)
Function:
(defun parse-*-alpha/digit/dash (input) (declare (xargs :guard (nat-listp input))) (seq-backtrack input ((tree := (parse-alpha/digit/dash input)) (trees := (parse-*-alpha/digit/dash input)) (return (cons tree trees))) ((return-raw (mv nil nil (nat-list-fix input))))))
Theorem:
(defthm not-of-parse-*-alpha/digit/dash.error? (b* (((mv ?error? ?trees ?rest-input) (parse-*-alpha/digit/dash input))) (not error?)) :rule-classes :rewrite)
Theorem:
(defthm tree-listp-of-parse-*-alpha/digit/dash.trees (b* (((mv ?error? ?trees ?rest-input) (parse-*-alpha/digit/dash input))) (tree-listp trees)) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-parse-*-alpha/digit/dash.rest-input (b* (((mv ?error? ?trees ?rest-input) (parse-*-alpha/digit/dash input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-parse-*-alpha/digit/dash-linear (b* (((mv ?error? ?trees ?rest-input) (parse-*-alpha/digit/dash input))) (<= (len rest-input) (len input))) :rule-classes :linear)
Theorem:
(defthm parse-*-alpha/digit/dash-of-nat-list-fix-input (equal (parse-*-alpha/digit/dash (nat-list-fix input)) (parse-*-alpha/digit/dash input)))
Theorem:
(defthm parse-*-alpha/digit/dash-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv input input-equiv) (equal (parse-*-alpha/digit/dash input) (parse-*-alpha/digit/dash input-equiv))) :rule-classes :congruence)