Create the sexpr-alists to use as the inputs for each phase of fully general simulations of a module.
This is basically name mangling. For instance, at phase 5 the
(defun stv-fully-general-in-alists (n mod) (declare (xargs :guard (posp n))) (let ((__function__ 'stv-fully-general-in-alists)) (declare (ignorable __function__)) (b* ((ins (gpl :i mod)) (flat-ins (pat-flatten1 ins)) ((when (mbe :logic (not (posp n)) :exec nil)) nil) ((unless (symbol-listp flat-ins)) (raise "Expected :i for ~x0 to be a symbol pattern." (gpl :n mod)) (ec-call (stv-fully-general-in-alists-aux (- n 1) flat-ins nil)))) (stv-fully-general-in-alists-aux (- n 1) flat-ins nil))))
(defthm cons-list-listp-of-stv-fully-general-in-alists (b* ((in-alists (stv-fully-general-in-alists n mod))) (cons-list-listp in-alists)) :rule-classes :rewrite)
(defthm len-stv-fully-general-in-alists (equal (len (stv-fully-general-in-alists n mod)) (nfix n)))