(stv-restrict-alist-aux name phase entries acc) → acc
Function:
(defun stv-restrict-alist-aux (name phase entries acc) (declare (xargs :guard (and (atom-listp name) (natp phase)))) (let ((__function__ 'stv-restrict-alist-aux)) (declare (ignorable __function__)) (b* (((when (atom entries)) acc) (name-at-phase (stv-suffix-signals name (str::cat ".P" (str::natstr phase)))) (val-at-phase (car entries)) (acc (safe-pairlis-onto-acc name-at-phase val-at-phase acc))) (stv-restrict-alist-aux name (+ 1 phase) (cdr entries) acc))))
Theorem:
(defthm alistp-of-stv-restrict-alist-aux (implies (alistp acc) (b* ((acc (stv-restrict-alist-aux name phase entries acc))) (alistp acc))) :rule-classes :rewrite)