Rules about array reads.
Theorem:
(defthm not-errorp-of-value-array-read-when-uchar-array-and-in-range (implies (and (uchar-arrayp array) (integerp index) (uchar-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-schar-array-and-in-range (implies (and (schar-arrayp array) (integerp index) (schar-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-ushort-array-and-in-range (implies (and (ushort-arrayp array) (integerp index) (ushort-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-sshort-array-and-in-range (implies (and (sshort-arrayp array) (integerp index) (sshort-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-uint-array-and-in-range (implies (and (uint-arrayp array) (integerp index) (uint-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-sint-array-and-in-range (implies (and (sint-arrayp array) (integerp index) (sint-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-ulong-array-and-in-range (implies (and (ulong-arrayp array) (integerp index) (ulong-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-slong-array-and-in-range (implies (and (slong-arrayp array) (integerp index) (slong-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-ullong-array-and-in-range (implies (and (ullong-arrayp array) (integerp index) (ullong-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-sllong-array-and-in-range (implies (and (sllong-arrayp array) (integerp index) (sllong-array-integer-index-okp array index)) (not (errorp (value-array-read index array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-uchar-array-and-in-range-cinteger (implies (and (uchar-arrayp array) (cintegerp index) (uchar-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-schar-array-and-in-range-cinteger (implies (and (schar-arrayp array) (cintegerp index) (schar-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-ushort-array-and-in-range-cinteger (implies (and (ushort-arrayp array) (cintegerp index) (ushort-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-sshort-array-and-in-range-cinteger (implies (and (sshort-arrayp array) (cintegerp index) (sshort-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-uint-array-and-in-range-cinteger (implies (and (uint-arrayp array) (cintegerp index) (uint-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-sint-array-and-in-range-cinteger (implies (and (sint-arrayp array) (cintegerp index) (sint-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-ulong-array-and-in-range-cinteger (implies (and (ulong-arrayp array) (cintegerp index) (ulong-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-slong-array-and-in-range-cinteger (implies (and (slong-arrayp array) (cintegerp index) (slong-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-ullong-array-and-in-range-cinteger (implies (and (ullong-arrayp array) (cintegerp index) (ullong-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm not-errorp-of-value-array-read-when-sllong-array-and-in-range-cinteger (implies (and (sllong-arrayp array) (cintegerp index) (sllong-array-index-okp array index)) (not (errorp (value-array-read (integer-from-cinteger index) array)))))
Theorem:
(defthm value-array-read-when-uchar-arrayp (implies (and (uchar-arrayp x) (cintegerp i) (uchar-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (uchar-array-read x i))))
Theorem:
(defthm value-array-read-when-schar-arrayp (implies (and (schar-arrayp x) (cintegerp i) (schar-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (schar-array-read x i))))
Theorem:
(defthm value-array-read-when-ushort-arrayp (implies (and (ushort-arrayp x) (cintegerp i) (ushort-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (ushort-array-read x i))))
Theorem:
(defthm value-array-read-when-sshort-arrayp (implies (and (sshort-arrayp x) (cintegerp i) (sshort-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (sshort-array-read x i))))
Theorem:
(defthm value-array-read-when-uint-arrayp (implies (and (uint-arrayp x) (cintegerp i) (uint-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (uint-array-read x i))))
Theorem:
(defthm value-array-read-when-sint-arrayp (implies (and (sint-arrayp x) (cintegerp i) (sint-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (sint-array-read x i))))
Theorem:
(defthm value-array-read-when-ulong-arrayp (implies (and (ulong-arrayp x) (cintegerp i) (ulong-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (ulong-array-read x i))))
Theorem:
(defthm value-array-read-when-slong-arrayp (implies (and (slong-arrayp x) (cintegerp i) (slong-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (slong-array-read x i))))
Theorem:
(defthm value-array-read-when-ullong-arrayp (implies (and (ullong-arrayp x) (cintegerp i) (ullong-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (ullong-array-read x i))))
Theorem:
(defthm value-array-read-when-sllong-arrayp (implies (and (sllong-arrayp x) (cintegerp i) (sllong-array-index-okp x i)) (equal (value-array-read (integer-from-cinteger i) x) (sllong-array-read x i))))