Parse a
(lex-*-rest-of-identifier abnf::input) → (mv abnf::trees abnf::rest-input)
Function:
(defun lex-*-rest-of-identifier (abnf::input) (declare (xargs :guard (nat-listp abnf::input))) (let ((__function__ 'lex-*-rest-of-identifier)) (declare (ignorable __function__)) (b* (((mv abnf::tree abnf::input) (lex-group-letter/digit/_ abnf::input)) ((when (reserrp abnf::tree)) (mv nil abnf::input)) ((mv abnf::trees abnf::input) (lex-*-rest-of-identifier abnf::input))) (mv (cons abnf::tree abnf::trees) abnf::input))))
Theorem:
(defthm tree-listp-of-lex-*-rest-of-identifier.trees (b* (((mv abnf::?trees abnf::?rest-input) (lex-*-rest-of-identifier abnf::input))) (abnf::tree-listp abnf::trees)) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-lex-*-rest-of-identifier.rest-input (b* (((mv abnf::?trees abnf::?rest-input) (lex-*-rest-of-identifier abnf::input))) (nat-listp abnf::rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-lex-*-rest-of-identifier (b* (((mv abnf::?trees abnf::?rest-input) (lex-*-rest-of-identifier abnf::input))) (<= (len abnf::rest-input) (len abnf::input))) :rule-classes :linear)
Theorem:
(defthm lex-*-rest-of-identifier-of-nat-list-fix-input (equal (lex-*-rest-of-identifier (nat-list-fix abnf::input)) (lex-*-rest-of-identifier abnf::input)))
Theorem:
(defthm lex-*-rest-of-identifier-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv abnf::input input-equiv) (equal (lex-*-rest-of-identifier abnf::input) (lex-*-rest-of-identifier input-equiv))) :rule-classes :congruence)