		Search-engine friendly clone of the ACL2 documentation.

Values

Bounds-of-integer-values

Linear rules about the bounds of the integer values.

Definitions and Theorems

Theorem: value-schar->get-bound

(defthm value-schar->get-bound
  (and (<= (schar-min) (value-schar->get x))
       (<= (value-schar->get x) (schar-max)))
  :rule-classes :linear)

Theorem: value-uchar->get-bound

(defthm value-uchar->get-bound
  (and (<= 0 (value-uchar->get x))
       (<= (value-uchar->get x) (uchar-max)))
  :rule-classes :linear)

Theorem: value-sshort->get-bound

(defthm value-sshort->get-bound
  (and (<= (sshort-min) (value-sshort->get x))
       (<= (value-sshort->get x) (sshort-max)))
  :rule-classes :linear)

Theorem: value-ushort->get-bound

(defthm value-ushort->get-bound
  (and (<= 0 (value-ushort->get x))
       (<= (value-ushort->get x) (ushort-max)))
  :rule-classes :linear)

Theorem: value-sint->get-bound

(defthm value-sint->get-bound
  (and (<= (sint-min) (value-sint->get x))
       (<= (value-sint->get x) (sint-max)))
  :rule-classes :linear)

Theorem: value-uint->get-bound

(defthm value-uint->get-bound
  (and (<= 0 (value-uint->get x))
       (<= (value-uint->get x) (uint-max)))
  :rule-classes :linear)

Theorem: value-slong->get-bound

(defthm value-slong->get-bound
  (and (<= (slong-min) (value-slong->get x))
       (<= (value-slong->get x) (slong-max)))
  :rule-classes :linear)

Theorem: value-ulong->get-bound

(defthm value-ulong->get-bound
  (and (<= 0 (value-ulong->get x))
       (<= (value-ulong->get x) (ulong-max)))
  :rule-classes :linear)

Theorem: value-sllong->get-bound

(defthm value-sllong->get-bound
  (and (<= (sllong-min) (value-sllong->get x))
       (<= (value-sllong->get x) (sllong-max)))
  :rule-classes :linear)

Theorem: value-ullong->get-bound

(defthm value-ullong->get-bound
  (and (<= 0 (value-ullong->get x))
       (<= (value-ullong->get x) (ullong-max)))
  :rule-classes :linear)