Parse a
(lex-optional-sequence-of-2hex-digits abnf::input) → (mv abnf::tree abnf::rest-input)
Function:
(defun lex-optional-sequence-of-2hex-digits (abnf::input) (declare (xargs :guard (nat-listp abnf::input))) (let ((__function__ 'lex-optional-sequence-of-2hex-digits)) (declare (ignorable __function__)) (b* (((mv abnf::treess abnf::input) (b* (((mv abnf::treess1 abnf::input1) (b* (((mv abnf::trees1 abnf::input) (lex-repetition-2-hex-digits abnf::input)) ((when (reserrp abnf::trees1)) (mv (fty::reserrf-push abnf::trees1) abnf::input)) ((mv abnf::trees2 abnf::input) (lex-repetition-*-optional-underbar-and-two-hex-digits abnf::input)) ((when (reserrp abnf::trees2)) (mv (fty::reserrf-push abnf::trees2) abnf::input)) (abnf::treess (list abnf::trees1 abnf::trees2))) (mv abnf::treess abnf::input))) ((when (not (reserrp abnf::treess1))) (mv abnf::treess1 abnf::input1))) (mv (reserrf (list :found (list abnf::treess1) :required '(((:repetition (:repeat 2 (:finite 2)) (:rulename (:rulename "hex-digit"))) (:repetition (:repeat 0 (:infinity)) (:group (((:repetition (:repeat 1 (:finite 1)) (:option (((:repetition (:repeat 1 (:finite 1)) (:char-val (:insensitive nil "_"))))))) (:repetition (:repeat 2 (:finite 2)) (:rulename (:rulename "hex-digit"))))))))))) abnf::input))) ((when (reserrp abnf::treess)) (mv (abnf::make-tree-nonleaf :rulename? nil :branches nil) (acl2::nat-list-fix abnf::input)))) (mv (abnf::make-tree-nonleaf :rulename? nil :branches abnf::treess) abnf::input))))
Theorem:
(defthm tree-resultp-of-lex-optional-sequence-of-2hex-digits.tree (b* (((mv abnf::?tree abnf::?rest-input) (lex-optional-sequence-of-2hex-digits abnf::input))) (abnf::tree-resultp abnf::tree)) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-lex-optional-sequence-of-2hex-digits.rest-input (b* (((mv abnf::?tree abnf::?rest-input) (lex-optional-sequence-of-2hex-digits abnf::input))) (nat-listp abnf::rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-lex-optional-sequence-of-2hex-digits-<= (b* (((mv abnf::?tree abnf::?rest-input) (lex-optional-sequence-of-2hex-digits abnf::input))) (<= (len abnf::rest-input) (len abnf::input))) :rule-classes :linear)
Theorem:
(defthm lex-optional-sequence-of-2hex-digits-of-nat-list-fix-input (equal (lex-optional-sequence-of-2hex-digits (acl2::nat-list-fix abnf::input)) (lex-optional-sequence-of-2hex-digits abnf::input)))
Theorem:
(defthm lex-optional-sequence-of-2hex-digits-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv abnf::input input-equiv) (equal (lex-optional-sequence-of-2hex-digits abnf::input) (lex-optional-sequence-of-2hex-digits input-equiv))) :rule-classes :congruence)