Check if a list of ABNF trees consists of one subtree, returning that subtree if successful.
(check-tree-list-1 trees) → sub
Function:
(defun check-tree-list-1 (trees) (declare (xargs :guard (abnf::tree-listp trees))) (let ((__function__ 'check-tree-list-1)) (declare (ignorable __function__)) (if (and (consp trees) (endp (cdr trees))) (abnf::tree-fix (car trees)) (reserrf (list :found (len trees))))))
Theorem:
(defthm tree-resultp-of-check-tree-list-1 (b* ((sub (check-tree-list-1 trees))) (abnf::tree-resultp sub)) :rule-classes :rewrite)
Theorem:
(defthm tree-count-of-check-tree-list-1 (b* ((?sub (check-tree-list-1 trees))) (implies (not (reserrp sub)) (< (abnf::tree-count sub) (abnf::tree-list-count trees)))) :rule-classes :linear)
Theorem:
(defthm check-tree-list-1-of-tree-list-fix-trees (equal (check-tree-list-1 (abnf::tree-list-fix trees)) (check-tree-list-1 trees)))
Theorem:
(defthm check-tree-list-1-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv trees trees-equiv) (equal (check-tree-list-1 trees) (check-tree-list-1 trees-equiv))) :rule-classes :congruence)