		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-rulename-info

Deftreeops-rulename-infop

Recognizer for deftreeops-rulename-info structures.

Signature
(deftreeops-rulename-infop x) → *

Definitions and Theorems

Function: deftreeops-rulename-infop

(defun deftreeops-rulename-infop (x)
 (declare (xargs :guard t))
 (let ((__function__ 'deftreeops-rulename-infop))
  (declare (ignorable __function__))
  (and
   (mbe
       :logic (and (alistp x)
                   (equal (strip-cars x)
                          '(alt nonleaf-thm rulename-thm
                                match-thm concs-thm conc-equivs-thm
                                alt-kind check-conc-fn conc-infos)))
       :exec (fty::alist-with-carsp
                  x
                  '(alt nonleaf-thm rulename-thm
                        match-thm concs-thm conc-equivs-thm
                        alt-kind check-conc-fn conc-infos)))
   (b* ((alt (cdr (std::da-nth 0 x)))
        (nonleaf-thm (cdr (std::da-nth 1 x)))
        (rulename-thm (cdr (std::da-nth 2 x)))
        (match-thm (cdr (std::da-nth 3 x)))
        (concs-thm (cdr (std::da-nth 4 x)))
        (conc-equivs-thm (cdr (std::da-nth 5 x)))
        (alt-kind (cdr (std::da-nth 6 x)))
        (check-conc-fn (cdr (std::da-nth 7 x)))
        (conc-infos (cdr (std::da-nth 8 x))))
     (and (alternationp alt)
          (common-lisp::symbolp nonleaf-thm)
          (common-lisp::symbolp rulename-thm)
          (common-lisp::symbolp match-thm)
          (common-lisp::symbolp concs-thm)
          (common-lisp::symbolp conc-equivs-thm)
          (natp alt-kind)
          (common-lisp::symbolp check-conc-fn)
          (deftreeops-conc-info-listp conc-infos))))))

Theorem: consp-when-deftreeops-rulename-infop

(defthm consp-when-deftreeops-rulename-infop
  (implies (deftreeops-rulename-infop x)
           (consp x))
  :rule-classes :compound-recognizer)