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