|
|
|---|
|
|
|
|---|
Theorems about reads of program counter over writes of registers.
These theorems are all enabled by default because they always clearly simplify the term.
Theorem:
(defthm read-pc-of-write-xreg (equal (read-pc (write-xreg reg val stat feat) feat) (read-pc stat feat)))
Theorem:
(defthm read-pc-of-write-xreg-32 (equal (read-pc (write-xreg-32 reg val stat feat) feat) (read-pc stat feat)))