Get the r/m field from a opcode.
(opcode->r/m x) → r/m
This is an ordinary field accessor created by defprod.
Function:
(defun opcode->r/m$inline (x) (declare (xargs :guard (opcode-p x))) (declare (xargs :guard t)) (let ((__function__ 'opcode->r/m)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (maybe-3bits-fix (std::prod-car (std::prod-cdr (std::prod-cdr (std::prod-car x)))))) :exec (std::prod-car (std::prod-cdr (std::prod-cdr (std::prod-car x)))))))
Theorem:
(defthm maybe-3bits-p-of-opcode->r/m (b* ((r/m (opcode->r/m$inline x))) (maybe-3bits-p r/m)) :rule-classes :rewrite)
Theorem:
(defthm opcode->r/m$inline-of-opcode-fix-x (equal (opcode->r/m$inline (opcode-fix x)) (opcode->r/m$inline x)))
Theorem:
(defthm opcode->r/m$inline-opcode-equiv-congruence-on-x (implies (opcode-equiv x x-equiv) (equal (opcode->r/m$inline x) (opcode->r/m$inline x-equiv))) :rule-classes :congruence)