		Search-engine friendly clone of the ACL2 documentation.

Reads-over-writes

Read-instr-of-write-xreg-theorems

Theorems about reads of instructions over writes of registers.

These theorems are all enabled by default because they always clearly simplify the term.

Definitions and Theorems

Theorem: read-instr-of-write-xreg

(defthm read-instr-of-write-xreg
  (equal (read-instr addr (write-xreg reg val stat feat)
                     feat)
         (read-instr addr stat feat)))

Theorem: read-instr-of-write-xreg-32

(defthm read-instr-of-write-xreg-32
  (equal (read-instr addr (write-xreg-32 reg val stat feat)
                     feat)
         (read-instr addr stat feat)))