Phys-mem-values-same
- Signature
(phys-mem-values-same addrs x86-1 x86-2) → *
Definitions and Theorems
Function: phys-mem-values-same
(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))))))
