		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

!ctri-from-alist

Update control registers as dictated by ctr-alist, which is required to be a ctri-alistp.

Signature
(!ctri-from-alist ctr-alist x86) → x86

Definitions and Theorems

Function: !ctri-from-alist

(defun !ctri-from-alist (ctr-alist x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (ctri-alistp ctr-alist)))
  (let ((__function__ '!ctri-from-alist))
    (declare (ignorable __function__))
    (cond ((endp ctr-alist) x86)
          (t (let ((x86 (!ctri (caar ctr-alist)
                               (cdar ctr-alist)
                               x86)))
               (!ctri-from-alist (cdr ctr-alist)
                                 x86))))))

Theorem: x86p-!ctri-from-alist

(defthm x86p-!ctri-from-alist
  (implies (and (ctri-alistp ctr-alist) (x86p x86))
           (x86p (!ctri-from-alist ctr-alist x86))))