		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svtv-spec->in-alists*

Signature
(svtv-spec->in-alists* x) → *
Arguments: x — Guard (svtv-spec-p x).

Definitions and Theorems

Function: svtv-spec->in-alists*

(defun svtv-spec->in-alists* (x)
  (declare (xargs :guard (svtv-spec-p x)))
  (let ((__function__ 'svtv-spec->in-alists*))
    (declare (ignorable __function__))
    (b* (((svtv-spec x)))
      (take (len (svtv-probealist-outvars x.probes))
            x.in-alists))))

Theorem: svtv-spec->in-alists*-of-svtv-spec-fix-x

(defthm svtv-spec->in-alists*-of-svtv-spec-fix-x
  (equal (svtv-spec->in-alists* (svtv-spec-fix x))
         (svtv-spec->in-alists* x)))

Theorem: svtv-spec->in-alists*-svtv-spec-equiv-congruence-on-x

(defthm svtv-spec->in-alists*-svtv-spec-equiv-congruence-on-x
  (implies (svtv-spec-equiv x x-equiv)
           (equal (svtv-spec->in-alists* x)
                  (svtv-spec->in-alists* x-equiv)))
  :rule-classes :congruence)