		Search-engine friendly clone of the ACL2 documentation.

Nat-equiv

Equivalence under nfix, i.e., natural number equivalence.

Theorem: int-equiv-refines-nat-equiv

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

Theorem: nat-equiv-implies-equal-zp-1

(defthm nat-equiv-implies-equal-zp-1
  (implies (nat-equiv a a-equiv)
           (equal (zp a) (zp a-equiv)))
  :rule-classes (:congruence))

Nats-equiv: Recognizer for lists that are the same length and that are pairwise equivalent up to nfix.