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