		Search-engine friendly clone of the ACL2 documentation.

Read-pc-of-write-memory-theorems

Theorems about reads of program counter over writes of memory.

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

Theorem: read-pc-of-write-mem8

(defthm read-pc-of-write-mem8
  (equal (read-pc (write-mem8 addr val stat feat)
                  feat)
         (read-pc stat feat)))

Theorem: read-pc-of-write-mem16

(defthm read-pc-of-write-mem16
  (equal (read-pc (write-mem16 addr val stat feat)
                  feat)
         (read-pc stat feat)))

Theorem: read-pc-of-write-mem32

(defthm read-pc-of-write-mem32
  (equal (read-pc (write-mem32 addr val stat feat)
                  feat)
         (read-pc stat feat)))

Theorem: read-pc-of-write-mem64

(defthm read-pc-of-write-mem64
  (equal (read-pc (write-mem64 addr val stat feat)
                  feat)
         (read-pc stat feat)))