Rules to simplify ifix applied to accessors of C integers.
The rule
Theorem:
(defthm ifix-of-integer-from-schar (equal (ifix (integer-from-schar x)) (integer-from-schar x)))
Theorem:
(defthm ifix-of-integer-from-uchar (equal (ifix (integer-from-uchar x)) (integer-from-uchar x)))
Theorem:
(defthm ifix-of-integer-from-sshort (equal (ifix (integer-from-sshort x)) (integer-from-sshort x)))
Theorem:
(defthm ifix-of-integer-from-ushort (equal (ifix (integer-from-ushort x)) (integer-from-ushort x)))
Theorem:
(defthm ifix-of-integer-from-sint (equal (ifix (integer-from-sint x)) (integer-from-sint x)))
Theorem:
(defthm ifix-of-integer-from-uint (equal (ifix (integer-from-uint x)) (integer-from-uint x)))
Theorem:
(defthm ifix-of-integer-from-slong (equal (ifix (integer-from-slong x)) (integer-from-slong x)))
Theorem:
(defthm ifix-of-integer-from-ulong (equal (ifix (integer-from-ulong x)) (integer-from-ulong x)))
Theorem:
(defthm ifix-of-integer-from-sllong (equal (ifix (integer-from-sllong x)) (integer-from-sllong x)))
Theorem:
(defthm ifix-of-integer-from-ullong (equal (ifix (integer-from-ullong x)) (integer-from-ullong x)))