		Search-engine friendly clone of the ACL2 documentation.

Rflag-specifications

Zf-spec

Signature
(zf-spec result) → *

General ZF Specification (Source: Intel Manuals, Vol. 1, Section 3.4.3.1):

Zero flag Set if the result is zero; cleared otherwise.

Definitions and Theorems

Function: zf-spec$inline

(defun zf-spec$inline (result)
  (declare (type (integer 0 *) result))
  (if (equal result 0) 1 0))

Theorem: n01p-zf-spec

(defthm n01p-zf-spec
 (unsigned-byte-p 1 (zf-spec result))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (zf-spec result))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (zf-spec result))
                   (< (zf-spec result) 2))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: zf-spec-thm

(defthm zf-spec-thm
  (implies (not (equal x 0))
           (equal (zf-spec x) 0)))