Get the kind (tag) of a op-32-funct structure.
(op-32-funct-kind x) → kind
Function:
(defun op-32-funct-kind$inline (x) (declare (xargs :guard (op-32-funct-p x))) (let ((__function__ 'op-32-funct-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :addw)) :addw) ((eq (car x) :subw) :subw) ((eq (car x) :sllw) :sllw) ((eq (car x) :srlw) :srlw) ((eq (car x) :sraw) :sraw) ((eq (car x) :mulw) :mulw) ((eq (car x) :divw) :divw) ((eq (car x) :divuw) :divuw) ((eq (car x) :remw) :remw) (t :remuw)) :exec (car x))))
Theorem:
(defthm op-32-funct-kind-possibilities (or (equal (op-32-funct-kind x) :addw) (equal (op-32-funct-kind x) :subw) (equal (op-32-funct-kind x) :sllw) (equal (op-32-funct-kind x) :srlw) (equal (op-32-funct-kind x) :sraw) (equal (op-32-funct-kind x) :mulw) (equal (op-32-funct-kind x) :divw) (equal (op-32-funct-kind x) :divuw) (equal (op-32-funct-kind x) :remw) (equal (op-32-funct-kind x) :remuw)) :rule-classes ((:forward-chaining :trigger-terms ((op-32-funct-kind x)))))