		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svtv-spec-fsm-bindings

Signature
(svtv-spec-fsm-bindings x) → bindings
Arguments: x — Guard (svtv-spec-p x).
Returns: bindings — Type (lhprobe-map-p bindings).

Definitions and Theorems

Function: svtv-spec-fsm-bindings

(defun svtv-spec-fsm-bindings (x)
 (declare (xargs :guard (svtv-spec-p x)))
 (declare (xargs :guard (svtv-spec-fsm-syntax-check x)))
 (let ((__function__ 'svtv-spec-fsm-bindings))
   (declare (ignorable __function__))
   (b*
     (((svtv-spec x))
      (len (len (svtv-probealist-outvars (svtv-spec->probes x))))
      ((with-fast x.namemap))
      (bindings
           (svtv-spec-fsm-bindings-for-alists (take len x.in-alists)
                                              0 x.namemap nil nil))
      (bindings (svtv-spec-fsm-bindings-for-alists
                     (take len x.override-val-alists)
                     0 x.namemap
                     :val bindings)))
     (svtv-spec-fsm-bindings-for-alists
          (take len x.override-test-alists)
          0 x.namemap
          :test bindings))))

Theorem: lhprobe-map-p-of-svtv-spec-fsm-bindings

(defthm lhprobe-map-p-of-svtv-spec-fsm-bindings
  (b* ((bindings (svtv-spec-fsm-bindings x)))
    (lhprobe-map-p bindings))
  :rule-classes :rewrite)

Theorem: lhprobe-map-max-stage-of-svtv-spec-fsm-bindings

(defthm lhprobe-map-max-stage-of-svtv-spec-fsm-bindings
  (b* ((?bindings (svtv-spec-fsm-bindings x)))
    (<= (lhprobe-map-max-stage bindings)
        (1- (len (svtv-probealist-outvars (svtv-spec->probes x))))))
  :rule-classes
  ((:linear :trigger-terms
            ((lhprobe-map-max-stage (svtv-spec-fsm-bindings x))))))

Theorem: svtv-spec-fsm-bindings-of-svtv-spec-fix-x

(defthm svtv-spec-fsm-bindings-of-svtv-spec-fix-x
  (equal (svtv-spec-fsm-bindings (svtv-spec-fix x))
         (svtv-spec-fsm-bindings x)))

Theorem: svtv-spec-fsm-bindings-svtv-spec-equiv-congruence-on-x

(defthm svtv-spec-fsm-bindings-svtv-spec-equiv-congruence-on-x
  (implies (svtv-spec-equiv x x-equiv)
           (equal (svtv-spec-fsm-bindings x)
                  (svtv-spec-fsm-bindings x-equiv)))
  :rule-classes :congruence)