|
|
|---|
|
|
|
|---|
Theorems about reads of instructions 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:
(defthm read-instr-of-write-pc (equal (read-instr addr (write-pc pc stat feat) feat) (read-instr addr stat feat)))
Theorem:
(defthm read-instr-of-inc4-pc (equal (read-instr addr (inc4-pc stat feat) feat) (read-instr addr stat feat)))