(svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc) → bindings
Function:
(defun svtv-spec-fsm-bindings-for-alist (x stage namemap overridetype bindings-acc) (declare (xargs :guard (and (svar/4vec-alist-p x) (natp stage) (svtv-name-lhs-map-p namemap) (svar-overridetype-p overridetype) (lhprobe-map-p bindings-acc)))) (let ((__function__ 'svtv-spec-fsm-bindings-for-alist)) (declare (ignorable __function__)) (b* (((when (atom x)) (lhprobe-map-fix bindings-acc)) ((unless (mbt (and (consp (car x)) (svar-p (caar x))))) (svtv-spec-fsm-bindings-for-alist (cdr x) stage namemap overridetype bindings-acc)) ((cons var val) (car x)) (look (hons-get var (svtv-name-lhs-map-fix namemap))) ((unless look) (svtv-spec-fsm-bindings-for-alist (cdr x) stage namemap overridetype bindings-acc)) (lhs (cdr look)) (lhprobe (make-lhprobe :lhs (lhs-change-override lhs overridetype) :stage stage :signedp (lhprobe-signedness-for-alist overridetype val))) (bindings-acc (svtv-spec-fsm-bindings-for-lhprobe lhprobe val bindings-acc))) (svtv-spec-fsm-bindings-for-alist (cdr x) stage namemap overridetype bindings-acc))))
Theorem:
(defthm lhprobe-map-p-of-svtv-spec-fsm-bindings-for-alist (b* ((bindings (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc))) (lhprobe-map-p bindings)) :rule-classes :rewrite)
Theorem:
(defthm lhprobe-map-max-stage-of-svtv-spec-fsm-bindings-for-alist (b* ((?bindings (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc))) (implies (and (<= (nfix stage) bound) (<= (lhprobe-map-max-stage bindings-acc) bound)) (<= (lhprobe-map-max-stage bindings) bound))))
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-of-svar/4vec-alist-fix-x (equal (svtv-spec-fsm-bindings-for-alist (svar/4vec-alist-fix x) stage namemap overridetype bindings-acc) (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc)))
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-svar/4vec-alist-equiv-congruence-on-x (implies (svar/4vec-alist-equiv x x-equiv) (equal (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc) (svtv-spec-fsm-bindings-for-alist x-equiv stage namemap overridetype bindings-acc))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-of-nfix-stage (equal (svtv-spec-fsm-bindings-for-alist x (nfix stage) namemap overridetype bindings-acc) (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc)))
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-nat-equiv-congruence-on-stage (implies (nat-equiv stage stage-equiv) (equal (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc) (svtv-spec-fsm-bindings-for-alist x stage-equiv namemap overridetype bindings-acc))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-of-svtv-name-lhs-map-fix-namemap (equal (svtv-spec-fsm-bindings-for-alist x stage (svtv-name-lhs-map-fix namemap) overridetype bindings-acc) (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc)))
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-svtv-name-lhs-map-equiv-congruence-on-namemap (implies (svtv-name-lhs-map-equiv namemap namemap-equiv) (equal (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc) (svtv-spec-fsm-bindings-for-alist x stage namemap-equiv overridetype bindings-acc))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-of-svar-overridetype-fix-overridetype (equal (svtv-spec-fsm-bindings-for-alist x stage namemap (svar-overridetype-fix overridetype) bindings-acc) (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc)))
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-svar-overridetype-equiv-congruence-on-overridetype (implies (svar-overridetype-equiv overridetype overridetype-equiv) (equal (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc) (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype-equiv bindings-acc))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-of-lhprobe-map-fix-bindings-acc (equal (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype (lhprobe-map-fix bindings-acc)) (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc)))
Theorem:
(defthm svtv-spec-fsm-bindings-for-alist-lhprobe-map-equiv-congruence-on-bindings-acc (implies (lhprobe-map-equiv bindings-acc bindings-acc-equiv) (equal (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc) (svtv-spec-fsm-bindings-for-alist x stage namemap overridetype bindings-acc-equiv))) :rule-classes :congruence)