		Search-engine friendly clone of the ACL2 documentation.

Boolean-neq

Boolean-neq-correctness

Correctness of the circuit.

We expand the boolean non-equality predicate to the boolean exclusive disjunction predicate, and we use its correctness theorem to rewrite it to its specification. We expand both specifications, which are equal.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: boolean-neq-pred-to-spec

(defthm boolean-neq-pred-to-spec
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (pfield::fep z prime)
                (bitp x)
                (bitp y))
           (equal (boolean-neq-pred x y z prime)
                  (boolean-neq-spec x y z prime))))

Theorem: boolean-neq-circuit-to-spec

(defthm boolean-neq-circuit-to-spec
  (implies
       (and (equal (pfcs::lookup-definition (pfname "boolean_neq")
                                            defs)
                   (boolean-neq-circuit))
            (equal (pfcs::lookup-definition (pfname "boolean_xor")
                                            defs)
                   (boolean-xor-circuit))
            (primep prime)
            (pfield::fep x prime)
            (pfield::fep y prime)
            (pfield::fep z prime)
            (bitp x)
            (bitp y))
       (equal (pfcs::definition-satp (pfname "boolean_neq")
                                     defs (list x y z)
                                     prime)
              (boolean-neq-spec x y z prime))))