(solve-gen-old-if-new-thm-aux vars index old-witness) → instantiation
Function:
(defun solve-gen-old-if-new-thm-aux (vars index old-witness) (declare (xargs :guard (and (symbol-listp vars) (natp index) (symbolp old-witness)))) (let ((__function__ 'solve-gen-old-if-new-thm-aux)) (declare (ignorable __function__)) (cond ((endp vars) nil) (t (cons (cons (car vars) (cons (cons 'mv-nth (cons index (cons (cons old-witness 'nil) 'nil))) 'nil)) (solve-gen-old-if-new-thm-aux (cdr vars) (1+ index) old-witness))))))
Theorem:
(defthm doublet-listp-of-solve-gen-old-if-new-thm-aux (b* ((instantiation (solve-gen-old-if-new-thm-aux vars index old-witness))) (doublet-listp instantiation)) :rule-classes :rewrite)