		Search-engine friendly clone of the ACL2 documentation.

Sd-problem

Sd-problem-p

Recognizer for sd-problem structures.

Signature
(sd-problem-p x) → *

Definitions and Theorems

Function: sd-problem-p

(defun sd-problem-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'sd-problem-p))
    (declare (ignorable __function__))
    (and (consp x)
         (eq (car x) :sd-problem)
         (consp (cdr x))
         (consp (car (cdr x)))
         (consp (cdr (cdr x)))
         (consp (cdr (cdr (cdr x))))
         (b* ((type (car (car (cdr x))))
              (priority (cdr (car (cdr x))))
              (groupsize (car (cdr (cdr x))))
              (key (car (cdr (cdr (cdr x)))))
              (ctx (cdr (cdr (cdr (cdr x))))))
           (and (symbolp type)
                (natp priority)
                (natp groupsize)
                (sd-key-p key)
                (vl-context1-p ctx))))))

Theorem: consp-when-sd-problem-p

(defthm consp-when-sd-problem-p
  (implies (sd-problem-p x) (consp x))
  :rule-classes :compound-recognizer)