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