		Search-engine friendly clone of the ACL2 documentation.

Arith-equivs

Bit-equiv

Equivalence under bfix, i.e., bit equivalence.

Definitions and Theorems

Theorem: nat-equiv-refines-bit-equiv

(defthm nat-equiv-refines-bit-equiv
        (implies (nat-equiv x y)
                 (bit-equiv x y))
        :rule-classes (:refinement))

Theorem: bit-equiv-implies-equal-zbp-1

(defthm bit-equiv-implies-equal-zbp-1
        (implies (bit-equiv a a-equiv)
                 (equal (zbp a) (zbp a-equiv)))
        :rule-classes (:congruence))