		Search-engine friendly clone of the ACL2 documentation.

Boolean-assert-neq

Boolean-assert-neq-correctness

Correctness of the circuit.

Soundness is proved by expanding the existentially quantified boolean non-equality assertion predicate to the boolean non-equality and truth assertion predicates, using the correcness theorems of the latter two, and expanding all three specifications.

Completeness is proved also by expanding the boolean non-equality and truth assertion predicates and all the specifications, but we we use the suff theorem for the boolean non-equality assertion predicate. The witness for the existential quantification is the result of comparing the two operands for non-equality.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: boolean-assert-neq-pred-soundness

(defthm boolean-assert-neq-pred-soundness
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (bitp x)
                (bitp y))
           (implies (boolean-assert-neq-pred x y prime)
                    (boolean-assert-neq-spec x y prime))))

Theorem: boolean-assert-neq-pred-completeness

(defthm boolean-assert-neq-pred-completeness
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (bitp x)
                (bitp y))
           (implies (boolean-assert-neq-spec x y prime)
                    (boolean-assert-neq-pred x y prime))))

Theorem: boolean-assert-neq-pred-to-spec

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

Theorem: boolean-assert-neq-circuit-to-spec

(defthm boolean-assert-neq-circuit-to-spec
 (implies
  (and
      (equal (pfcs::lookup-definition (pfname "boolean_assert_neq")
                                      defs)
             (boolean-assert-neq-circuit))
      (equal (pfcs::lookup-definition (pfname "boolean_assert_true")
                                      defs)
             (boolean-assert-true-circuit))
      (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)
      (bitp x)
      (bitp y))
  (equal (pfcs::definition-satp (pfname "boolean_assert_neq")
                                defs (list x y)
                                prime)
         (boolean-assert-neq-spec x y prime))))