		Search-engine friendly clone of the ACL2 documentation.

Abnf::tree-list-tuple10

Abnf::tree-list-tuple10p

Recognizer for abnf::tree-list-tuple10 structures.

Signature
(abnf::tree-list-tuple10p abnf::x) → *

Definitions and Theorems

Function: tree-list-tuple10p

(defun abnf::tree-list-tuple10p (abnf::x)
 (declare (xargs :guard t))
 (let ((__function__ 'abnf::tree-list-tuple10p))
  (declare (ignorable __function__))
  (and
   (mbe
    :logic (and (alistp abnf::x)
                (equal (strip-cars abnf::x)
                       '(1st 2nd 3rd 4th 5th 6th 7th 8th 9th 10th)))
    :exec (fty::alist-with-carsp
               abnf::x
               '(1st 2nd 3rd 4th 5th 6th 7th 8th 9th 10th)))
   (b* ((1st (cdr (std::da-nth 0 abnf::x)))
        (2nd (cdr (std::da-nth 1 abnf::x)))
        (3rd (cdr (std::da-nth 2 abnf::x)))
        (4th (cdr (std::da-nth 3 abnf::x)))
        (5th (cdr (std::da-nth 4 abnf::x)))
        (6th (cdr (std::da-nth 5 abnf::x)))
        (7th (cdr (std::da-nth 6 abnf::x)))
        (8th (cdr (std::da-nth 7 abnf::x)))
        (9th (cdr (std::da-nth 8 abnf::x)))
        (10th (cdr (std::da-nth 9 abnf::x))))
     (and (abnf::tree-listp 1st)
          (abnf::tree-listp 2nd)
          (abnf::tree-listp 3rd)
          (abnf::tree-listp 4th)
          (abnf::tree-listp 5th)
          (abnf::tree-listp 6th)
          (abnf::tree-listp 7th)
          (abnf::tree-listp 8th)
          (abnf::tree-listp 9th)
          (abnf::tree-listp 10th))))))

Theorem: consp-when-tree-list-tuple10p

(defthm abnf::consp-when-tree-list-tuple10p
  (implies (abnf::tree-list-tuple10p abnf::x)
           (consp abnf::x))
  :rule-classes :compound-recognizer)