Recognizer for phase-fsm-params structures.
(phase-fsm-params-p x) → *
Function:
(defun phase-fsm-params-p (x) (declare (xargs :guard t)) (let ((__function__ 'phase-fsm-params-p)) (declare (ignorable __function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(scc-selfcompose-limit rewrite))) :exec (fty::alist-with-carsp x '(scc-selfcompose-limit rewrite))) (b* ((scc-selfcompose-limit (cdr (std::da-nth 0 x))) (rewrite (cdr (std::da-nth 1 x)))) (and (maybe-natp scc-selfcompose-limit) (booleanp rewrite))))))
Theorem:
(defthm consp-when-phase-fsm-params-p (implies (phase-fsm-params-p x) (consp x)) :rule-classes :compound-recognizer)