		Search-engine friendly clone of the ACL2 documentation.

Svtv-cyclephase

Svtv-cyclephase-p

Recognizer for svtv-cyclephase structures.

Signature
(svtv-cyclephase-p x) → *

Definitions and Theorems

Function: svtv-cyclephase-p

(defun svtv-cyclephase-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'svtv-cyclephase-p))
    (declare (ignorable __function__))
    (and (consp x)
         (consp (cdr x))
         (b* ((constants (car x))
              (inputs-free (car (cdr x)))
              (outputs-captured (cdr (cdr x))))
           (and (svex-env-p constants)
                (booleanp inputs-free)
                (booleanp outputs-captured))))))

Theorem: consp-when-svtv-cyclephase-p

(defthm consp-when-svtv-cyclephase-p
  (implies (svtv-cyclephase-p x)
           (consp x))
  :rule-classes :compound-recognizer)