		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-list-list-9

Check if a list of lists of ABNF trees consists of nine lists of subtrees, returning those lists of subtrees if successful.

Signature
(check-tree-list-list-9 treess) → sub
Arguments: treess — Guard (tree-list-listp treess).
Returns: sub — Type (tree-list-tuple9-resultp sub).

Definitions and Theorems

Function: check-tree-list-list-9

(defun check-tree-list-list-9 (treess)
  (declare (xargs :guard (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)))))
        (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: tree-list-tuple9-resultp-of-check-tree-list-list-9

(defthm tree-list-tuple9-resultp-of-check-tree-list-list-9
  (b* ((sub (check-tree-list-list-9 treess)))
    (tree-list-tuple9-resultp sub))
  :rule-classes :rewrite)

Theorem: tree-count-of-check-tree-list-list-9

(defthm tree-count-of-check-tree-list-list-9
  (b* ((?sub (check-tree-list-list-9 treess)))
    (implies (not (reserrp sub))
             (and (< (tree-list-count (tree-list-tuple9->1st sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple9->2nd sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple9->3rd sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple9->4th sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple9->5th sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple9->6th sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple9->7th sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple9->8th sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple9->9th sub))
                     (tree-list-list-count treess)))))
  :rule-classes :linear)

Theorem: check-tree-list-list-9-of-tree-list-list-fix-treess

(defthm check-tree-list-list-9-of-tree-list-list-fix-treess
  (equal (check-tree-list-list-9 (tree-list-list-fix treess))
         (check-tree-list-list-9 treess)))

Theorem: check-tree-list-list-9-tree-list-list-equiv-congruence-on-treess

(defthm
   check-tree-list-list-9-tree-list-list-equiv-congruence-on-treess
  (implies (tree-list-list-equiv treess treess-equiv)
           (equal (check-tree-list-list-9 treess)
                  (check-tree-list-list-9 treess-equiv)))
  :rule-classes :congruence)