Rules about disjointness of array values.
Theorem:
(defthm not-schar-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (ullong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-uchar-arrayp (implies (uchar-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (ullong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-schar-arrayp (implies (schar-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-schar-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (ullong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-ushort-arrayp (implies (ushort-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-schar-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (ullong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-sshort-arrayp (implies (sshort-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-schar-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (ullong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-uint-arrayp (implies (uint-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-schar-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (ullong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-sint-arrayp (implies (sint-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-schar-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (ullong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-ulong-arrayp (implies (ulong-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-schar-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (ullong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-slong-arrayp (implies (slong-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-schar-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-sllong-arrayp-when-ullong-arrayp (implies (ullong-arrayp x) (not (sllong-arrayp x))))
Theorem:
(defthm not-uchar-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (uchar-arrayp x))))
Theorem:
(defthm not-schar-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (schar-arrayp x))))
Theorem:
(defthm not-ushort-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (ushort-arrayp x))))
Theorem:
(defthm not-sshort-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (sshort-arrayp x))))
Theorem:
(defthm not-uint-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (uint-arrayp x))))
Theorem:
(defthm not-sint-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (sint-arrayp x))))
Theorem:
(defthm not-ulong-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (ulong-arrayp x))))
Theorem:
(defthm not-slong-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (slong-arrayp x))))
Theorem:
(defthm not-ullong-arrayp-when-sllong-arrayp (implies (sllong-arrayp x) (not (ullong-arrayp x))))