(svtv-phase-var-assigns x phase) → assigns
Function:
(defun svtv-phase-var-assigns (x phase) (declare (xargs :guard (and (svarlist-p x) (natp phase)))) (let ((__function__ 'svtv-phase-var-assigns)) (declare (ignorable __function__)) (if (atom x) nil (cons (let ((v (svar-fix (car x)))) (cons v (svex-var (svex-phase-var v phase)))) (svtv-phase-var-assigns (cdr x) phase)))))
Theorem:
(defthm svex-alist-p-of-svtv-phase-var-assigns (b* ((assigns (svtv-phase-var-assigns x phase))) (svex-alist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm svtv-phase-var-assigns-of-svarlist-fix-x (equal (svtv-phase-var-assigns (svarlist-fix x) phase) (svtv-phase-var-assigns x phase)))
Theorem:
(defthm svtv-phase-var-assigns-svarlist-equiv-congruence-on-x (implies (svarlist-equiv x x-equiv) (equal (svtv-phase-var-assigns x phase) (svtv-phase-var-assigns x-equiv phase))) :rule-classes :congruence)
Theorem:
(defthm svtv-phase-var-assigns-of-nfix-phase (equal (svtv-phase-var-assigns x (nfix phase)) (svtv-phase-var-assigns x phase)))
Theorem:
(defthm svtv-phase-var-assigns-nat-equiv-congruence-on-phase (implies (nat-equiv phase phase-equiv) (equal (svtv-phase-var-assigns x phase) (svtv-phase-var-assigns x phase-equiv))) :rule-classes :congruence)