• 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-in-system-level-marking-view

Definitions and Theorems

Theorem: xr-not-mem-and-get-prefixes

(defthm xr-not-mem-and-get-prefixes
 (implies
  (and (not (equal fld :mem))
       (not (equal fld :fault)))
  (equal
    (xr fld index
        (mv-nth 3
                (get-prefixes proc-mode
                              start-rip prefixes rex-byte cnt x86)))
    (xr fld index x86))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: xr-fault-and-get-prefixes

(defthm xr-fault-and-get-prefixes
 (implies
  (and (canonical-address-p start-rip)
       (not (mv-nth 0
                    (las-to-pas cnt start-rip
                                :x (double-rewrite x86)))))
  (equal
   (xr
      :fault index
      (mv-nth 3
              (get-prefixes 0 start-rip prefixes rex-byte cnt x86)))
   (xr :fault index x86))))

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

(defthm get-prefixes-xw-values-in-sys-view
 (implies
  (and (not (app-view x86))
       (not (equal fld :mem))
       (not (equal fld :rflags))
       (not (equal fld :ctr))
       (not (equal fld :seg-visible))
       (not (equal fld :seg-hidden-base))
       (not (equal fld :seg-hidden-limit))
       (not (equal fld :seg-hidden-attr))
       (not (equal fld :msr))
       (not (equal fld :fault))
       (not (equal fld :app-view))
       (not (equal fld :marking-view)))
  (and
   (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw fld index value x86)))
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte cnt x86)))
   (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw fld index value x86)))
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte cnt x86)))
   (equal
       (mv-nth 2
               (get-prefixes 0 start-rip prefixes
                             rex-byte cnt (xw fld index value x86)))
       (mv-nth 2
               (get-prefixes 0 start-rip
                             prefixes rex-byte cnt x86))))))

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

(defthm get-prefixes-xw-state-in-sys-view
 (implies
  (and (not (app-view x86))
       (not (equal fld :mem))
       (not (equal fld :rflags))
       (not (equal fld :ctr))
       (not (equal fld :seg-visible))
       (not (equal fld :seg-hidden-base))
       (not (equal fld :seg-hidden-limit))
       (not (equal fld :seg-hidden-attr))
       (not (equal fld :msr))
       (not (equal fld :fault))
       (not (equal fld :app-view))
       (not (equal fld :marking-view)))
  (equal
       (mv-nth 3
               (get-prefixes 0 start-rip prefixes
                             rex-byte cnt (xw fld index value x86)))
       (xw fld index value
           (mv-nth 3
                   (get-prefixes 0 start-rip
                                 prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-0-get-prefixes-xw-doc
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :doc index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-ms
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :ms index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-env
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :env index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-undef
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :undef index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-os-info
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :os-info index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-rgf
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :rgf index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-rip
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :rip index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-str
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :str index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-ssr-visible
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :ssr-visible index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-ssr-hidden-base
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-base index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-ssr-hidden-limit
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-limit index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-ssr-hidden-attr
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-attr index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-dbg
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :dbg index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-fp-data
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-data index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-fp-ctrl
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-ctrl index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-fp-status
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-status index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-fp-tag
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-tag index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-fp-last-inst
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-last-inst index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-fp-last-data
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-last-data index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-fp-opcode
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-opcode index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-mxcsr
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :mxcsr index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-opmsk
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :opmsk index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-0-get-prefixes-xw-zmm
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 0
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :zmm index val x86)))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-doc
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :doc index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-ms
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :ms index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-env
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :env index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-undef
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :undef index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-os-info
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :os-info index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-rgf
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :rgf index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-rip
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :rip index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-str
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :str index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-ssr-visible
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :ssr-visible index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-ssr-hidden-base
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-base index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-ssr-hidden-limit
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-limit index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-ssr-hidden-attr
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-attr index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-dbg
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :dbg index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-fp-data
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-data index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-fp-ctrl
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-ctrl index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-fp-status
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-status index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-fp-tag
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-tag index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-fp-last-inst
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-last-inst index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-fp-last-data
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-last-data index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-fp-opcode
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-opcode index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-mxcsr
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :mxcsr index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-opmsk
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :opmsk index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-1-get-prefixes-xw-zmm
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 1
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :zmm index val x86)))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-doc
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :doc index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-ms
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :ms index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-env
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :env index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-undef
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :undef index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-os-info
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :os-info index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-rgf
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :rgf index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-rip
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :rip index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-str
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :str index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-ssr-visible
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :ssr-visible index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-ssr-hidden-base
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-base index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-ssr-hidden-limit
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-limit index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-ssr-hidden-attr
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte cnt
                            (xw :ssr-hidden-attr index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-dbg
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :dbg index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-fp-data
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-data index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-fp-ctrl
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-ctrl index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-fp-status
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-status index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-fp-tag
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-tag index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-fp-last-inst
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-last-inst index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-fp-last-data
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-last-data index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-fp-opcode
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes rex-byte
                            cnt (xw :fp-opcode index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-mxcsr
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :mxcsr index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-opmsk
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :opmsk index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-2-get-prefixes-xw-zmm
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 2
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :zmm index val x86)))
      (mv-nth 2
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86)))))

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

