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