		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read-xreg-unsigned-to-read32-xreg-unsigned{3}

Rewriting of riscv::read-xreg-unsigned to read32-xreg-unsigned{3}.

Definitions and Theorems

Theorem: read-xreg-unsigned-to-read32-xreg-unsigned{3}

(defthm read-xreg-unsigned-to-read32-xreg-unsigned{3}
 (implies
     (and (riscv::statp stat)
          (equal feat (feat-rv32im-le))
          (riscv::stat-validp stat feat)
          (natp reg)
          (< reg 32))
     (equal (riscv::read-xreg-unsigned reg stat feat)
            (read32-xreg-unsigned{3} reg (stat32-from-stat stat)))))