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