Less-than comparison of signed integer values.
Function:
(defun int-lt (left right) (declare (xargs :guard (and (intp left) (intp right)))) (declare (xargs :guard (= (int->size left) (int->size right)))) (b* ((x (int->value left)) (y (int->value right))) (bool (< x y))))
Theorem:
(defthm boolp-of-int-lt (b* ((result (int-lt left right))) (boolp result)) :rule-classes :rewrite)
Theorem:
(defthm int-lt-of-int-fix-left (equal (int-lt (int-fix left) right) (int-lt left right)))
Theorem:
(defthm int-lt-int-equiv-congruence-on-left (implies (int-equiv left left-equiv) (equal (int-lt left right) (int-lt left-equiv right))) :rule-classes :congruence)
Theorem:
(defthm int-lt-of-int-fix-right (equal (int-lt left (int-fix right)) (int-lt left right)))
Theorem:
(defthm int-lt-int-equiv-congruence-on-right (implies (int-equiv right right-equiv) (equal (int-lt left right) (int-lt left right-equiv))) :rule-classes :congruence)