(svtv-spec-fsm-bindings x) → bindings
Function:
(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:
(defthm lhprobe-map-p-of-svtv-spec-fsm-bindings (b* ((bindings (svtv-spec-fsm-bindings x))) (lhprobe-map-p bindings)) :rule-classes :rewrite)
Theorem:
(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:
(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:
(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)