(stv-fully-general-in-alist-n n flat-ins) → nth-alist
We memoize this to ensure that we'll get the same fully general alist across different STVs that target the same module for the same numbers of steps.
Function:
(defun stv-fully-general-in-alist-n (n flat-ins) (declare (xargs :guard (and (natp n) (symbol-listp flat-ins)))) (let ((__function__ 'stv-fully-general-in-alist-n)) (declare (ignorable __function__)) (pairlis$ flat-ins (stv-suffix-signals flat-ins (str::cat ".P" (str::natstr n))))))
Theorem:
(defthm cons-listp-of-stv-fully-general-in-alist-n (b* ((nth-alist (stv-fully-general-in-alist-n n flat-ins))) (cons-listp nth-alist)) :rule-classes :rewrite)