		Search-engine friendly clone of the ACL2 documentation.

Rflags-reads-and-writes

Undef-flg

Signature
(undef-flg x86) → (mv unknown-bit x86)
Returns: unknown-bit — Type (bitp unknown-bit).; x86 — Type (x86p x86), given (x86p x86).

Definitions and Theorems

Function: undef-flg$notinline

(defun undef-flg$notinline (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'undef-flg))
    (declare (ignorable __function__))
    (b* (((mv val x86) (undef-flg-logic x86)))
      (mv (n01 val) x86))))

Theorem: bitp-of-undef-flg.unknown-bit

(defthm bitp-of-undef-flg.unknown-bit
  (b* (((mv ?unknown-bit ?x86)
        (undef-flg$notinline x86)))
    (bitp unknown-bit))
  :rule-classes :type-prescription)

Theorem: x86p-of-undef-flg.x86

(defthm x86p-of-undef-flg.x86
  (implies (x86p x86)
           (b* (((mv ?unknown-bit ?x86)
                 (undef-flg$notinline x86)))
             (x86p x86)))
  :rule-classes :rewrite)