		Search-engine friendly clone of the ACL2 documentation.

Arith-equivs

Nat-equiv

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

Definitions and Theorems

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

Subtopics

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