(stv-fully-general-in-alists-aux n flat-ins acc) → in-alists
Function:
(defun stv-fully-general-in-alists-aux (n flat-ins acc) (declare (xargs :guard (and (natp n) (symbol-listp flat-ins)))) (let ((__function__ 'stv-fully-general-in-alists-aux)) (declare (ignorable __function__)) (let ((acc (cons (stv-fully-general-in-alist-n n flat-ins) acc))) (if (zp n) acc (stv-fully-general-in-alists-aux (- n 1) flat-ins acc)))))
Theorem:
(defthm cons-list-listp-of-stv-fully-general-in-alists-aux (implies (cons-list-listp acc) (b* ((in-alists (stv-fully-general-in-alists-aux n flat-ins acc))) (cons-list-listp in-alists))) :rule-classes :rewrite)
Theorem:
(defthm len-stv-fully-general-in-alists-aux (equal (len (stv-fully-general-in-alists-aux n flat-ins acc)) (+ 1 (nfix n) (len acc))))