		Search-engine friendly clone of the ACL2 documentation.

2vecnatx

2vecnatx-equiv

Equivalence up to 2vecnatx-fix.

This is a universal equivalence, introduced using def-universal-equiv.

Function: 2vecnatx-equiv

(defun 2vecnatx-equiv (x y)
  (and (equal (2vecnatx-fix x)
              (2vecnatx-fix y))))

Definitions and Theorems

Function: 2vecnatx-equiv

(defun 2vecnatx-equiv (x y)
  (and (equal (2vecnatx-fix x)
              (2vecnatx-fix y))))

Theorem: 2vecnatx-equiv-is-an-equivalence

(defthm 2vecnatx-equiv-is-an-equivalence
  (and (booleanp (2vecnatx-equiv x y))
       (2vecnatx-equiv x x)
       (implies (2vecnatx-equiv x y)
                (2vecnatx-equiv y x))
       (implies (and (2vecnatx-equiv x y)
                     (2vecnatx-equiv y z))
                (2vecnatx-equiv x z)))
  :rule-classes (:equivalence))

Theorem: 2vecx-equiv-refines-2vecnatx-equiv

(defthm 2vecx-equiv-refines-2vecnatx-equiv
  (implies (2vecx-equiv x y)
           (2vecnatx-equiv x y))
  :rule-classes (:refinement))

Theorem: 2vecnatx-equiv-implies-equal-2vecnatx-fix-1

(defthm 2vecnatx-equiv-implies-equal-2vecnatx-fix-1
  (implies (2vecnatx-equiv x x-equiv)
           (equal (2vecnatx-fix x)
                  (2vecnatx-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: __deffixtype-2vecnatx-equiv-means-equal-of-2vecnatx-fix

(defthm
      acl2::__deffixtype-2vecnatx-equiv-means-equal-of-2vecnatx-fix
  (implies (2vecnatx-equiv x y)
           (equal (2vecnatx-fix x)
                  (2vecnatx-fix y)))
  :rule-classes nil)