Lift atj-gen-test-value to lists.
(atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$) → (mv block exprs types new-jvar-value-index)
Function:
(defun atj-gen-test-values (tvalues jvar-value-base jvar-value-index deep$ guards$) (declare (xargs :guard (and (atj-test-value-listp tvalues) (stringp jvar-value-base) (posp jvar-value-index) (booleanp deep$) (booleanp guards$)))) (let ((__function__ 'atj-gen-test-values)) (declare (ignorable __function__)) (b* (((when (endp tvalues)) (mv nil nil nil jvar-value-index)) ((mv first-block first-expr first-type jvar-value-index) (atj-gen-test-value (car tvalues) jvar-value-base jvar-value-index deep$ guards$)) ((mv rest-block rest-exprs rest-types jvar-value-index) (atj-gen-test-values (cdr tvalues) jvar-value-base jvar-value-index deep$ guards$))) (mv (append first-block rest-block) (cons first-expr rest-exprs) (cons first-type rest-types) jvar-value-index))))
Theorem:
(defthm jblockp-of-atj-gen-test-values.block (b* (((mv common-lisp::?block ?exprs ?types ?new-jvar-value-index) (atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexpr-listp-of-atj-gen-test-values.exprs (b* (((mv common-lisp::?block ?exprs ?types ?new-jvar-value-index) (atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$))) (jexpr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-listp-of-atj-gen-test-values.types (b* (((mv common-lisp::?block ?exprs ?types ?new-jvar-value-index) (atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$))) (atj-type-listp types)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atj-gen-test-values.new-jvar-value-index (implies (posp jvar-value-index) (b* (((mv common-lisp::?block ?exprs ?types ?new-jvar-value-index) (atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$))) (posp new-jvar-value-index))) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-gen-test-values.exprs (b* (((mv common-lisp::?block ?exprs ?types ?new-jvar-value-index) (atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$))) (equal (len exprs) (len tvalues))))
Theorem:
(defthm len-of-atj-gen-test-values.types (b* (((mv common-lisp::?block ?exprs ?types ?new-jvar-value-index) (atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$))) (equal (len types) (len tvalues))))
Theorem:
(defthm consp-of-atj-gen-test-values.exprs (b* (((mv common-lisp::?block ?exprs ?types ?new-jvar-value-index) (atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$))) (implies (consp tvalues) (consp exprs))) :rule-classes :type-prescription)
Theorem:
(defthm consp-of-atj-gen-test-values.types (b* (((mv common-lisp::?block ?exprs ?types ?new-jvar-value-index) (atj-gen-test-values tvalues jvar-value-base jvar-value-index deep$ guards$))) (implies (consp tvalues) (consp types))) :rule-classes :type-prescription)