		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-list-list-3

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

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

Definitions and Theorems

Function: check-tree-list-list-3

(defun check-tree-list-list-3 (treess)
  (declare (xargs :guard (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)))
        (tree-list-tuple3 (car treess)
                          (cadr treess)
                          (caddr treess))
      (reserrf (list :found (len treess))))))

Theorem: tree-list-tuple3-resultp-of-check-tree-list-list-3

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

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

(defthm tree-count-of-check-tree-list-list-3
  (b* ((?sub (check-tree-list-list-3 treess)))
    (implies (not (reserrp sub))
             (and (< (tree-list-count (tree-list-tuple3->1st sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple3->2nd sub))
                     (tree-list-list-count treess))
                  (< (tree-list-count (tree-list-tuple3->3rd sub))
                     (tree-list-list-count treess)))))
  :rule-classes :linear)

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

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

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

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