		Search-engine friendly clone of the ACL2 documentation.

Read-memory-of-write-pc-theorems

Theorems about reads of memory over writes of program counter.

The writes of program counter include not only write-pc but also inc4-pc.

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

Theorem: read-mem8-of-write-pc

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

Theorem: read-mem16-of-write-pc

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

Theorem: read-mem32-of-write-pc

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

Theorem: read-mem64-of-write-pc

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

Theorem: read-mem8-of-inc4-pc

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

Theorem: read-mem16-of-inc4-pc

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

Theorem: read-mem32-of-inc4-pc

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

Theorem: read-mem64-of-inc4-pc

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