Recognizer for ex-outs structures.
(ex-outs-p x) → *
Function:
(defun ex-outs-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'ex-outs-p)) (declare (ignorable acl2::__function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(expanded-term-lst expanded-fn-lst))) :exec (fty::alist-with-carsp x '(expanded-term-lst expanded-fn-lst))) (b* ((expanded-term-lst (cdr (std::da-nth 0 x))) (expanded-fn-lst (cdr (std::da-nth 1 x)))) (and (pseudo-term-listp expanded-term-lst) (pseudo-term-alistp expanded-fn-lst))))))
Theorem:
(defthm consp-when-ex-outs-p (implies (ex-outs-p x) (consp x)) :rule-classes :compound-recognizer)