		Search-engine friendly clone of the ACL2 documentation.

Strict-opcode-p

Signature
(strict-opcode-p x) → *

Definitions and Theorems

Function: strict-opcode-p

(defun strict-opcode-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'strict-opcode-p))
  (declare (ignorable __function__))
  (and
   (opcode-p x)
   (b*
    (((opcode x))
     ((when
          (and (any-present-in (append (list :avx :avx2 :bmi1 :bmi2)
                                       *avx512-feature-flags*)
                               x.feat)
               (null x.vex)
               (null x.evex)))
      nil))
    t))))

Function: strict-opcode-fix

(defun strict-opcode-fix (x)
  (declare (xargs :guard (strict-opcode-p x)))
  (let ((__function__ 'strict-opcode-fix))
    (declare (ignorable __function__))
    (if (strict-opcode-p x)
        x
      (b* ((x (opcode-fix x))
           (x (change-opcode x :feat nil)))
        x))))

Theorem: strict-opcode-p-of-strict-opcode-fix

(defthm strict-opcode-p-of-strict-opcode-fix
  (strict-opcode-p (strict-opcode-fix x)))

Function: strict-opcode-equiv$inline

(defun strict-opcode-equiv$inline (x y)
  (declare (xargs :guard (and (strict-opcode-p x)
                              (strict-opcode-p y))))
  (equal (strict-opcode-fix x)
         (strict-opcode-fix y)))

Theorem: strict-opcode-equiv-is-an-equivalence

(defthm strict-opcode-equiv-is-an-equivalence
  (and (booleanp (strict-opcode-equiv x y))
       (strict-opcode-equiv x x)
       (implies (strict-opcode-equiv x y)
                (strict-opcode-equiv y x))
       (implies (and (strict-opcode-equiv x y)
                     (strict-opcode-equiv y z))
                (strict-opcode-equiv x z)))
  :rule-classes (:equivalence))

Theorem: strict-opcode-equiv-implies-equal-strict-opcode-fix-1

(defthm strict-opcode-equiv-implies-equal-strict-opcode-fix-1
  (implies (strict-opcode-equiv x x-equiv)
           (equal (strict-opcode-fix x)
                  (strict-opcode-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: strict-opcode-fix-under-strict-opcode-equiv

(defthm strict-opcode-fix-under-strict-opcode-equiv
  (strict-opcode-equiv (strict-opcode-fix x)
                       x)
  :rule-classes (:rewrite :rewrite-quoted-constant))