		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Compare

Signature
(compare x y) → *
Arguments: x — Guard (integerp x).; y — Guard (integerp y).

Definitions and Theorems

Function: compare

(defun compare (x y)
  (declare (xargs :guard (and (integerp x) (integerp y))))
  (let ((__function__ 'compare))
    (declare (ignorable __function__))
    (b* ((x (lifix x)) (y (lifix y)))
      (cond ((eql x y) 0)
            ((< x y) -1)
            (t 1)))))

Theorem: minus-of-compare

(defthm minus-of-compare
  (equal (- (compare x y)) (compare y x)))

Theorem: compare-of-ifix-x

(defthm compare-of-ifix-x
  (equal (compare (ifix x) y)
         (compare x y)))

Theorem: compare-int-equiv-congruence-on-x

(defthm compare-int-equiv-congruence-on-x
  (implies (int-equiv x x-equiv)
           (equal (compare x y)
                  (compare x-equiv y)))
  :rule-classes :congruence)

Theorem: compare-of-ifix-y

(defthm compare-of-ifix-y
  (equal (compare x (ifix y))
         (compare x y)))

Theorem: compare-int-equiv-congruence-on-y

(defthm compare-int-equiv-congruence-on-y
  (implies (int-equiv y y-equiv)
           (equal (compare x y)
                  (compare x y-equiv)))
  :rule-classes :congruence)