Lift atj-process-test-input-jprim-value to lists.
(atj-process-test-input-jprim-values inputs type fn call ctx state) → (mv erp values state)
Function:
(defun atj-process-test-input-jprim-values (inputs type fn call ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-term-listp inputs) (primitive-typep type) (symbolp fn) (pseudo-termp call) (ctxp ctx)))) (let ((__function__ 'atj-process-test-input-jprim-values)) (declare (ignorable __function__)) (b* (((when (endp inputs)) (value nil)) ((cons input inputs) inputs) ((mv erp value state) (atj-process-test-input-jprim-value input type fn call ctx state)) ((when erp) (mv erp nil state)) ((er values) (atj-process-test-input-jprim-values inputs type fn call ctx state))) (value (cons value values)))))
Theorem:
(defthm boolean-value-listp-of-atj-process-test-input-jprim-values.values (implies (primitive-type-case type :boolean) (b* (((mv ?erp ?values acl2::?state) (atj-process-test-input-jprim-values inputs type fn call ctx state))) (boolean-value-listp values))) :rule-classes :rewrite)
Theorem:
(defthm char-value-listp-of-atj-process-test-input-jprim-values.values (implies (primitive-type-case type :char) (b* (((mv ?erp ?values acl2::?state) (atj-process-test-input-jprim-values inputs type fn call ctx state))) (char-value-listp values))) :rule-classes :rewrite)
Theorem:
(defthm byte-value-listp-of-atj-process-test-input-jprim-values.values (implies (primitive-type-case type :byte) (b* (((mv ?erp ?values acl2::?state) (atj-process-test-input-jprim-values inputs type fn call ctx state))) (byte-value-listp values))) :rule-classes :rewrite)
Theorem:
(defthm short-value-listp-of-atj-process-test-input-jprim-values.values (implies (primitive-type-case type :short) (b* (((mv ?erp ?values acl2::?state) (atj-process-test-input-jprim-values inputs type fn call ctx state))) (short-value-listp values))) :rule-classes :rewrite)
Theorem:
(defthm int-value-listp-of-atj-process-test-input-jprim-values.values (implies (primitive-type-case type :int) (b* (((mv ?erp ?values acl2::?state) (atj-process-test-input-jprim-values inputs type fn call ctx state))) (int-value-listp values))) :rule-classes :rewrite)
Theorem:
(defthm long-value-listp-of-atj-process-test-input-jprim-values.values (implies (primitive-type-case type :long) (b* (((mv ?erp ?values acl2::?state) (atj-process-test-input-jprim-values inputs type fn call ctx state))) (long-value-listp values))) :rule-classes :rewrite)