		Search-engine friendly clone of the ACL2 documentation.

Bit-equiv

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

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))