Generate a ACL2::4v-res expression to resolve a list of emodwires.
(vl-make-res-sexpr args) generates a
Note that the RES operation is commutative and associative, so any nest of RES operations is equivalent. So, we just resolve the arguments in a straightforward, right-associative manner.
Function:
(defun vl-make-res-sexpr (args) (declare (xargs :guard (vl-emodwirelist-p args))) (cond ((atom args) acl2::*4vz-sexpr*) ((atom (cdr args)) (car args)) (t (acl2::hons-list 'acl2::res (car args) (vl-make-res-sexpr (cdr args))))))
Theorem:
(defthm 4v-sexpr-vars-of-vl-make-res-sexpr (implies (force (vl-emodwirelist-p args)) (equal (acl2::4v-sexpr-vars (vl-make-res-sexpr args)) (mergesort args))))