		Search-engine friendly clone of the ACL2 documentation.

Boolean-if

Boolean-if-correctness

Correctness of the circuit.

The equivalence between predicate and specification is proved automatically via the prime fields library rules.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: boolean-if-pred-to-spec

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

Theorem: boolean-if-circuit-to-spec

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