		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

N64p-byte-alistp

Recognizer for a list of pairs of up to 64-bit wide linear address and byte.

Signature
(n64p-byte-alistp alst) → *

Definitions and Theorems

Function: n64p-byte-alistp

(defun n64p-byte-alistp (alst)
  (declare (xargs :guard t))
  (let ((__function__ 'n64p-byte-alistp))
    (declare (ignorable __function__))
    (if (atom alst)
        (equal alst nil)
      (if (atom (car alst))
          nil
        (let ((addr (caar alst))
              (byte (cdar alst))
              (rest (cdr alst)))
          (and (n64p addr)
               (n08p byte)
               (n64p-byte-alistp rest)))))))

Theorem: n64p-byte-alistp-fwd-chain-to-alistp

(defthm n64p-byte-alistp-fwd-chain-to-alistp
  (implies (n64p-byte-alistp alst)
           (alistp alst))
  :rule-classes :forward-chaining)