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