Parse an
(parse-affine-group-literal token input) → (mv tree next-token rest-input)
Function:
(defun parse-affine-group-literal (token input) (declare (xargs :guard (and (abnf::tree-optionp token) (abnf::tree-listp input)))) (let ((__function__ 'parse-affine-group-literal)) (declare (ignorable __function__)) (b* (((pok tree1) (parse-symbol "(" token input)) ((pok tree2) (parse-group-coordinate token input)) ((pok tree3) (parse-symbol "," token input)) ((pok tree4) (parse-group-coordinate token input)) ((pok tree5) (parse-symbol ")group" token input)) (tree (abnf::make-tree-nonleaf :rulename? (abnf::rulename "affine-group-literal") :branches (list (list tree1) (list tree2) (list tree3) (list tree4) (list tree5))))) (mv tree token input))))
Theorem:
(defthm tree-resultp-of-parse-affine-group-literal.tree (b* (((mv ?tree ?next-token ?rest-input) (parse-affine-group-literal token input))) (abnf::tree-resultp tree)) :rule-classes :rewrite)
Theorem:
(defthm tree-optionp-of-parse-affine-group-literal.next-token (b* (((mv ?tree ?next-token ?rest-input) (parse-affine-group-literal token input))) (abnf::tree-optionp next-token)) :rule-classes :rewrite)
Theorem:
(defthm tree-listp-of-parse-affine-group-literal.rest-input (b* (((mv ?tree ?next-token ?rest-input) (parse-affine-group-literal token input))) (abnf::tree-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-affine-group-literal-<= (b* (((mv ?tree ?next-token ?rest-input) (parse-affine-group-literal token input))) (<= (parsize next-token rest-input) (parsize token input))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-affine-group-literal-< (b* (((mv ?tree ?next-token ?rest-input) (parse-affine-group-literal token input))) (implies (not (reserrp tree)) (< (parsize next-token rest-input) (parsize token input)))) :rule-classes :linear)
Theorem:
(defthm parse-affine-group-literal-of-tree-option-fix-token (equal (parse-affine-group-literal (abnf::tree-option-fix token) input) (parse-affine-group-literal token input)))
Theorem:
(defthm parse-affine-group-literal-tree-option-equiv-congruence-on-token (implies (abnf::tree-option-equiv token token-equiv) (equal (parse-affine-group-literal token input) (parse-affine-group-literal token-equiv input))) :rule-classes :congruence)
Theorem:
(defthm parse-affine-group-literal-of-tree-list-fix-input (equal (parse-affine-group-literal token (abnf::tree-list-fix input)) (parse-affine-group-literal token input)))
Theorem:
(defthm parse-affine-group-literal-tree-list-equiv-congruence-on-input (implies (abnf::tree-list-equiv input input-equiv) (equal (parse-affine-group-literal token input) (parse-affine-group-literal token input-equiv))) :rule-classes :congruence)