Lift atj-test-value-of-type to lists.
(atj-test-values-of-types values types) → test-values
Function:
(defun atj-test-values-of-types (values types) (declare (xargs :guard (and (true-listp values) (atj-type-listp types)))) (declare (xargs :guard (= (len values) (len types)))) (let ((__function__ 'atj-test-values-of-types)) (declare (ignorable __function__)) (cond ((endp values) nil) (t (cons (atj-test-value-of-type (car values) (car types)) (atj-test-values-of-types (cdr values) (cdr types)))))))
Theorem:
(defthm atj-test-value-listp-of-atj-test-values-of-types (b* ((test-values (atj-test-values-of-types values types))) (atj-test-value-listp test-values)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-test-values-of-types (b* ((?test-values (atj-test-values-of-types values types))) (equal (len test-values) (len values))))
Theorem:
(defthm atj-test-values-of-types-of-list-fix-values (equal (atj-test-values-of-types (list-fix values) types) (atj-test-values-of-types values types)))
Theorem:
(defthm atj-test-values-of-types-list-equiv-congruence-on-values (implies (list-equiv values values-equiv) (equal (atj-test-values-of-types values types) (atj-test-values-of-types values-equiv types))) :rule-classes :congruence)
Theorem:
(defthm atj-test-values-of-types-of-atj-type-list-fix-types (equal (atj-test-values-of-types values (atj-type-list-fix types)) (atj-test-values-of-types values types)))
Theorem:
(defthm atj-test-values-of-types-atj-type-list-equiv-congruence-on-types (implies (atj-type-list-equiv types types-equiv) (equal (atj-test-values-of-types values types) (atj-test-values-of-types values types-equiv))) :rule-classes :congruence)