Some rules about array values.
Theorem:
(defthm valuep-when-uchar-arrayp (implies (uchar-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-schar-arrayp (implies (schar-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-ushort-arrayp (implies (ushort-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-sshort-arrayp (implies (sshort-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-uint-arrayp (implies (uint-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-sint-arrayp (implies (sint-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-ulong-arrayp (implies (ulong-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-slong-arrayp (implies (slong-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-ullong-arrayp (implies (ullong-arrayp x) (valuep x)))
Theorem:
(defthm valuep-when-sllong-arrayp (implies (sllong-arrayp x) (valuep x)))
Theorem:
(defthm value-kind-when-uchar-arrayp (implies (uchar-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-schar-arrayp (implies (schar-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-ushort-arrayp (implies (ushort-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-sshort-arrayp (implies (sshort-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-uint-arrayp (implies (uint-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-sint-arrayp (implies (sint-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-ulong-arrayp (implies (ulong-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-slong-arrayp (implies (slong-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-ullong-arrayp (implies (ullong-arrayp x) (equal (value-kind x) :array)))
Theorem:
(defthm value-kind-when-sllong-arrayp (implies (sllong-arrayp x) (equal (value-kind x) :array)))