		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Int-gt

Greater-than comparison of signed integer values.

Signature
(int-gt left right) → result
Arguments: left — Guard (intp left).; right — Guard (intp right).
Returns: result — Type (boolp result).

Definitions and Theorems

Function: int-gt

(defun int-gt (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: boolp-of-int-gt

(defthm boolp-of-int-gt
  (b* ((result (int-gt left right)))
    (boolp result))
  :rule-classes :rewrite)

Theorem: int-gt-of-int-fix-left

(defthm int-gt-of-int-fix-left
  (equal (int-gt (int-fix left) right)
         (int-gt left right)))

Theorem: int-gt-int-equiv-congruence-on-left

(defthm int-gt-int-equiv-congruence-on-left
  (implies (int-equiv left left-equiv)
           (equal (int-gt left right)
                  (int-gt left-equiv right)))
  :rule-classes :congruence)

Theorem: int-gt-of-int-fix-right

(defthm int-gt-of-int-fix-right
  (equal (int-gt left (int-fix right))
         (int-gt left right)))

Theorem: int-gt-int-equiv-congruence-on-right

(defthm int-gt-int-equiv-congruence-on-right
  (implies (int-equiv right right-equiv)
           (equal (int-gt left right)
                  (int-gt left right-equiv)))
  :rule-classes :congruence)