(vl-op-simple-vector-p x) → *
Function:
(defun vl-op-simple-vector-p (x) (declare (xargs :guard (vl-op-p x))) (let ((__function__ 'vl-op-simple-vector-p)) (declare (ignorable __function__)) (member (vl-op-fix x) '(:vl-unary-plus :vl-unary-minus :vl-unary-lognot :vl-unary-bitnot :vl-unary-bitand :vl-unary-nand :vl-unary-bitor :vl-unary-nor :vl-unary-xor :vl-unary-xnor :vl-binary-plus :vl-binary-minus :vl-binary-times :vl-binary-div :vl-binary-rem :vl-binary-eq :vl-binary-neq :vl-binary-ceq :vl-binary-cne :vl-binary-wildeq :vl-binary-wildneq :vl-binary-logand :vl-binary-logor :vl-binary-power :vl-binary-lt :vl-binary-lte :vl-binary-gt :vl-binary-gte :vl-binary-bitand :vl-binary-bitor :vl-binary-xor :vl-binary-xnor :vl-binary-shr :vl-binary-shl :vl-binary-ashr :vl-binary-ashl :vl-implies :vl-equiv :vl-bitselect :vl-select-colon :vl-select-pluscolon :vl-select-minuscolon :vl-partselect-colon :vl-partselect-pluscolon :vl-partselect-minuscolon :vl-multiconcat))))
Theorem:
(defthm vl-op-simple-vector-p-of-vl-op-fix-x (equal (vl-op-simple-vector-p (vl-op-fix x)) (vl-op-simple-vector-p x)))
Theorem:
(defthm vl-op-simple-vector-p-vl-op-equiv-congruence-on-x (implies (vl-op-equiv x x-equiv) (equal (vl-op-simple-vector-p x) (vl-op-simple-vector-p x-equiv))) :rule-classes :congruence)