• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Introduction
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
        • Implemented-opcodes
        • Proof-utilities
          • System-level-marking-view-proof-utilities
            • Rb-alt
            • Unwind-x86-interpreter-in-marking-view
            • Get-prefixes-alt
              • Get-prefixes-in-system-level-marking-view
              • Program-at-alt
              • Rb-in-system-level-marking-view
              • Xlate-equiv-memory-and-rml08
              • Reasoning-about-page-tables
              • Las-to-pas-two-n-ind-hint
              • Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
              • Replace-element
            • Non-marking-view-proof-utilities
            • App-view-proof-utilities
            • Subset-p
            • Disjoint-p
            • Pos
            • Member-p
            • No-duplicates-p
            • Common-system-level-utils
            • Debugging-code-proofs
            • General-memory-utils
            • X86-row-wow-thms
          • To-do
          • Concrete-simulation-examples
          • Model-validation
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • System-level-marking-view-proof-utilities

    Get-prefixes-alt

    Rewriting get-prefixes to get-prefixes-alt

    Signature
    (get-prefixes-alt start-rip prefixes rex-byte cnt x86) → *

    The following is not a theorem, which is why we can not define congruence rules about get-prefixes and xlate-equiv-memory directly.

    (implies 
 (xlate-equiv-memory x86-1 x86-2) 
 (equal (mv-nth 0 (get-prefixes 
                   *64-bit-mode* start-rip prefixes rex-byte cnt x86-1)) 
        (mv-nth 0 (get-prefixes 
                   *64-bit-mode* start-rip prefixes rex-byte cnt x86-2))))

    The above would be a theorem if the following pre-conditions held about both x86-1 and x86-2:

    (and (marking-view x86) 
     (not (app-view x86)) 
     (canonical-address-p start-rip) 
     (disjoint-p 
      (mv-nth 1 (las-to-pas cnt start-rip :x x86)) 
      (open-qword-paddr-list 
       (gather-all-paging-structure-qword-addresses x86))) 
     (not (mv-nth 0 (las-to-pas cnt start-rip :x x86))))

    Since 'conditional' congruence rules can't be defined, we define an alternative version of get-prefixes, called get-prefixes-alt, which is equal to get-prefixes if these pre-conditions hold, and if not, it returns benign values. We prove a rewrite rule that rewrites get-prefixes to get-prefixes-alt when applicable, and then we can prove congruence rules about get-prefixes-alt and xlate-equiv-memory. Note that this approach will be most successful if we expect these pre-conditions to hold all the time.

    A drawback of this approach to have 'conditional' congruence-based rules is that all the theorems I have about get-prefixes now have to be re-proved in terms of get-prefixes-alt.

    Definitions and Theorems

    Function: get-prefixes-alt

    (defun get-prefixes-alt (start-rip prefixes rex-byte cnt x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (signed-byte 48) start-rip)
          (type (unsigned-byte 52) prefixes)
          (type (unsigned-byte 8) rex-byte)
          (type (integer 0 15) cnt))
 (declare
      (xargs :guard (and (canonical-address-p (+ -1 cnt start-rip))
                         (not (app-view x86))
                         (marking-view x86))
             :non-executable t))
 (prog2$
  (acl2::throw-nonexec-error
       'get-prefixes-alt
       (list start-rip prefixes rex-byte cnt x86))
  (let ((__function__ 'get-prefixes-alt))
   (declare (ignorable __function__))
   (if
    (and
       (marking-view x86)
       (64-bit-modep x86)
       (not (app-view x86))
       (canonical-address-p start-rip)
       (disjoint-p
            (mv-nth 1 (las-to-pas cnt start-rip :x x86))
            (open-qword-paddr-list
                 (gather-all-paging-structure-qword-addresses x86)))
       (not (mv-nth 0 (las-to-pas cnt start-rip :x x86))))
    (get-prefixes 0 start-rip prefixes rex-byte cnt x86)
    (mv nil prefixes rex-byte x86)))))

    Theorem: natp-get-prefixes-alt.new-prefixes

    (defthm natp-get-prefixes-alt.new-prefixes
 (implies
  (forced-and (natp prefixes)
              (canonical-address-p start-rip)
              (x86p x86))
  (natp
   (mv-nth 1
           (get-prefixes-alt start-rip prefixes rex-byte cnt x86))))
 :rule-classes :type-prescription)

    Theorem: natp-get-prefixes-alt.new-rex-byte

    (defthm natp-get-prefixes-alt.new-rex-byte
 (implies
  (forced-and (natp rex-byte)
              (natp prefixes)
              (x86p x86))
  (natp
   (mv-nth 2
           (get-prefixes-alt start-rip prefixes rex-byte cnt x86))))
 :rule-classes :type-prescription)

    Theorem: prefixes-width-p-of-get-prefixes.new-prefixes-alt

    (defthm prefixes-width-p-of-get-prefixes.new-prefixes-alt
 (implies
  (and (unsigned-byte-p 52 prefixes)
       (x86p x86))
  (unsigned-byte-p
   52
   (mv-nth 1
           (get-prefixes-alt start-rip prefixes rex-byte cnt x86))))
 :rule-classes
 (:rewrite
  (:linear
   :corollary
   (implies
    (and (unsigned-byte-p 52 prefixes)
         (x86p x86))
    (and
     (<=
       0
       (mv-nth
            1
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
     (< (mv-nth
             1
             (get-prefixes-alt start-rip prefixes rex-byte cnt x86))
        4503599627370496)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

    Theorem: byte-p-of-get-prefixes.new-rex-byte-alt

    (defthm byte-p-of-get-prefixes.new-rex-byte-alt
 (implies
  (and (unsigned-byte-p 8 rex-byte)
       (natp prefixes)
       (x86p x86))
  (unsigned-byte-p
   8
   (mv-nth 2
           (get-prefixes-alt start-rip prefixes rex-byte cnt x86))))
 :rule-classes
 (:rewrite
  (:linear
   :corollary
   (implies
    (and (unsigned-byte-p 8 rex-byte)
         (natp prefixes)
         (x86p x86))
    (and
     (<=
       0
       (mv-nth
            2
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
     (< (mv-nth
             2
             (get-prefixes-alt start-rip prefixes rex-byte cnt x86))
        256)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

    Theorem: x86p-get-prefixes-alt

    (defthm x86p-get-prefixes-alt
 (implies
  (force (x86p x86))
  (x86p
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: xr-doc-mv-nth-3-get-prefixes-alt

    (defthm xr-doc-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :doc index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :doc index x86)))

    Theorem: xr-ms-mv-nth-3-get-prefixes-alt

    (defthm xr-ms-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :ms index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :ms index x86)))

    Theorem: xr-env-mv-nth-3-get-prefixes-alt

    (defthm xr-env-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :env index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :env index x86)))

    Theorem: xr-undef-mv-nth-3-get-prefixes-alt

    (defthm xr-undef-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :undef index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :undef index x86)))

    Theorem: xr-app-view-mv-nth-3-get-prefixes-alt

    (defthm xr-app-view-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :app-view index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :app-view index x86)))

    Theorem: xr-marking-view-mv-nth-3-get-prefixes-alt

    (defthm xr-marking-view-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :marking-view index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :marking-view index x86)))

    Theorem: xr-os-info-mv-nth-3-get-prefixes-alt

    (defthm xr-os-info-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :os-info index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :os-info index x86)))

    Theorem: xr-rgf-mv-nth-3-get-prefixes-alt

    (defthm xr-rgf-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :rgf index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :rgf index x86)))

    Theorem: xr-rip-mv-nth-3-get-prefixes-alt

    (defthm xr-rip-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :rip index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :rip index x86)))

    Theorem: xr-rflags-mv-nth-3-get-prefixes-alt

    (defthm xr-rflags-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :rflags index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :rflags index x86)))

    Theorem: xr-seg-visible-mv-nth-3-get-prefixes-alt

    (defthm xr-seg-visible-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :seg-visible index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :seg-visible index x86)))

    Theorem: xr-seg-hidden-base-mv-nth-3-get-prefixes-alt

    (defthm xr-seg-hidden-base-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :seg-hidden-base index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :seg-hidden-base index x86)))

    Theorem: xr-seg-hidden-limit-mv-nth-3-get-prefixes-alt

    (defthm xr-seg-hidden-limit-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :seg-hidden-limit index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :seg-hidden-limit index x86)))

    Theorem: xr-seg-hidden-attr-mv-nth-3-get-prefixes-alt

    (defthm xr-seg-hidden-attr-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :seg-hidden-attr index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :seg-hidden-attr index x86)))

    Theorem: xr-str-mv-nth-3-get-prefixes-alt

    (defthm xr-str-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :str index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :str index x86)))

    Theorem: xr-ssr-visible-mv-nth-3-get-prefixes-alt

    (defthm xr-ssr-visible-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :ssr-visible index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :ssr-visible index x86)))

    Theorem: xr-ssr-hidden-base-mv-nth-3-get-prefixes-alt

    (defthm xr-ssr-hidden-base-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :ssr-hidden-base index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :ssr-hidden-base index x86)))

    Theorem: xr-ssr-hidden-limit-mv-nth-3-get-prefixes-alt

    (defthm xr-ssr-hidden-limit-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :ssr-hidden-limit index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :ssr-hidden-limit index x86)))

    Theorem: xr-ssr-hidden-attr-mv-nth-3-get-prefixes-alt

    (defthm xr-ssr-hidden-attr-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :ssr-hidden-attr index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :ssr-hidden-attr index x86)))

    Theorem: xr-ctr-mv-nth-3-get-prefixes-alt

    (defthm xr-ctr-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :ctr index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :ctr index x86)))

    Theorem: xr-dbg-mv-nth-3-get-prefixes-alt

    (defthm xr-dbg-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :dbg index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :dbg index x86)))

    Theorem: xr-fp-data-mv-nth-3-get-prefixes-alt

    (defthm xr-fp-data-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :fp-data index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :fp-data index x86)))

    Theorem: xr-fp-ctrl-mv-nth-3-get-prefixes-alt

    (defthm xr-fp-ctrl-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :fp-ctrl index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :fp-ctrl index x86)))

    Theorem: xr-fp-status-mv-nth-3-get-prefixes-alt

    (defthm xr-fp-status-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :fp-status index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :fp-status index x86)))

    Theorem: xr-fp-tag-mv-nth-3-get-prefixes-alt

    (defthm xr-fp-tag-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :fp-tag index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :fp-tag index x86)))

    Theorem: xr-fp-last-inst-mv-nth-3-get-prefixes-alt

    (defthm xr-fp-last-inst-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :fp-last-inst index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :fp-last-inst index x86)))

    Theorem: xr-fp-last-data-mv-nth-3-get-prefixes-alt

    (defthm xr-fp-last-data-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :fp-last-data index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :fp-last-data index x86)))

    Theorem: xr-fp-opcode-mv-nth-3-get-prefixes-alt

    (defthm xr-fp-opcode-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :fp-opcode index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :fp-opcode index x86)))

    Theorem: xr-mxcsr-mv-nth-3-get-prefixes-alt

    (defthm xr-mxcsr-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :mxcsr index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :mxcsr index x86)))

    Theorem: xr-opmsk-mv-nth-3-get-prefixes-alt

    (defthm xr-opmsk-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :opmsk index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :opmsk index x86)))

    Theorem: xr-zmm-mv-nth-3-get-prefixes-alt

    (defthm xr-zmm-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :zmm index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :zmm index x86)))

    Theorem: xr-msr-mv-nth-3-get-prefixes-alt

    (defthm xr-msr-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :msr index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :msr index x86)))

    Theorem: xr-fault-and-get-prefixes-alt

    (defthm xr-fault-and-get-prefixes-alt
 (equal
  (xr
    :fault index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :fault index x86)))

    Theorem: mv-nth-0-get-prefixes-alt-xw-doc

    (defthm mv-nth-0-get-prefixes-alt-xw-doc
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :doc index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-ms

    (defthm mv-nth-0-get-prefixes-alt-xw-ms
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (xw :ms index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-env

    (defthm mv-nth-0-get-prefixes-alt-xw-env
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :env index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-undef

    (defthm mv-nth-0-get-prefixes-alt-xw-undef
 (equal
  (mv-nth 0
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :undef index val x86)))
  (mv-nth 0
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-os-info

    (defthm mv-nth-0-get-prefixes-alt-xw-os-info
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :os-info index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-rgf

    (defthm mv-nth-0-get-prefixes-alt-xw-rgf
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :rgf index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-rip

    (defthm mv-nth-0-get-prefixes-alt-xw-rip
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :rip index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-str

    (defthm mv-nth-0-get-prefixes-alt-xw-str
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :str index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-ssr-visible

    (defthm mv-nth-0-get-prefixes-alt-xw-ssr-visible
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :ssr-visible index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-ssr-hidden-base

    (defthm mv-nth-0-get-prefixes-alt-xw-ssr-hidden-base
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte cnt
                               (xw :ssr-hidden-base index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-ssr-hidden-limit

    (defthm mv-nth-0-get-prefixes-alt-xw-ssr-hidden-limit
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes rex-byte cnt
                              (xw :ssr-hidden-limit index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-ssr-hidden-attr

    (defthm mv-nth-0-get-prefixes-alt-xw-ssr-hidden-attr
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte cnt
                               (xw :ssr-hidden-attr index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-dbg

    (defthm mv-nth-0-get-prefixes-alt-xw-dbg
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :dbg index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-fp-data

    (defthm mv-nth-0-get-prefixes-alt-xw-fp-data
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-data index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-fp-ctrl

    (defthm mv-nth-0-get-prefixes-alt-xw-fp-ctrl
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-ctrl index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-fp-status

    (defthm mv-nth-0-get-prefixes-alt-xw-fp-status
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-status index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-fp-tag

    (defthm mv-nth-0-get-prefixes-alt-xw-fp-tag
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-tag index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-fp-last-inst

    (defthm mv-nth-0-get-prefixes-alt-xw-fp-last-inst
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes rex-byte
                              cnt (xw :fp-last-inst index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-fp-last-data

    (defthm mv-nth-0-get-prefixes-alt-xw-fp-last-data
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes rex-byte
                              cnt (xw :fp-last-data index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-fp-opcode

    (defthm mv-nth-0-get-prefixes-alt-xw-fp-opcode
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-opcode index val x86)))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-mxcsr

    (defthm mv-nth-0-get-prefixes-alt-xw-mxcsr
 (equal
  (mv-nth 0
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :mxcsr index val x86)))
  (mv-nth 0
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-opmsk

    (defthm mv-nth-0-get-prefixes-alt-xw-opmsk
 (equal
  (mv-nth 0
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :opmsk index val x86)))
  (mv-nth 0
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-0-get-prefixes-alt-xw-zmm

    (defthm mv-nth-0-get-prefixes-alt-xw-zmm
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :zmm index val x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-doc

    (defthm mv-nth-1-get-prefixes-alt-xw-doc
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :doc index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-ms

    (defthm mv-nth-1-get-prefixes-alt-xw-ms
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (xw :ms index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-env

    (defthm mv-nth-1-get-prefixes-alt-xw-env
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :env index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-undef

    (defthm mv-nth-1-get-prefixes-alt-xw-undef
 (equal
  (mv-nth 1
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :undef index val x86)))
  (mv-nth 1
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-os-info

    (defthm mv-nth-1-get-prefixes-alt-xw-os-info
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :os-info index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-rgf

    (defthm mv-nth-1-get-prefixes-alt-xw-rgf
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :rgf index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-rip

    (defthm mv-nth-1-get-prefixes-alt-xw-rip
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :rip index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-str

    (defthm mv-nth-1-get-prefixes-alt-xw-str
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :str index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-ssr-visible

    (defthm mv-nth-1-get-prefixes-alt-xw-ssr-visible
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :ssr-visible index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-ssr-hidden-base

    (defthm mv-nth-1-get-prefixes-alt-xw-ssr-hidden-base
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte cnt
                               (xw :ssr-hidden-base index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-ssr-hidden-limit

    (defthm mv-nth-1-get-prefixes-alt-xw-ssr-hidden-limit
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes rex-byte cnt
                              (xw :ssr-hidden-limit index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-ssr-hidden-attr

    (defthm mv-nth-1-get-prefixes-alt-xw-ssr-hidden-attr
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte cnt
                               (xw :ssr-hidden-attr index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-dbg

    (defthm mv-nth-1-get-prefixes-alt-xw-dbg
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :dbg index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-fp-data

    (defthm mv-nth-1-get-prefixes-alt-xw-fp-data
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-data index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-fp-ctrl

    (defthm mv-nth-1-get-prefixes-alt-xw-fp-ctrl
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-ctrl index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-fp-status

    (defthm mv-nth-1-get-prefixes-alt-xw-fp-status
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-status index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-fp-tag

    (defthm mv-nth-1-get-prefixes-alt-xw-fp-tag
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-tag index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-fp-last-inst

    (defthm mv-nth-1-get-prefixes-alt-xw-fp-last-inst
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes rex-byte
                              cnt (xw :fp-last-inst index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-fp-last-data

    (defthm mv-nth-1-get-prefixes-alt-xw-fp-last-data
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes rex-byte
                              cnt (xw :fp-last-data index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-fp-opcode

    (defthm mv-nth-1-get-prefixes-alt-xw-fp-opcode
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-opcode index val x86)))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-mxcsr

    (defthm mv-nth-1-get-prefixes-alt-xw-mxcsr
 (equal
  (mv-nth 1
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :mxcsr index val x86)))
  (mv-nth 1
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-opmsk

    (defthm mv-nth-1-get-prefixes-alt-xw-opmsk
 (equal
  (mv-nth 1
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :opmsk index val x86)))
  (mv-nth 1
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-1-get-prefixes-alt-xw-zmm

    (defthm mv-nth-1-get-prefixes-alt-xw-zmm
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :zmm index val x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-doc

    (defthm mv-nth-2-get-prefixes-alt-xw-doc
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :doc index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-ms

    (defthm mv-nth-2-get-prefixes-alt-xw-ms
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (xw :ms index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-env

    (defthm mv-nth-2-get-prefixes-alt-xw-env
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :env index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-undef

    (defthm mv-nth-2-get-prefixes-alt-xw-undef
 (equal
  (mv-nth 2
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :undef index val x86)))
  (mv-nth 2
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-os-info

    (defthm mv-nth-2-get-prefixes-alt-xw-os-info
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :os-info index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-rgf

    (defthm mv-nth-2-get-prefixes-alt-xw-rgf
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :rgf index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-rip

    (defthm mv-nth-2-get-prefixes-alt-xw-rip
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :rip index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-str

    (defthm mv-nth-2-get-prefixes-alt-xw-str
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :str index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-ssr-visible

    (defthm mv-nth-2-get-prefixes-alt-xw-ssr-visible
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :ssr-visible index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-ssr-hidden-base

    (defthm mv-nth-2-get-prefixes-alt-xw-ssr-hidden-base
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte cnt
                               (xw :ssr-hidden-base index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-ssr-hidden-limit

    (defthm mv-nth-2-get-prefixes-alt-xw-ssr-hidden-limit
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes rex-byte cnt
                              (xw :ssr-hidden-limit index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-ssr-hidden-attr

    (defthm mv-nth-2-get-prefixes-alt-xw-ssr-hidden-attr
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte cnt
                               (xw :ssr-hidden-attr index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-dbg

    (defthm mv-nth-2-get-prefixes-alt-xw-dbg
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :dbg index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-fp-data

    (defthm mv-nth-2-get-prefixes-alt-xw-fp-data
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-data index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-fp-ctrl

    (defthm mv-nth-2-get-prefixes-alt-xw-fp-ctrl
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-ctrl index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-fp-status

    (defthm mv-nth-2-get-prefixes-alt-xw-fp-status
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-status index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-fp-tag

    (defthm mv-nth-2-get-prefixes-alt-xw-fp-tag
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-tag index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-fp-last-inst

    (defthm mv-nth-2-get-prefixes-alt-xw-fp-last-inst
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes rex-byte
                              cnt (xw :fp-last-inst index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-fp-last-data

    (defthm mv-nth-2-get-prefixes-alt-xw-fp-last-data
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes rex-byte
                              cnt (xw :fp-last-data index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-fp-opcode

    (defthm mv-nth-2-get-prefixes-alt-xw-fp-opcode
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :fp-opcode index val x86)))
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-mxcsr

    (defthm mv-nth-2-get-prefixes-alt-xw-mxcsr
 (equal
  (mv-nth 2
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :mxcsr index val x86)))
  (mv-nth 2
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-opmsk

    (defthm mv-nth-2-get-prefixes-alt-xw-opmsk
 (equal
  (mv-nth 2
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :opmsk index val x86)))
  (mv-nth 2
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-2-get-prefixes-alt-xw-zmm

    (defthm mv-nth-2-get-prefixes-alt-xw-zmm
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (xw :zmm index val x86)))
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-doc

    (defthm mv-nth-3-get-prefixes-alt-xw-doc
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :doc index val x86)))
  (xw
     :doc index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-ms

    (defthm mv-nth-3-get-prefixes-alt-xw-ms
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :ms index val x86)))
  (xw
     :ms index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-env

    (defthm mv-nth-3-get-prefixes-alt-xw-env
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :env index val x86)))
  (xw
     :env index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-undef

    (defthm mv-nth-3-get-prefixes-alt-xw-undef
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :undef index val x86)))
  (xw
     :undef index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-os-info

    (defthm mv-nth-3-get-prefixes-alt-xw-os-info
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :os-info index val x86)))
  (xw
     :os-info index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-rgf

    (defthm mv-nth-3-get-prefixes-alt-xw-rgf
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :rgf index val x86)))
  (xw
     :rgf index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-rip

    (defthm mv-nth-3-get-prefixes-alt-xw-rip
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :rip index val x86)))
  (xw
     :rip index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-str

    (defthm mv-nth-3-get-prefixes-alt-xw-str
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :str index val x86)))
  (xw
     :str index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-ssr-visible

    (defthm mv-nth-3-get-prefixes-alt-xw-ssr-visible
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :ssr-visible index val x86)))
  (xw
     :ssr-visible index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-ssr-hidden-base

    (defthm mv-nth-3-get-prefixes-alt-xw-ssr-hidden-base
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-base index val x86)))
  (xw
     :ssr-hidden-base index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-ssr-hidden-limit

    (defthm mv-nth-3-get-prefixes-alt-xw-ssr-hidden-limit
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-limit index val x86)))
  (xw
     :ssr-hidden-limit index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-ssr-hidden-attr

    (defthm mv-nth-3-get-prefixes-alt-xw-ssr-hidden-attr
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-attr index val x86)))
  (xw
     :ssr-hidden-attr index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-dbg

    (defthm mv-nth-3-get-prefixes-alt-xw-dbg
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :dbg index val x86)))
  (xw
     :dbg index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-fp-data

    (defthm mv-nth-3-get-prefixes-alt-xw-fp-data
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :fp-data index val x86)))
  (xw
     :fp-data index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-fp-ctrl

    (defthm mv-nth-3-get-prefixes-alt-xw-fp-ctrl
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :fp-ctrl index val x86)))
  (xw
     :fp-ctrl index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-fp-status

    (defthm mv-nth-3-get-prefixes-alt-xw-fp-status
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :fp-status index val x86)))
  (xw
     :fp-status index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-fp-tag

    (defthm mv-nth-3-get-prefixes-alt-xw-fp-tag
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :fp-tag index val x86)))
  (xw
     :fp-tag index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-fp-last-inst

    (defthm mv-nth-3-get-prefixes-alt-xw-fp-last-inst
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :fp-last-inst index val x86)))
  (xw
     :fp-last-inst index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-fp-last-data

    (defthm mv-nth-3-get-prefixes-alt-xw-fp-last-data
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :fp-last-data index val x86)))
  (xw
     :fp-last-data index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-fp-opcode

    (defthm mv-nth-3-get-prefixes-alt-xw-fp-opcode
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :fp-opcode index val x86)))
  (xw
     :fp-opcode index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-mxcsr

    (defthm mv-nth-3-get-prefixes-alt-xw-mxcsr
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :mxcsr index val x86)))
  (xw
     :mxcsr index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-opmsk

    (defthm mv-nth-3-get-prefixes-alt-xw-opmsk
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :opmsk index val x86)))
  (xw
     :opmsk index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: mv-nth-3-get-prefixes-alt-xw-zmm

    (defthm mv-nth-3-get-prefixes-alt-xw-zmm
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (xw :zmm index val x86)))
  (xw
     :zmm index val
     (mv-nth
          3
          (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))))

    Theorem: get-prefixes-alt-values-and-xw-rflags-in-sys-view

    (defthm get-prefixes-alt-values-and-xw-rflags-in-sys-view
 (implies
  (and (equal (rflagsbits->ac (double-rewrite value))
              (rflagsbits->ac (rflags x86)))
       (x86p x86))
  (and
   (equal
      (mv-nth 0
              (get-prefixes-alt start-rip prefixes rex-byte
                                cnt (xw :rflags nil value x86)))
      (mv-nth 0
              (get-prefixes-alt start-rip prefixes
                                rex-byte cnt (double-rewrite x86))))
   (equal
      (mv-nth 1
              (get-prefixes-alt start-rip prefixes rex-byte
                                cnt (xw :rflags nil value x86)))
      (mv-nth 1
              (get-prefixes-alt start-rip prefixes
                                rex-byte cnt (double-rewrite x86))))
   (equal
      (mv-nth 2
              (get-prefixes-alt start-rip prefixes rex-byte
                                cnt (xw :rflags nil value x86)))
      (mv-nth
           2
           (get-prefixes-alt start-rip prefixes
                             rex-byte cnt (double-rewrite x86)))))))

    Theorem: get-prefixes-alt-and-xw-rflags-state-in-sys-view

    (defthm get-prefixes-alt-and-xw-rflags-state-in-sys-view
 (implies
  (and (equal (rflagsbits->ac (double-rewrite value))
              (rflagsbits->ac (rflags x86)))
       (not (app-view x86))
       (x86p x86))
  (equal
       (mv-nth 3
               (get-prefixes-alt start-rip prefixes rex-byte
                                 cnt (xw :rflags nil value x86)))
       (xw :rflags nil value
           (mv-nth 3
                   (get-prefixes-alt start-rip
                                     prefixes rex-byte cnt x86))))))

    Theorem: xr-rflags-and-mv-nth-3-get-prefixes-alt

    (defthm xr-rflags-and-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :rflags nil
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :rflags nil x86)))

    Theorem: alignment-checking-enabled-p-and-mv-nth-3-get-prefixes-alt

    (defthm alignment-checking-enabled-p-and-mv-nth-3-get-prefixes-alt
 (equal
  (alignment-checking-enabled-p
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (alignment-checking-enabled-p x86)))

    Theorem: rewrite-get-prefixes-to-get-prefixes-alt

    (defthm rewrite-get-prefixes-to-get-prefixes-alt
 (implies
  (forced-and
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86))))
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip))
  (equal (get-prefixes 0 start-rip prefixes rex-byte cnt x86)
         (get-prefixes-alt start-rip prefixes
                           rex-byte cnt (double-rewrite x86)))))

    Theorem: get-prefixes-alt-opener-lemma-zero-cnt

    (defthm get-prefixes-alt-opener-lemma-zero-cnt
  (implies
       (and (marking-view x86)
            (64-bit-modep (double-rewrite x86))
            (not (app-view x86))
            (canonical-address-p start-rip))
       (equal (get-prefixes-alt start-rip prefixes rex-byte 0 x86)
              (mv t prefixes rex-byte x86))))

    Theorem: get-prefixes-alt-opener-lemma-no-prefix-byte

    (defthm get-prefixes-alt-opener-lemma-no-prefix-byte
 (implies
  (and
    (b* (((mv flg prefix-byte &)
          (rb-alt 1 start-rip
                  :x (double-rewrite x86)))
         (prefix-byte-group-code
              (get-one-byte-prefix-array-code prefix-byte)))
      (and (not flg)
           (zp prefix-byte-group-code)
           (not (equal (ash prefix-byte -4) 4))))
    (not (zp cnt))
    (marking-view x86)
    (64-bit-modep (double-rewrite x86))
    (not (app-view x86))
    (canonical-address-p start-rip)
    (not (mv-nth 0
                 (las-to-pas cnt start-rip
                             :x (double-rewrite x86))))
    (disjoint-p (mv-nth 1
                        (las-to-pas cnt start-rip
                                    :x (double-rewrite x86)))
                (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                            (double-rewrite x86)))))
  (b* (((mv new-flg new-prefixes new-rex-byte &)
        (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
   (and
    (equal new-flg nil)
    (equal
     new-prefixes
     (let
      ((prefixes
           (!prefixes->nxt (mv-nth 1
                                   (rb-alt 1 start-rip
                                           :x (double-rewrite x86)))
                           prefixes)))
      (!prefixes->num (- 15 cnt) prefixes)))
    (equal new-rex-byte rex-byte)))))

    Theorem: get-prefixes-alt-opener-lemma-no-legacy-prefix-but-rex-prefix

    (defthm
      get-prefixes-alt-opener-lemma-no-legacy-prefix-but-rex-prefix
 (implies
  (and
    (b* (((mv flg prefix-byte &)
          (rb-alt 1 start-rip
                  :x (double-rewrite x86)))
         (prefix-byte-group-code
              (get-one-byte-prefix-array-code prefix-byte)))
      (and (not flg)
           (zp prefix-byte-group-code)
           (equal (ash prefix-byte -4) 4)))
    (not (zp cnt))
    (marking-view x86)
    (64-bit-modep (double-rewrite x86))
    (not (app-view x86))
    (canonical-address-p start-rip)
    (not (mv-nth 0
                 (las-to-pas cnt start-rip
                             :x (double-rewrite x86))))
    (disjoint-p (mv-nth 1
                        (las-to-pas cnt start-rip
                                    :x (double-rewrite x86)))
                (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                            (double-rewrite x86)))))
  (equal
       (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
       (b* (((mv & byte byte-x86)
             (rb-alt 1 start-rip :x x86))
            (next-rip (the (signed-byte 49) (1+ start-rip))))
         (if (not (canonical-address-p next-rip))
             (mv (list :non-canonical-instruction-pointer next-rip)
                 prefixes rex-byte byte-x86)
           (get-prefixes-alt next-rip prefixes byte (1- cnt)
                             byte-x86))))))

    Theorem: get-prefixes-alt-opener-lemma-group-1-prefix-in-marking-view

    (defthm get-prefixes-alt-opener-lemma-group-1-prefix-in-marking-view
 (b* (((mv flg prefix-byte new-x86)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (not flg)
     (equal prefix-byte-group-code 1)
     (canonical-address-p (1+ start-rip))
     (not (zp cnt))
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip)
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86)))))
   (equal
        (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
        (get-prefixes-alt (+ 1 start-rip)
                          (if (equal prefix-byte 240)
                              (!prefixes->lck prefix-byte prefixes)
                            (!prefixes->rep prefix-byte prefixes))
                          0 (+ -1 cnt)
                          new-x86)))))

    Theorem: get-prefixes-alt-opener-lemma-group-2-prefix-in-marking-view

    (defthm get-prefixes-alt-opener-lemma-group-2-prefix-in-marking-view
 (b* (((mv flg prefix-byte new-x86)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (canonical-address-p (1+ start-rip))
     (not (zp cnt))
     (not flg)
     (equal prefix-byte-group-code 2)
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip)
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86)))))
   (equal
        (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
        (if (or (equal prefix-byte 100)
                (equal prefix-byte 101))
            (get-prefixes-alt (1+ start-rip)
                              (!prefixes->seg prefix-byte prefixes)
                              0 (1- cnt)
                              new-x86)
          (get-prefixes-alt (1+ start-rip)
                            prefixes 0 (1- cnt)
                            new-x86))))))

    Theorem: get-prefixes-alt-opener-lemma-group-3-prefix-in-marking-view

    (defthm get-prefixes-alt-opener-lemma-group-3-prefix-in-marking-view
 (b* (((mv flg prefix-byte new-x86)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (canonical-address-p (1+ start-rip))
     (not (zp cnt))
     (not flg)
     (equal prefix-byte-group-code 3)
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip)
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86)))))
   (equal (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
          (get-prefixes-alt (+ 1 start-rip)
                            (!prefixes->opr prefix-byte prefixes)
                            0 (+ -1 cnt)
                            new-x86)))))

    Theorem: get-prefixes-alt-opener-lemma-group-4-prefix-in-marking-view

    (defthm get-prefixes-alt-opener-lemma-group-4-prefix-in-marking-view
 (b* (((mv flg prefix-byte new-x86)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (canonical-address-p (1+ start-rip))
     (not (zp cnt))
     (not flg)
     (equal prefix-byte-group-code 4)
     (marking-view x86)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (canonical-address-p start-rip)
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86)))))
   (equal (get-prefixes-alt start-rip prefixes rex-byte cnt x86)
          (get-prefixes-alt (+ 1 start-rip)
                            (!prefixes->adr prefix-byte prefixes)
                            0 (+ -1 cnt)
                            new-x86)))))

    Theorem: get-prefixes-alt-xw-rflags-not-ac-values-in-sys-view

    (defthm get-prefixes-alt-xw-rflags-not-ac-values-in-sys-view
 (implies
  (equal (rflagsbits->ac (double-rewrite value))
         (rflagsbits->ac (rflags x86)))
  (and
   (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes rex-byte
                              cnt (xw :rflags nil value x86)))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
   (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes rex-byte
                              cnt (xw :rflags nil value x86)))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
   (equal (mv-nth 2
                  (get-prefixes-alt start-rip prefixes rex-byte
                                    cnt (xw :rflags nil value x86)))
          (mv-nth 2
                  (get-prefixes-alt start-rip
                                    prefixes rex-byte cnt x86))))))

    Theorem: xlate-equiv-memory-and-two-mv-nth-0-get-prefixes-alt-cong

    (defthm xlate-equiv-memory-and-two-mv-nth-0-get-prefixes-alt-cong
 (implies
  (xlate-equiv-memory x86-1 x86-2)
  (equal
   (mv-nth 0
           (get-prefixes-alt start-rip prefixes rex-byte cnt x86-1))
   (mv-nth 0
           (get-prefixes-alt start-rip
                             prefixes rex-byte cnt x86-2))))
 :rule-classes :congruence)

    Theorem: xlate-equiv-memory-and-two-mv-nth-1-get-prefixes-alt-cong

    (defthm xlate-equiv-memory-and-two-mv-nth-1-get-prefixes-alt-cong
 (implies
  (xlate-equiv-memory x86-1 x86-2)
  (equal
   (mv-nth 1
           (get-prefixes-alt start-rip prefixes rex-byte cnt x86-1))
   (mv-nth 1
           (get-prefixes-alt start-rip
                             prefixes rex-byte cnt x86-2))))
 :rule-classes :congruence)

    Theorem: xlate-equiv-memory-and-two-mv-nth-2-get-prefixes-alt-cong

    (defthm xlate-equiv-memory-and-two-mv-nth-2-get-prefixes-alt-cong
 (implies
  (xlate-equiv-memory x86-1 x86-2)
  (equal
   (mv-nth 2
           (get-prefixes-alt start-rip prefixes rex-byte cnt x86-1))
   (mv-nth 2
           (get-prefixes-alt start-rip
                             prefixes rex-byte cnt x86-2))))
 :rule-classes :congruence)

    Theorem: xlate-equiv-memory-and-two-mv-nth-3-get-prefixes-alt-cong

    (defthm xlate-equiv-memory-and-two-mv-nth-3-get-prefixes-alt-cong
 (implies
  (xlate-equiv-memory x86-1 x86-2)
  (xlate-equiv-memory
   (mv-nth 3
           (get-prefixes-alt start-rip prefixes rex-byte cnt x86-1))
   (mv-nth 3
           (get-prefixes-alt start-rip
                             prefixes rex-byte cnt x86-2))))
 :rule-classes :congruence)

    Theorem: xlate-equiv-memory-and-mv-nth-3-get-prefixes-alt

    (defthm xlate-equiv-memory-and-mv-nth-3-get-prefixes-alt
 (and
  (xlate-equiv-memory
    x86
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xlate-equiv-memory
     (mv-nth 3
             (get-prefixes-alt start-rip prefixes rex-byte cnt x86))
     (double-rewrite x86))))

    Theorem: mv-nth-3-get-prefixes-alt-no-prefix-byte

    (defthm mv-nth-3-get-prefixes-alt-no-prefix-byte
 (b* (((mv flg prefix-byte &)
       (rb-alt 1 start-rip
               :x (double-rewrite x86)))
      (prefix-byte-group-code
           (get-one-byte-prefix-array-code prefix-byte)))
  (implies
   (and
     (not flg)
     (zp prefix-byte-group-code)
     (not (equal (ash prefix-byte -4) 4))
     (not (zp cnt))
     (not (mv-nth 0
                  (las-to-pas cnt start-rip
                              :x (double-rewrite x86))))
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (64-bit-modep (double-rewrite x86)))
   (equal
     (mv-nth 3
             (get-prefixes-alt start-rip prefixes rex-byte cnt x86))
     (mv-nth 2 (las-to-pas 1 start-rip :x x86))))))

    Theorem: mv-nth-0-rb-and-xw-mem-in-sys-view

    (defthm mv-nth-0-rb-and-xw-mem-in-sys-view
  (implies
       (and (disjoint-p (list index)
                        (all-xlation-governing-entries-paddrs
                             n lin-addr (double-rewrite x86)))
            (canonical-address-p lin-addr)
            (canonical-address-p (+ -1 n lin-addr))
            (physical-address-p index)
            (unsigned-byte-p 8 value)
            (64-bit-modep (double-rewrite x86))
            (x86p x86))
       (equal (mv-nth 0
                      (rb n
                          lin-addr r-x (xw :mem index value x86)))
              (mv-nth 0
                      (rb n lin-addr r-x (double-rewrite x86))))))

    Theorem: read-from-physical-memory-xw-mem

    (defthm read-from-physical-memory-xw-mem
 (implies
  (disjoint-p (list index) p-addrs)
  (equal
       (read-from-physical-memory p-addrs (xw :mem index value x86))
       (read-from-physical-memory p-addrs x86))))

    Theorem: mv-nth-1-rb-and-xw-mem-in-sys-view

    (defthm mv-nth-1-rb-and-xw-mem-in-sys-view
 (implies
  (and
     (disjoint-p (list index)
                 (all-xlation-governing-entries-paddrs
                      n lin-addr (double-rewrite x86)))
     (disjoint-p
          (list index)
          (mv-nth 1
                  (las-to-pas n lin-addr r-x (double-rewrite x86))))
     (disjoint-p
          (mv-nth 1
                  (las-to-pas n lin-addr r-x (double-rewrite x86)))
          (all-xlation-governing-entries-paddrs
               n lin-addr (double-rewrite x86)))
     (canonical-address-p lin-addr)
     (canonical-address-p (+ -1 n lin-addr))
     (physical-address-p index)
     (unsigned-byte-p 8 value)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (x86p x86))
  (equal (mv-nth 1
                 (rb n
                     lin-addr r-x (xw :mem index value x86)))
         (mv-nth 1 (rb n lin-addr r-x x86)))))

    Function: find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux

    (defun find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux (vars calls)
 (declare (xargs :guard (true-listp vars)))
 (declare (xargs :guard (equal (len vars) 2)))
 (let
  ((__function__ 'find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux))
  (declare (ignorable __function__))
  (if (atom calls)
      nil
    (b* ((one-call (car calls))
         ((unless (and (true-listp one-call)
                       (equal 3 (len one-call))))
          nil)
         (mv-nth-term-1 (nth 1 one-call))
         ((unless (and (true-listp mv-nth-term-1)
                       (equal 3 (len mv-nth-term-1))))
          nil)
         (term-1 (nth 2 mv-nth-term-1))
         ((unless (and (true-listp term-1)
                       (equal 5 (len term-1))))
          nil)
         ((list n-var addr-var) vars))
      (cons (list (cons n-var (nth 1 term-1))
                  (cons addr-var (nth 2 term-1)))
            (find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
                 vars (cdr calls)))))))

    Function: find-l-addrs-from-disjoint-p-of-las-to-pas-and-all-xlation

    (defun find-l-addrs-from-disjoint-p-of-las-to-pas-and-all-xlation
       (vars r-w-x mfc state)
 (declare (xargs :stobjs (state))
          (ignorable state))
 (b*
  ((calls
    (acl2::find-matches-list
     (cons
      'disjoint-p
      (cons
       (cons
          'mv-nth
          (cons '1
                (cons (cons 'las-to-pas
                            (cons 'n
                                  (cons 'addr (cons r-w-x '(x86)))))
                      'nil)))
       '((all-xlation-governing-entries-paddrs n addr x86))))
     (mfc-clause mfc)
     nil))
   ((when (not calls)) nil))
  (find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux vars calls)))

    Theorem: get-prefixes-xw-mem-in-sys-view

    (defthm get-prefixes-xw-mem-in-sys-view
 (implies
  (and (disjoint-p (mv-nth 1
                           (las-to-pas cnt start-rip
                                       :x (double-rewrite x86)))
                   (all-xlation-governing-entries-paddrs
                        cnt start-rip (double-rewrite x86)))
       (disjoint-p (list index)
                   (mv-nth 1
                           (las-to-pas cnt start-rip
                                       :x (double-rewrite x86))))
       (disjoint-p (list index)
                   (all-xlation-governing-entries-paddrs
                        cnt start-rip (double-rewrite x86)))
       (not (mv-nth 0
                    (las-to-pas cnt start-rip
                                :x (double-rewrite x86))))
       (posp cnt)
       (canonical-address-p start-rip)
       (canonical-address-p (+ -1 cnt start-rip))
       (physical-address-p index)
       (unsigned-byte-p 8 value)
       (64-bit-modep (double-rewrite x86))
       (not (app-view x86))
       (marking-view x86)
       (x86p x86))
  (and
   (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :mem index value x86)))
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (double-rewrite x86))))
   (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :mem index value x86)))
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (double-rewrite x86))))
   (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :mem index value x86)))
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (double-rewrite x86))))
   (equal
    (mv-nth 3
            (get-prefixes 0 start-rip prefixes
                          rex-byte cnt (xw :mem index value x86)))
    (xw
      :mem index value
      (mv-nth 3
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (double-rewrite x86))))))))

    Theorem: get-prefixes-and-write-to-physical-memory

    (defthm get-prefixes-and-write-to-physical-memory
 (implies
  (and (disjoint-p (mv-nth 1
                           (las-to-pas cnt start-rip
                                       :x (double-rewrite x86)))
                   (all-xlation-governing-entries-paddrs
                        cnt start-rip (double-rewrite x86)))
       (disjoint-p p-addrs
                   (mv-nth 1
                           (las-to-pas cnt start-rip
                                       :x (double-rewrite x86))))
       (disjoint-p p-addrs
                   (all-xlation-governing-entries-paddrs
                        cnt start-rip (double-rewrite x86)))
       (not (mv-nth 0
                    (las-to-pas cnt start-rip
                                :x (double-rewrite x86))))
       (posp cnt)
       (canonical-address-p start-rip)
       (canonical-address-p (+ -1 cnt start-rip))
       (physical-address-listp p-addrs)
       (64-bit-modep (double-rewrite x86))
       (not (app-view x86))
       (marking-view x86)
       (x86p x86))
  (and
   (equal
    (mv-nth
        0
        (get-prefixes 0 start-rip prefixes rex-byte cnt
                      (write-to-physical-memory p-addrs value x86)))
    (mv-nth 0
            (get-prefixes 0 start-rip prefixes
                          rex-byte cnt (double-rewrite x86))))
   (equal
    (mv-nth
        1
        (get-prefixes 0 start-rip prefixes rex-byte cnt
                      (write-to-physical-memory p-addrs value x86)))
    (mv-nth 1
            (get-prefixes 0 start-rip prefixes
                          rex-byte cnt (double-rewrite x86))))
   (equal
    (mv-nth
        2
        (get-prefixes 0 start-rip prefixes rex-byte cnt
                      (write-to-physical-memory p-addrs value x86)))
    (mv-nth 2
            (get-prefixes 0 start-rip prefixes
                          rex-byte cnt (double-rewrite x86))))
   (equal
    (mv-nth
        3
        (get-prefixes 0 start-rip prefixes rex-byte cnt
                      (write-to-physical-memory p-addrs value x86)))
    (write-to-physical-memory
         p-addrs value
         (mv-nth 3
                 (get-prefixes 0 start-rip
                               prefixes rex-byte cnt x86)))))))

    Theorem: get-prefixes-alt-and-write-to-physical-memory-disjoint-from-paging-structures

    (defthm
 get-prefixes-alt-and-write-to-physical-memory-disjoint-from-paging-structures
 (implies
  (and
    (disjoint-p p-addrs
                (mv-nth 1
                        (las-to-pas cnt start-rip
                                    :x (double-rewrite x86))))
    (disjoint-p$ p-addrs
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
    (posp cnt)
    (canonical-address-p (+ -1 cnt start-rip))
    (physical-address-listp p-addrs)
    (x86p x86))
  (and
   (equal
      (mv-nth 0
              (get-prefixes-alt
                   start-rip prefixes rex-byte cnt
                   (write-to-physical-memory p-addrs value x86)))
      (mv-nth 0
              (get-prefixes-alt start-rip prefixes
                                rex-byte cnt (double-rewrite x86))))
   (equal
      (mv-nth 1
              (get-prefixes-alt
                   start-rip prefixes rex-byte cnt
                   (write-to-physical-memory p-addrs value x86)))
      (mv-nth 1
              (get-prefixes-alt start-rip prefixes
                                rex-byte cnt (double-rewrite x86))))
   (equal
      (mv-nth 2
              (get-prefixes-alt
                   start-rip prefixes rex-byte cnt
                   (write-to-physical-memory p-addrs value x86)))
      (mv-nth 2
              (get-prefixes-alt start-rip prefixes
                                rex-byte cnt (double-rewrite x86))))
   (equal
     (mv-nth 3
             (get-prefixes-alt
                  start-rip prefixes rex-byte cnt
                  (write-to-physical-memory p-addrs value x86)))
     (write-to-physical-memory
          p-addrs value
          (mv-nth 3
                  (get-prefixes-alt start-rip
                                    prefixes rex-byte cnt x86)))))))

    Theorem: get-prefixes-alt-and-wb-in-system-level-marking-view-disjoint-from-paging-structures

    (defthm
 get-prefixes-alt-and-wb-in-system-level-marking-view-disjoint-from-paging-structures
 (implies
  (and
    (disjoint-p$ (mv-nth 1
                         (las-to-pas n-w write-addr
                                     :w (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
    (disjoint-p (mv-nth 1
                        (las-to-pas n-w write-addr
                                    :w (double-rewrite x86)))
                (mv-nth 1
                        (las-to-pas cnt start-rip
                                    :x (double-rewrite x86))))
    (posp cnt)
    (canonical-address-p (+ -1 cnt start-rip))
    (64-bit-modep (double-rewrite x86))
    (not (app-view x86))
    (x86p x86))
  (and
   (equal
    (mv-nth
      0
      (get-prefixes-alt start-rip prefixes rex-byte cnt
                        (mv-nth 1 (wb n-w write-addr w value x86))))
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86))))
   (equal
    (mv-nth
      1
      (get-prefixes-alt start-rip prefixes rex-byte cnt
                        (mv-nth 1 (wb n-w write-addr w value x86))))
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes
                              rex-byte cnt (double-rewrite x86))))
   (equal
    (mv-nth
      2
      (get-prefixes-alt start-rip prefixes rex-byte cnt
                        (mv-nth 1 (wb n-w write-addr w value x86))))
    (mv-nth
         2
         (get-prefixes-alt start-rip prefixes
                           rex-byte cnt (double-rewrite x86)))))))

    Theorem: get-prefixes-alt-and-write-to-physical-memory-paging-structures

    (defthm
    get-prefixes-alt-and-write-to-physical-memory-paging-structures
 (implies
  (and
     (equal p-addrs (addr-range 8 index))
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (disjoint-p p-addrs
                 (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86))))
     (disjoint-p$ p-addrs
                  (all-xlation-governing-entries-paddrs
                       cnt start-rip (double-rewrite x86)))
     (equal (page-size (double-rewrite value))
            1)
     (posp cnt)
     (canonical-address-p (+ -1 cnt start-rip))
     (physical-address-listp p-addrs)
     (unsigned-byte-p 64 value)
     (physical-address-p index)
     (equal (loghead 3 index) 0)
     (x86p x86))
  (and
   (equal
      (mv-nth 0
              (get-prefixes-alt
                   start-rip prefixes rex-byte cnt
                   (write-to-physical-memory p-addrs value x86)))
      (mv-nth 0
              (get-prefixes-alt start-rip prefixes
                                rex-byte cnt (double-rewrite x86))))
   (equal
      (mv-nth 1
              (get-prefixes-alt
                   start-rip prefixes rex-byte cnt
                   (write-to-physical-memory p-addrs value x86)))
      (mv-nth 1
              (get-prefixes-alt start-rip prefixes
                                rex-byte cnt (double-rewrite x86))))
   (equal
      (mv-nth 2
              (get-prefixes-alt
                   start-rip prefixes rex-byte cnt
                   (write-to-physical-memory p-addrs value x86)))
      (mv-nth
           2
           (get-prefixes-alt start-rip prefixes
                             rex-byte cnt (double-rewrite x86)))))))

    Theorem: get-prefixes-alt-and-wb-to-paging-structures

    (defthm get-prefixes-alt-and-wb-to-paging-structures
 (implies
  (and
     (equal (page-size (double-rewrite value))
            1)
     (direct-map-p 8 lin-addr
                   :w (double-rewrite x86))
     (disjoint-p (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
     (disjoint-p (mv-nth 1
                         (las-to-pas 8 lin-addr
                                     :w (double-rewrite x86)))
                 (all-xlation-governing-entries-paddrs
                      cnt start-rip (double-rewrite x86)))
     (disjoint-p (mv-nth 1
                         (las-to-pas 8 lin-addr
                                     :w (double-rewrite x86)))
                 (mv-nth 1
                         (las-to-pas cnt start-rip
                                     :x (double-rewrite x86))))
     (posp cnt)
     (canonical-address-p (+ -1 cnt start-rip))
     (physical-address-p lin-addr)
     (equal (loghead 3 lin-addr) 0)
     (canonical-address-p lin-addr)
     (unsigned-byte-p 64 value)
     (64-bit-modep (double-rewrite x86))
     (not (app-view x86))
     (x86p x86))
  (and
   (equal
     (mv-nth
          0
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (mv-nth 1 (wb 8 lin-addr w value x86))))
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86))))
   (equal
     (mv-nth
          1
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (mv-nth 1 (wb 8 lin-addr w value x86))))
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes
                               rex-byte cnt (double-rewrite x86))))
   (equal
     (mv-nth
          2
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (mv-nth 1 (wb 8 lin-addr w value x86))))
     (mv-nth
          2
          (get-prefixes-alt start-rip prefixes
                            rex-byte cnt (double-rewrite x86)))))))