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