(phys-mem-values-same addrs x86-1 x86-2) → *
Function:
(defun phys-mem-values-same (addrs x86-1 x86-2) (declare (xargs :non-executable t)) (declare (xargs :guard t)) (prog2$ (acl2::throw-nonexec-error 'phys-mem-values-same (list addrs x86-1 x86-2)) (let ((__function__ 'phys-mem-values-same)) (declare (ignorable __function__)) (if (atom addrs) t (and (equal (xr :mem (car addrs) x86-1) (xr :mem (car addrs) x86-2)) (phys-mem-values-same (cdr addrs) x86-1 x86-2))))))