		Search-engine friendly clone of the ACL2 documentation.

Tree-list-tuple10

Tree-list-tuple10p

Recognizer for tree-list-tuple10 structures.

Signature
(tree-list-tuple10p x) → *

Definitions and Theorems

Function: tree-list-tuple10p

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

Theorem: consp-when-tree-list-tuple10p

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