(svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings) → constraints
Function:
(defun svtv-spec-fsm-constraints-for-alist (x stage namemap overridetype bindings) (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)))) (let ((__function__ 'svtv-spec-fsm-constraints-for-alist)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((unless (mbt (and (consp (car x)) (svar-p (caar x))))) (svtv-spec-fsm-constraints-for-alist (cdr x) stage namemap overridetype bindings)) ((cons var val) (car x)) (look (hons-get var (svtv-name-lhs-map-fix namemap))) ((unless look) (svtv-spec-fsm-constraints-for-alist (cdr x) stage namemap overridetype bindings)) (lhs (cdr look)) (lhprobe (make-lhprobe :lhs (lhs-change-override lhs overridetype) :stage stage :signedp (lhprobe-signedness-for-alist overridetype val)))) (append (svtv-spec-fsm-constraints-for-lhprobe lhprobe val bindings) (svtv-spec-fsm-constraints-for-alist (cdr x) stage namemap overridetype bindings)))))
Theorem:
(defthm lhprobe-constraintlist-p-of-svtv-spec-fsm-constraints-for-alist (b* ((constraints (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings))) (lhprobe-constraintlist-p constraints)) :rule-classes :rewrite)
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-of-svar/4vec-alist-fix-x (equal (svtv-spec-fsm-constraints-for-alist (svar/4vec-alist-fix x) stage namemap overridetype bindings) (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings)))
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-svar/4vec-alist-equiv-congruence-on-x (implies (svar/4vec-alist-equiv x x-equiv) (equal (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings) (svtv-spec-fsm-constraints-for-alist x-equiv stage namemap overridetype bindings))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-of-nfix-stage (equal (svtv-spec-fsm-constraints-for-alist x (nfix stage) namemap overridetype bindings) (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings)))
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-nat-equiv-congruence-on-stage (implies (nat-equiv stage stage-equiv) (equal (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings) (svtv-spec-fsm-constraints-for-alist x stage-equiv namemap overridetype bindings))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-of-svtv-name-lhs-map-fix-namemap (equal (svtv-spec-fsm-constraints-for-alist x stage (svtv-name-lhs-map-fix namemap) overridetype bindings) (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings)))
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-svtv-name-lhs-map-equiv-congruence-on-namemap (implies (svtv-name-lhs-map-equiv namemap namemap-equiv) (equal (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings) (svtv-spec-fsm-constraints-for-alist x stage namemap-equiv overridetype bindings))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-of-svar-overridetype-fix-overridetype (equal (svtv-spec-fsm-constraints-for-alist x stage namemap (svar-overridetype-fix overridetype) bindings) (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings)))
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-svar-overridetype-equiv-congruence-on-overridetype (implies (svar-overridetype-equiv overridetype overridetype-equiv) (equal (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings) (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype-equiv bindings))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-of-lhprobe-map-fix-bindings (equal (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype (lhprobe-map-fix bindings)) (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings)))
Theorem:
(defthm svtv-spec-fsm-constraints-for-alist-lhprobe-map-equiv-congruence-on-bindings (implies (lhprobe-map-equiv bindings bindings-equiv) (equal (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings) (svtv-spec-fsm-constraints-for-alist x stage namemap overridetype bindings-equiv))) :rule-classes :congruence)