Lex
(lex-1*-digit input) → (mv trees rest-input)
Function:
(defun lex-1*-digit (input) (declare (xargs :guard (nat-listp input))) (let ((__function__ 'lex-1*-digit)) (declare (ignorable __function__)) (b* (((mv tree-thing1 input-after-thing1) (lex-digit input)) ((when (reserrp tree-thing1)) (mv (reserrf-push tree-thing1) (nat-list-fix input))) ((mv trees input-after-trees) (lex-*-digit input-after-thing1))) (mv (cons tree-thing1 trees) input-after-trees))))
Theorem:
(defthm tree-list-resultp-of-lex-1*-digit.trees (b* (((mv ?trees ?rest-input) (lex-1*-digit input))) (abnf::tree-list-resultp trees)) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-lex-1*-digit.rest-input (b* (((mv ?trees ?rest-input) (lex-1*-digit input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-lex-1*-digit-<= (b* (((mv ?trees ?rest-input) (lex-1*-digit input))) (<= (len rest-input) (len input))) :rule-classes :linear)
Theorem:
(defthm len-of-lex-1*-digit-< (b* (((mv ?trees ?rest-input) (lex-1*-digit input))) (implies (not (reserrp trees)) (< (len rest-input) (len input)))) :rule-classes :linear)
Theorem:
(defthm lex-1*-digit-of-nat-list-fix-input (equal (lex-1*-digit (nat-list-fix input)) (lex-1*-digit input)))
Theorem:
(defthm lex-1*-digit-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv input input-equiv) (equal (lex-1*-digit input) (lex-1*-digit input-equiv))) :rule-classes :congruence)