		Search-engine friendly clone of the ACL2 documentation.

Int-value-bound-theorems

Theorems about the bounds of the integer values.

Theorem: value-i8-lower-bound

(defthm value-i8-lower-bound
  (<= -128 (value-i8->get x))
  :rule-classes :linear)

Theorem: value-i8-upper-bound

(defthm value-i8-upper-bound
  (<= (value-i8->get x) 127)
  :rule-classes :linear)

Theorem: value-i16-lower-bound

(defthm value-i16-lower-bound
  (<= -32768 (value-i16->get x))
  :rule-classes :linear)

Theorem: value-i16-upper-bound

(defthm value-i16-upper-bound
  (<= (value-i16->get x) 32767)
  :rule-classes :linear)

Theorem: value-i32-lower-bound

(defthm value-i32-lower-bound
  (<= -2147483648 (value-i32->get x))
  :rule-classes :linear)

Theorem: value-i32-upper-bound

(defthm value-i32-upper-bound
  (<= (value-i32->get x) 2147483647)
  :rule-classes :linear)

Theorem: value-i64-lower-bound

(defthm value-i64-lower-bound
  (<= -9223372036854775808 (value-i64->get x))
  :rule-classes :linear)

Theorem: value-i64-upper-bound

(defthm value-i64-upper-bound
  (<= (value-i64->get x)
      9223372036854775807)
  :rule-classes :linear)

Theorem: value-i128-lower-bound

(defthm value-i128-lower-bound
  (<= -170141183460469231731687303715884105728
      (value-i128->get x))
  :rule-classes :linear)

Theorem: value-i128-upper-bound

(defthm value-i128-upper-bound
  (<= (value-i128->get x)
      170141183460469231731687303715884105727)
  :rule-classes :linear)