• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
        • System-level-marking-view-proof-utilities
          • Rb-alt
          • Unwind-x86-interpreter-in-marking-view
          • Program-at-alt
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • 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
          • Phys-mem-values-same
        • 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
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • 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-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-enable-peripherals-mv-nth-3-get-prefixes-alt

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

Theorem: xr-handle-exceptions-mv-nth-3-get-prefixes-alt

(defthm xr-handle-exceptions-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :handle-exceptions index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :handle-exceptions 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-inhibit-interrupts-one-instruction-mv-nth-3-get-prefixes-alt

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

Theorem: xr-time-stamp-counter-mv-nth-3-get-prefixes-alt

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

Theorem: xr-last-clock-event-mv-nth-3-get-prefixes-alt

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

Theorem: xr-implicit-supervisor-access-mv-nth-3-get-prefixes-alt

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

Theorem: xr-tty-in-mv-nth-3-get-prefixes-alt

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

Theorem: xr-tty-out-mv-nth-3-get-prefixes-alt

(defthm xr-tty-out-mv-nth-3-get-prefixes-alt
 (equal
  (xr
    :tty-out index
    (mv-nth 3
            (get-prefixes-alt start-rip prefixes rex-byte cnt x86)))
  (xr :tty-out 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-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-enable-peripherals

(defthm mv-nth-0-get-prefixes-alt-xw-enable-peripherals
 (equal
  (mv-nth 0
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :enable-peripherals 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-handle-exceptions

(defthm mv-nth-0-get-prefixes-alt-xw-handle-exceptions
 (equal
   (mv-nth 0
           (get-prefixes-alt start-rip prefixes rex-byte cnt
                             (xw :handle-exceptions 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-0-get-prefixes-alt-xw-inhibit-interrupts-one-instruction

(defthm
    mv-nth-0-get-prefixes-alt-xw-inhibit-interrupts-one-instruction
 (equal
   (mv-nth 0
           (get-prefixes-alt start-rip prefixes rex-byte cnt
                             (xw :inhibit-interrupts-one-instruction
                                 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-time-stamp-counter

(defthm mv-nth-0-get-prefixes-alt-xw-time-stamp-counter
 (equal
  (mv-nth 0
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :time-stamp-counter 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-last-clock-event

(defthm mv-nth-0-get-prefixes-alt-xw-last-clock-event
 (equal
    (mv-nth 0
            (get-prefixes-alt start-rip prefixes rex-byte cnt
                              (xw :last-clock-event 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-tty-in

(defthm mv-nth-0-get-prefixes-alt-xw-tty-in
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :tty-in 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-tty-out

(defthm mv-nth-0-get-prefixes-alt-xw-tty-out
 (equal
     (mv-nth 0
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :tty-out 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-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-enable-peripherals

(defthm mv-nth-1-get-prefixes-alt-xw-enable-peripherals
 (equal
  (mv-nth 1
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :enable-peripherals 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-handle-exceptions

(defthm mv-nth-1-get-prefixes-alt-xw-handle-exceptions
 (equal
   (mv-nth 1
           (get-prefixes-alt start-rip prefixes rex-byte cnt
                             (xw :handle-exceptions 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-1-get-prefixes-alt-xw-inhibit-interrupts-one-instruction

(defthm
    mv-nth-1-get-prefixes-alt-xw-inhibit-interrupts-one-instruction
 (equal
   (mv-nth 1
           (get-prefixes-alt start-rip prefixes rex-byte cnt
                             (xw :inhibit-interrupts-one-instruction
                                 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-time-stamp-counter

(defthm mv-nth-1-get-prefixes-alt-xw-time-stamp-counter
 (equal
  (mv-nth 1
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :time-stamp-counter 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-last-clock-event

(defthm mv-nth-1-get-prefixes-alt-xw-last-clock-event
 (equal
    (mv-nth 1
            (get-prefixes-alt start-rip prefixes rex-byte cnt
                              (xw :last-clock-event 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-tty-in

(defthm mv-nth-1-get-prefixes-alt-xw-tty-in
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :tty-in 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-tty-out

(defthm mv-nth-1-get-prefixes-alt-xw-tty-out
 (equal
     (mv-nth 1
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :tty-out 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-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-enable-peripherals

(defthm mv-nth-2-get-prefixes-alt-xw-enable-peripherals
 (equal
  (mv-nth 2
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :enable-peripherals 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-handle-exceptions

(defthm mv-nth-2-get-prefixes-alt-xw-handle-exceptions
 (equal
   (mv-nth 2
           (get-prefixes-alt start-rip prefixes rex-byte cnt
                             (xw :handle-exceptions 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-2-get-prefixes-alt-xw-inhibit-interrupts-one-instruction

(defthm
    mv-nth-2-get-prefixes-alt-xw-inhibit-interrupts-one-instruction
 (equal
   (mv-nth 2
           (get-prefixes-alt start-rip prefixes rex-byte cnt
                             (xw :inhibit-interrupts-one-instruction
                                 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-time-stamp-counter

(defthm mv-nth-2-get-prefixes-alt-xw-time-stamp-counter
 (equal
  (mv-nth 2
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :time-stamp-counter 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-last-clock-event

(defthm mv-nth-2-get-prefixes-alt-xw-last-clock-event
 (equal
    (mv-nth 2
            (get-prefixes-alt start-rip prefixes rex-byte cnt
                              (xw :last-clock-event 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-tty-in

(defthm mv-nth-2-get-prefixes-alt-xw-tty-in
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :tty-in 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-tty-out

(defthm mv-nth-2-get-prefixes-alt-xw-tty-out
 (equal
     (mv-nth 2
             (get-prefixes-alt start-rip prefixes rex-byte
                               cnt (xw :tty-out 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-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-enable-peripherals

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

Theorem: mv-nth-3-get-prefixes-alt-xw-handle-exceptions

(defthm mv-nth-3-get-prefixes-alt-xw-handle-exceptions
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte cnt
                            (xw :handle-exceptions index val x86)))
  (xw
     :handle-exceptions 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: mv-nth-3-get-prefixes-alt-xw-inhibit-interrupts-one-instruction

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

Theorem: mv-nth-3-get-prefixes-alt-xw-time-stamp-counter

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

Theorem: mv-nth-3-get-prefixes-alt-xw-last-clock-event

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

Theorem: mv-nth-3-get-prefixes-alt-xw-tty-in

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

Theorem: mv-nth-3-get-prefixes-alt-xw-tty-out

(defthm mv-nth-3-get-prefixes-alt-xw-tty-out
 (equal
  (mv-nth 3
          (get-prefixes-alt start-rip prefixes rex-byte
                            cnt (xw :tty-out index val x86)))
  (xw
     :tty-out 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: paging-equiv-memory-and-two-mv-nth-0-get-prefixes-alt

(defthm paging-equiv-memory-and-two-mv-nth-0-get-prefixes-alt
 (implies
  (and (paging-equiv-memory x86-1 x86-2)
       (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)))))

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

(defthm paging-equiv-memory-and-two-mv-nth-1-get-prefixes-alt
 (implies
  (and (paging-equiv-memory x86-1 x86-2)
       (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)))))

Theorem: get-prefixes-alt-and-mv-nth-2-las-to-pas

(defthm get-prefixes-alt-and-mv-nth-2-las-to-pas
 (implies
  (64-bit-modep (double-rewrite x86))
  (and
   (equal
      (mv-nth 1
              (get-prefixes-alt
                   rip prefixes rex-byte cnt
                   (mv-nth 2 (las-to-pas n lin-addr r-w-x x86))))
      (mv-nth
           1
           (get-prefixes-alt rip prefixes
                             rex-byte cnt (double-rewrite x86)))))))

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

(defthm paging-equiv-memory-and-two-mv-nth-2-get-prefixes-alt
 (implies
  (and (paging-equiv-memory x86-1 x86-2)
       (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)))))