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