		Search-engine friendly clone of the ACL2 documentation.

Sparseint

Sparseint-<

Check whether the value of x is less than the value of y.

Signature
(sparseint-< x y) → less
Arguments: x — Guard (sparseint-p x).; y — Guard (sparseint-p y).
Returns: less — Type (booleanp less).

Definitions and Theorems

Function: sparseint-<$inline

(defun sparseint-<$inline (x y)
  (declare (xargs :guard (and (sparseint-p x) (sparseint-p y))))
  (let ((__function__ 'sparseint-<))
    (declare (ignorable __function__))
    (eql (sparseint-compare x y) -1)))

Theorem: booleanp-of-sparseint-<

(defthm booleanp-of-sparseint-<
  (b* ((less (sparseint-<$inline x y)))
    (booleanp less))
  :rule-classes :type-prescription)

Theorem: sparseint-<-correct

(defthm sparseint-<-correct
  (b* ((?less (sparseint-<$inline x y)))
    (equal less
           (< (sparseint-val x)
              (sparseint-val y)))))

Theorem: sparseint-<$inline-of-sparseint-fix-x

(defthm sparseint-<$inline-of-sparseint-fix-x
  (equal (sparseint-<$inline (sparseint-fix x) y)
         (sparseint-<$inline x y)))

Theorem: sparseint-<$inline-sparseint-equiv-congruence-on-x

(defthm sparseint-<$inline-sparseint-equiv-congruence-on-x
  (implies (sparseint-equiv x x-equiv)
           (equal (sparseint-<$inline x y)
                  (sparseint-<$inline x-equiv y)))
  :rule-classes :congruence)

Theorem: sparseint-<$inline-of-sparseint-fix-y

(defthm sparseint-<$inline-of-sparseint-fix-y
  (equal (sparseint-<$inline x (sparseint-fix y))
         (sparseint-<$inline x y)))

Theorem: sparseint-<$inline-sparseint-equiv-congruence-on-y

(defthm sparseint-<$inline-sparseint-equiv-congruence-on-y
  (implies (sparseint-equiv y y-equiv)
           (equal (sparseint-<$inline x y)
                  (sparseint-<$inline x y-equiv)))
  :rule-classes :congruence)