(defthm mv-nth-3-get-prefixes-xw-doc
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes
                              rex-byte cnt (xw :doc index val x86)))
        (xw :doc index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-ms
 (implies
  (not (app-view x86))
  (equal (mv-nth 3
                 (get-prefixes 0 start-rip prefixes
                               rex-byte cnt (xw :ms index val x86)))
         (xw :ms index val
             (mv-nth 3
                     (get-prefixes 0 start-rip
                                   prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-env
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes
                              rex-byte cnt (xw :env index val x86)))
        (xw :env index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-undef
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 3
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :undef index val x86)))
      (xw :undef index val
          (mv-nth 3
                  (get-prefixes 0 start-rip
                                prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-os-info
 (implies
    (not (app-view x86))
    (equal (mv-nth 3
                   (get-prefixes 0 start-rip prefixes rex-byte
                                 cnt (xw :os-info index val x86)))
           (xw :os-info index val
               (mv-nth 3
                       (get-prefixes 0 start-rip
                                     prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-rgf
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes
                              rex-byte cnt (xw :rgf index val x86)))
        (xw :rgf index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-rip
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes
                              rex-byte cnt (xw :rip index val x86)))
        (xw :rip index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-str
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes
                              rex-byte cnt (xw :str index val x86)))
        (xw :str index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-ssr-visible
 (implies
  (not (app-view x86))
  (equal (mv-nth 3
                 (get-prefixes 0 start-rip prefixes rex-byte
                               cnt (xw :ssr-visible index val x86)))
         (xw :ssr-visible index val
             (mv-nth 3
                     (get-prefixes 0 start-rip
                                   prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-ssr-hidden-base
 (implies
  (not (app-view x86))
  (equal (mv-nth 3
                 (get-prefixes 0 start-rip prefixes rex-byte cnt
                               (xw :ssr-hidden-base index val x86)))
         (xw :ssr-hidden-base index val
             (mv-nth 3
                     (get-prefixes 0 start-rip
                                   prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-ssr-hidden-limit
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes rex-byte cnt
                              (xw :ssr-hidden-limit index val x86)))
        (xw :ssr-hidden-limit index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-ssr-hidden-attr
 (implies
  (not (app-view x86))
  (equal (mv-nth 3
                 (get-prefixes 0 start-rip prefixes rex-byte cnt
                               (xw :ssr-hidden-attr index val x86)))
         (xw :ssr-hidden-attr index val
             (mv-nth 3
                     (get-prefixes 0 start-rip
                                   prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-dbg
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes
                              rex-byte cnt (xw :dbg index val x86)))
        (xw :dbg index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-fp-data
 (implies
    (not (app-view x86))
    (equal (mv-nth 3
                   (get-prefixes 0 start-rip prefixes rex-byte
                                 cnt (xw :fp-data index val x86)))
           (xw :fp-data index val
               (mv-nth 3
                       (get-prefixes 0 start-rip
                                     prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-fp-ctrl
 (implies
    (not (app-view x86))
    (equal (mv-nth 3
                   (get-prefixes 0 start-rip prefixes rex-byte
                                 cnt (xw :fp-ctrl index val x86)))
           (xw :fp-ctrl index val
               (mv-nth 3
                       (get-prefixes 0 start-rip
                                     prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-fp-status
 (implies
    (not (app-view x86))
    (equal (mv-nth 3
                   (get-prefixes 0 start-rip prefixes rex-byte
                                 cnt (xw :fp-status index val x86)))
           (xw :fp-status index val
               (mv-nth 3
                       (get-prefixes 0 start-rip
                                     prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-fp-tag
 (implies
    (not (app-view x86))
    (equal (mv-nth 3
                   (get-prefixes 0 start-rip prefixes rex-byte
                                 cnt (xw :fp-tag index val x86)))
           (xw :fp-tag index val
               (mv-nth 3
                       (get-prefixes 0 start-rip
                                     prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-fp-last-inst
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes rex-byte
                              cnt (xw :fp-last-inst index val x86)))
        (xw :fp-last-inst index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-fp-last-data
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes rex-byte
                              cnt (xw :fp-last-data index val x86)))
        (xw :fp-last-data index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-fp-opcode
 (implies
    (not (app-view x86))
    (equal (mv-nth 3
                   (get-prefixes 0 start-rip prefixes rex-byte
                                 cnt (xw :fp-opcode index val x86)))
           (xw :fp-opcode index val
               (mv-nth 3
                       (get-prefixes 0 start-rip
                                     prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-mxcsr
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 3
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :mxcsr index val x86)))
      (xw :mxcsr index val
          (mv-nth 3
                  (get-prefixes 0 start-rip
                                prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-opmsk
 (implies
  (not (app-view x86))
  (equal
      (mv-nth 3
              (get-prefixes 0 start-rip prefixes
                            rex-byte cnt (xw :opmsk index val x86)))
      (xw :opmsk index val
          (mv-nth 3
                  (get-prefixes 0 start-rip
                                prefixes rex-byte cnt x86))))))

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

(defthm mv-nth-3-get-prefixes-xw-zmm
 (implies
   (not (app-view x86))
   (equal
        (mv-nth 3
                (get-prefixes 0 start-rip prefixes
                              rex-byte cnt (xw :zmm index val x86)))
        (xw :zmm index val
            (mv-nth 3
                    (get-prefixes 0 start-rip
                                  prefixes rex-byte cnt x86))))))

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

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

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

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

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

(defthm get-prefixes-opener-lemma-group-1-prefix-in-marking-view
  (b*
    (((mv flg byte new-x86)
      (rml08 start-rip
             :x (double-rewrite x86)))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (implies
         (and (canonical-address-p (1+ start-rip))
              (not (zp cnt))
              (not flg)
              (equal prefix-byte-group-code 1)
              (not (app-view x86)))
         (equal (get-prefixes 0 start-rip prefixes rex-byte cnt x86)
                (get-prefixes 0 (+ 1 start-rip)
                              (if (equal byte 240)
                                  (!prefixes->lck byte prefixes)
                                (!prefixes->rep byte prefixes))
                              0 (+ -1 cnt)
                              new-x86)))))

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

(defthm get-prefixes-opener-lemma-group-2-prefix-in-marking-view
  (b*
    (((mv flg byte new-x86)
      (rml08 start-rip
             :x (double-rewrite x86)))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (implies
         (and (canonical-address-p (1+ start-rip))
              (not (zp cnt))
              (not flg)
              (equal prefix-byte-group-code 2)
              (not (app-view x86)))
         (equal (get-prefixes 0 start-rip prefixes rex-byte cnt x86)
                (if (or (equal byte 100) (equal byte 101))
                    (get-prefixes 0 (1+ start-rip)
                                  (!prefixes->seg byte prefixes)
                                  0 (1- cnt)
                                  new-x86)
                  (get-prefixes 0 (1+ start-rip)
                                prefixes 0 (1- cnt)
                                new-x86))))))

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

(defthm get-prefixes-opener-lemma-group-3-prefix-in-marking-view
  (b*
    (((mv flg byte new-x86)
      (rml08 start-rip
             :x (double-rewrite x86)))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (implies
         (and (canonical-address-p (1+ start-rip))
              (not (zp cnt))
              (not flg)
              (equal prefix-byte-group-code 3)
              (not (app-view x86)))
         (equal (get-prefixes 0 start-rip prefixes rex-byte cnt x86)
                (get-prefixes 0 (1+ start-rip)
                              (!prefixes->opr byte prefixes)
                              0 (1- cnt)
                              new-x86)))))

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

(defthm get-prefixes-opener-lemma-group-4-prefix-in-marking-view
  (b*
    (((mv flg byte new-x86)
      (rml08 start-rip
             :x (double-rewrite x86)))
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (implies
         (and (canonical-address-p (1+ start-rip))
              (not (zp cnt))
              (not flg)
              (equal prefix-byte-group-code 4)
              (not (app-view x86)))
         (equal (get-prefixes 0 start-rip prefixes rex-byte cnt x86)
                (get-prefixes 0 (1+ start-rip)
                              (!prefixes->adr byte prefixes)
                              0 (1- cnt)
                              new-x86)))))

Function: get-prefixes-two-x86-induct-hint

(defun get-prefixes-two-x86-induct-hint
       (start-rip prefixes rex-byte cnt x86-1 x86-2)
 (declare (xargs :non-executable t))
 (prog2$
  (acl2::throw-nonexec-error
       'get-prefixes-two-x86-induct-hint
       (list start-rip
             prefixes rex-byte cnt x86-1 x86-2))
  (if (zp cnt)
      (mv nil prefixes x86-1 x86-2)
   (b*
    ((ctx 'get-prefixes-two-x86-induct-hint)
     ((mv flg-1 byte-1 x86-1)
      (rml08 start-rip :x x86-1))
     ((mv flg-2 byte-2 x86-2)
      (rml08 start-rip :x x86-2))
     ((when flg-1)
      (mv (cons ctx flg-1) byte-1 x86-1))
     ((when flg-2)
      (mv (cons ctx flg-2) byte-2 x86-2))
     ((when (not (equal byte-1 byte-2)))
      (mv nil prefixes x86-1 x86-2))
     (byte byte-1)
     (prefix-byte-group-code (get-one-byte-prefix-array-code byte)))
    (case prefix-byte-group-code
     (0
       (b* ((rex? (equal (the (unsigned-byte 4) (ash byte -4))
                         4))
            ((when rex?)
             (let ((next-rip (the (signed-byte 49) (1+ start-rip))))
               (if (canonical-address-p next-rip)
                   (get-prefixes-two-x86-induct-hint
                        next-rip prefixes
                        byte (the (integer 0 15) (1- cnt))
                        x86-1 x86-2)
                 (mv (cons 'non-canonical-address next-rip)
                     prefixes rex-byte x86-1 x86-2)))))
         (let ((prefixes (!prefixes->nxt byte prefixes)))
           (mv nil (!prefixes->num (- 15 cnt) prefixes)
               rex-byte x86-1 x86-2))))
     (1 (b* ((next-rip (the (signed-byte 49) (1+ start-rip)))
             ((when (not (canonical-address-p next-rip)))
              (mv (cons 'non-canonical-address next-rip)
                  prefixes rex-byte x86-1 x86-2))
             (prefixes (if (equal byte 240)
                           (!prefixes->lck byte prefixes)
                         (!prefixes->rep byte prefixes))))
          (get-prefixes-two-x86-induct-hint
               next-rip
               prefixes 0 (the (integer 0 15) (1- cnt))
               x86-1 x86-2)))
     (2 (b* ((next-rip (the (signed-byte 49) (1+ start-rip)))
             ((when (not (canonical-address-p next-rip)))
              (mv (cons 'non-canonical-address next-rip)
                  prefixes rex-byte x86-1 x86-2)))
          (if (or (equal byte 100) (equal byte 101))
              (get-prefixes-two-x86-induct-hint
                   next-rip (!prefixes->seg byte prefixes)
                   0 (the (integer 0 15) (1- cnt))
                   x86-1 x86-2)
            (get-prefixes-two-x86-induct-hint
                 next-rip
                 prefixes 0 (the (integer 0 15) (1- cnt))
                 x86-1 x86-2))))
     (3 (b* ((next-rip (the (signed-byte 49) (1+ start-rip)))
             ((when (not (canonical-address-p next-rip)))
              (mv (cons 'non-canonical-address next-rip)
                  prefixes rex-byte x86-1 x86-2)))
          (get-prefixes-two-x86-induct-hint
               next-rip (!prefixes->opr byte prefixes)
               0 (the (integer 0 15) (1- cnt))
               x86-1 x86-2)))
     (4 (b* ((next-rip (the (signed-byte 49) (1+ start-rip)))
             ((when (not (canonical-address-p next-rip)))
              (mv (cons 'non-canonical-address next-rip)
                  prefixes rex-byte x86-1 x86-2)))
          (get-prefixes-two-x86-induct-hint
               next-rip (!prefixes->adr byte prefixes)
               0 (the (integer 0 15) (1- cnt))
               x86-1 x86-2)))
     (otherwise (mv t prefixes rex-byte x86-1 x86-2)))))))

Theorem: xlate-equiv-memory-and-two-get-prefixes-values

(defthm xlate-equiv-memory-and-two-get-prefixes-values
 (implies
  (and
   (bind-free (find-an-xlate-equiv-x86
                   'xlate-equiv-memory-and-two-get-prefixes-values
                   x86-1 'x86-2
                   mfc state)
              (x86-2))
   (syntaxp (not (equal x86-1 x86-2)))
   (xlate-equiv-memory (double-rewrite x86-1)
                       x86-2)
   (canonical-address-p start-rip)
   (not (mv-nth 0
                (las-to-pas cnt start-rip
                            :x (double-rewrite x86-1))))
   (disjoint-p (mv-nth 1
                       (las-to-pas cnt start-rip
                                   :x (double-rewrite x86-1)))
               (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                           (double-rewrite x86-1))))
   (64-bit-modep (double-rewrite x86-1)))
  (and
   (equal
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86-1))
      (mv-nth 0
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86-2)))
   (equal
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86-1))
      (mv-nth 1
              (get-prefixes 0
                            start-rip prefixes rex-byte cnt x86-2)))
   (equal
       (mv-nth 2
               (get-prefixes 0
                             start-rip prefixes rex-byte cnt x86-1))
       (mv-nth 2
               (get-prefixes 0 start-rip
                             prefixes rex-byte cnt x86-2))))))

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

(defthm xlate-equiv-memory-and-mv-nth-3-get-prefixes
 (implies
  (and (not (app-view (double-rewrite x86)))
       (marking-view (double-rewrite x86))
       (canonical-address-p start-rip)
       (not (mv-nth 0
                    (las-to-pas cnt start-rip
                                :x (double-rewrite x86))))
       (64-bit-modep (double-rewrite x86)))
  (xlate-equiv-memory
       (mv-nth 3
               (get-prefixes 0 start-rip prefixes rex-byte cnt x86))
       (double-rewrite x86))))

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

(defthm xlate-equiv-memory-and-two-mv-nth-3-get-prefixes
 (implies
  (and (xlate-equiv-memory (double-rewrite x86-1)
                           x86-2)
       (not (app-view x86-2))
       (marking-view (double-rewrite x86-2))
       (canonical-address-p start-rip)
       (not (mv-nth 0
                    (las-to-pas cnt start-rip
                                :x (double-rewrite x86-2))))
       (64-bit-modep x86-2))
  (xlate-equiv-memory
       (mv-nth 3
               (get-prefixes 0
                             start-rip prefixes rex-byte cnt x86-1))
       (mv-nth 3
               (get-prefixes 0 start-rip
                             prefixes rex-byte cnt x86-2)))))