Rules about uaconvert-values on values of given types.
These are not used during the symbolic execution; they are used to prove rules used during the symbolic execution.
Theorem:
(defthm uaconvert-values-when-scharp-and-scharp (implies (and (scharp x) (scharp y)) (equal (uaconvert-values x y) (mv (sint-from-schar x) (sint-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-scharp-and-ucharp (implies (and (scharp x) (ucharp y)) (equal (uaconvert-values x y) (mv (sint-from-schar x) (sint-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-scharp-and-sshortp (implies (and (scharp x) (sshortp y)) (equal (uaconvert-values x y) (mv (sint-from-schar x) (sint-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-scharp-and-ushortp (implies (and (scharp x) (ushortp y)) (equal (uaconvert-values x y) (mv (sint-from-schar x) (sint-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-scharp-and-sintp (implies (and (scharp x) (sintp y)) (equal (uaconvert-values x y) (mv (sint-from-schar x) y))))
Theorem:
(defthm uaconvert-values-when-scharp-and-uintp (implies (and (scharp x) (uintp y)) (equal (uaconvert-values x y) (mv (uint-from-schar x) y))))
Theorem:
(defthm uaconvert-values-when-scharp-and-slongp (implies (and (scharp x) (slongp y)) (equal (uaconvert-values x y) (mv (slong-from-schar x) y))))
Theorem:
(defthm uaconvert-values-when-scharp-and-ulongp (implies (and (scharp x) (ulongp y)) (equal (uaconvert-values x y) (mv (ulong-from-schar x) y))))
Theorem:
(defthm uaconvert-values-when-scharp-and-sllongp (implies (and (scharp x) (sllongp y)) (equal (uaconvert-values x y) (mv (sllong-from-schar x) y))))
Theorem:
(defthm uaconvert-values-when-scharp-and-ullongp (implies (and (scharp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-schar x) y))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-scharp (implies (and (ucharp x) (scharp y)) (equal (uaconvert-values x y) (mv (sint-from-uchar x) (sint-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-ucharp (implies (and (ucharp x) (ucharp y)) (equal (uaconvert-values x y) (mv (sint-from-uchar x) (sint-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-sshortp (implies (and (ucharp x) (sshortp y)) (equal (uaconvert-values x y) (mv (sint-from-uchar x) (sint-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-ushortp (implies (and (ucharp x) (ushortp y)) (equal (uaconvert-values x y) (mv (sint-from-uchar x) (sint-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-sintp (implies (and (ucharp x) (sintp y)) (equal (uaconvert-values x y) (mv (sint-from-uchar x) y))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-uintp (implies (and (ucharp x) (uintp y)) (equal (uaconvert-values x y) (mv (uint-from-uchar x) y))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-slongp (implies (and (ucharp x) (slongp y)) (equal (uaconvert-values x y) (mv (slong-from-uchar x) y))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-ulongp (implies (and (ucharp x) (ulongp y)) (equal (uaconvert-values x y) (mv (ulong-from-uchar x) y))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-sllongp (implies (and (ucharp x) (sllongp y)) (equal (uaconvert-values x y) (mv (sllong-from-uchar x) y))))
Theorem:
(defthm uaconvert-values-when-ucharp-and-ullongp (implies (and (ucharp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-uchar x) y))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-scharp (implies (and (sshortp x) (scharp y)) (equal (uaconvert-values x y) (mv (sint-from-sshort x) (sint-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-ucharp (implies (and (sshortp x) (ucharp y)) (equal (uaconvert-values x y) (mv (sint-from-sshort x) (sint-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-sshortp (implies (and (sshortp x) (sshortp y)) (equal (uaconvert-values x y) (mv (sint-from-sshort x) (sint-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-ushortp (implies (and (sshortp x) (ushortp y)) (equal (uaconvert-values x y) (mv (sint-from-sshort x) (sint-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-sintp (implies (and (sshortp x) (sintp y)) (equal (uaconvert-values x y) (mv (sint-from-sshort x) y))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-uintp (implies (and (sshortp x) (uintp y)) (equal (uaconvert-values x y) (mv (uint-from-sshort x) y))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-slongp (implies (and (sshortp x) (slongp y)) (equal (uaconvert-values x y) (mv (slong-from-sshort x) y))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-ulongp (implies (and (sshortp x) (ulongp y)) (equal (uaconvert-values x y) (mv (ulong-from-sshort x) y))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-sllongp (implies (and (sshortp x) (sllongp y)) (equal (uaconvert-values x y) (mv (sllong-from-sshort x) y))))
Theorem:
(defthm uaconvert-values-when-sshortp-and-ullongp (implies (and (sshortp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-sshort x) y))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-scharp (implies (and (ushortp x) (scharp y)) (equal (uaconvert-values x y) (mv (sint-from-ushort x) (sint-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-ucharp (implies (and (ushortp x) (ucharp y)) (equal (uaconvert-values x y) (mv (sint-from-ushort x) (sint-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-sshortp (implies (and (ushortp x) (sshortp y)) (equal (uaconvert-values x y) (mv (sint-from-ushort x) (sint-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-ushortp (implies (and (ushortp x) (ushortp y)) (equal (uaconvert-values x y) (mv (sint-from-ushort x) (sint-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-sintp (implies (and (ushortp x) (sintp y)) (equal (uaconvert-values x y) (mv (sint-from-ushort x) y))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-uintp (implies (and (ushortp x) (uintp y)) (equal (uaconvert-values x y) (mv (uint-from-ushort x) y))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-slongp (implies (and (ushortp x) (slongp y)) (equal (uaconvert-values x y) (mv (slong-from-ushort x) y))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-ulongp (implies (and (ushortp x) (ulongp y)) (equal (uaconvert-values x y) (mv (ulong-from-ushort x) y))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-sllongp (implies (and (ushortp x) (sllongp y)) (equal (uaconvert-values x y) (mv (sllong-from-ushort x) y))))
Theorem:
(defthm uaconvert-values-when-ushortp-and-ullongp (implies (and (ushortp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-ushort x) y))))
Theorem:
(defthm uaconvert-values-when-sintp-and-scharp (implies (and (sintp x) (scharp y)) (equal (uaconvert-values x y) (mv x (sint-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-sintp-and-ucharp (implies (and (sintp x) (ucharp y)) (equal (uaconvert-values x y) (mv x (sint-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-sintp-and-sshortp (implies (and (sintp x) (sshortp y)) (equal (uaconvert-values x y) (mv x (sint-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-sintp-and-ushortp (implies (and (sintp x) (ushortp y)) (equal (uaconvert-values x y) (mv x (sint-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-sintp-and-sintp (implies (and (sintp x) (sintp y)) (equal (uaconvert-values x y) (mv x y))))
Theorem:
(defthm uaconvert-values-when-sintp-and-uintp (implies (and (sintp x) (uintp y)) (equal (uaconvert-values x y) (mv (uint-from-sint x) y))))
Theorem:
(defthm uaconvert-values-when-sintp-and-slongp (implies (and (sintp x) (slongp y)) (equal (uaconvert-values x y) (mv (slong-from-sint x) y))))
Theorem:
(defthm uaconvert-values-when-sintp-and-ulongp (implies (and (sintp x) (ulongp y)) (equal (uaconvert-values x y) (mv (ulong-from-sint x) y))))
Theorem:
(defthm uaconvert-values-when-sintp-and-sllongp (implies (and (sintp x) (sllongp y)) (equal (uaconvert-values x y) (mv (sllong-from-sint x) y))))
Theorem:
(defthm uaconvert-values-when-sintp-and-ullongp (implies (and (sintp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-sint x) y))))
Theorem:
(defthm uaconvert-values-when-uintp-and-scharp (implies (and (uintp x) (scharp y)) (equal (uaconvert-values x y) (mv x (uint-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-uintp-and-ucharp (implies (and (uintp x) (ucharp y)) (equal (uaconvert-values x y) (mv x (uint-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-uintp-and-sshortp (implies (and (uintp x) (sshortp y)) (equal (uaconvert-values x y) (mv x (uint-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-uintp-and-ushortp (implies (and (uintp x) (ushortp y)) (equal (uaconvert-values x y) (mv x (uint-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-uintp-and-sintp (implies (and (uintp x) (sintp y)) (equal (uaconvert-values x y) (mv x (uint-from-sint y)))))
Theorem:
(defthm uaconvert-values-when-uintp-and-uintp (implies (and (uintp x) (uintp y)) (equal (uaconvert-values x y) (mv x y))))
Theorem:
(defthm uaconvert-values-when-uintp-and-slongp (implies (and (uintp x) (slongp y)) (equal (uaconvert-values x y) (mv (slong-from-uint x) y))))
Theorem:
(defthm uaconvert-values-when-uintp-and-ulongp (implies (and (uintp x) (ulongp y)) (equal (uaconvert-values x y) (mv (ulong-from-uint x) y))))
Theorem:
(defthm uaconvert-values-when-uintp-and-sllongp (implies (and (uintp x) (sllongp y)) (equal (uaconvert-values x y) (mv (sllong-from-uint x) y))))
Theorem:
(defthm uaconvert-values-when-uintp-and-ullongp (implies (and (uintp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-uint x) y))))
Theorem:
(defthm uaconvert-values-when-slongp-and-scharp (implies (and (slongp x) (scharp y)) (equal (uaconvert-values x y) (mv x (slong-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-slongp-and-ucharp (implies (and (slongp x) (ucharp y)) (equal (uaconvert-values x y) (mv x (slong-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-slongp-and-sshortp (implies (and (slongp x) (sshortp y)) (equal (uaconvert-values x y) (mv x (slong-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-slongp-and-ushortp (implies (and (slongp x) (ushortp y)) (equal (uaconvert-values x y) (mv x (slong-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-slongp-and-sintp (implies (and (slongp x) (sintp y)) (equal (uaconvert-values x y) (mv x (slong-from-sint y)))))
Theorem:
(defthm uaconvert-values-when-slongp-and-uintp (implies (and (slongp x) (uintp y)) (equal (uaconvert-values x y) (mv x (slong-from-uint y)))))
Theorem:
(defthm uaconvert-values-when-slongp-and-slongp (implies (and (slongp x) (slongp y)) (equal (uaconvert-values x y) (mv x y))))
Theorem:
(defthm uaconvert-values-when-slongp-and-ulongp (implies (and (slongp x) (ulongp y)) (equal (uaconvert-values x y) (mv (ulong-from-slong x) y))))
Theorem:
(defthm uaconvert-values-when-slongp-and-sllongp (implies (and (slongp x) (sllongp y)) (equal (uaconvert-values x y) (mv (sllong-from-slong x) y))))
Theorem:
(defthm uaconvert-values-when-slongp-and-ullongp (implies (and (slongp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-slong x) y))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-scharp (implies (and (ulongp x) (scharp y)) (equal (uaconvert-values x y) (mv x (ulong-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-ucharp (implies (and (ulongp x) (ucharp y)) (equal (uaconvert-values x y) (mv x (ulong-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-sshortp (implies (and (ulongp x) (sshortp y)) (equal (uaconvert-values x y) (mv x (ulong-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-ushortp (implies (and (ulongp x) (ushortp y)) (equal (uaconvert-values x y) (mv x (ulong-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-sintp (implies (and (ulongp x) (sintp y)) (equal (uaconvert-values x y) (mv x (ulong-from-sint y)))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-uintp (implies (and (ulongp x) (uintp y)) (equal (uaconvert-values x y) (mv x (ulong-from-uint y)))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-slongp (implies (and (ulongp x) (slongp y)) (equal (uaconvert-values x y) (mv x (ulong-from-slong y)))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-ulongp (implies (and (ulongp x) (ulongp y)) (equal (uaconvert-values x y) (mv x y))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-sllongp (implies (and (ulongp x) (sllongp y)) (equal (uaconvert-values x y) (mv (ullong-from-ulong x) (ullong-from-sllong y)))))
Theorem:
(defthm uaconvert-values-when-ulongp-and-ullongp (implies (and (ulongp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-ulong x) y))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-scharp (implies (and (sllongp x) (scharp y)) (equal (uaconvert-values x y) (mv x (sllong-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-ucharp (implies (and (sllongp x) (ucharp y)) (equal (uaconvert-values x y) (mv x (sllong-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-sshortp (implies (and (sllongp x) (sshortp y)) (equal (uaconvert-values x y) (mv x (sllong-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-ushortp (implies (and (sllongp x) (ushortp y)) (equal (uaconvert-values x y) (mv x (sllong-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-sintp (implies (and (sllongp x) (sintp y)) (equal (uaconvert-values x y) (mv x (sllong-from-sint y)))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-uintp (implies (and (sllongp x) (uintp y)) (equal (uaconvert-values x y) (mv x (sllong-from-uint y)))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-slongp (implies (and (sllongp x) (slongp y)) (equal (uaconvert-values x y) (mv x (sllong-from-slong y)))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-ulongp (implies (and (sllongp x) (ulongp y)) (equal (uaconvert-values x y) (mv (ullong-from-sllong x) (ullong-from-ulong y)))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-sllongp (implies (and (sllongp x) (sllongp y)) (equal (uaconvert-values x y) (mv x y))))
Theorem:
(defthm uaconvert-values-when-sllongp-and-ullongp (implies (and (sllongp x) (ullongp y)) (equal (uaconvert-values x y) (mv (ullong-from-sllong x) y))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-scharp (implies (and (ullongp x) (scharp y)) (equal (uaconvert-values x y) (mv x (ullong-from-schar y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-ucharp (implies (and (ullongp x) (ucharp y)) (equal (uaconvert-values x y) (mv x (ullong-from-uchar y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-sshortp (implies (and (ullongp x) (sshortp y)) (equal (uaconvert-values x y) (mv x (ullong-from-sshort y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-ushortp (implies (and (ullongp x) (ushortp y)) (equal (uaconvert-values x y) (mv x (ullong-from-ushort y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-sintp (implies (and (ullongp x) (sintp y)) (equal (uaconvert-values x y) (mv x (ullong-from-sint y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-uintp (implies (and (ullongp x) (uintp y)) (equal (uaconvert-values x y) (mv x (ullong-from-uint y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-slongp (implies (and (ullongp x) (slongp y)) (equal (uaconvert-values x y) (mv x (ullong-from-slong y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-ulongp (implies (and (ullongp x) (ulongp y)) (equal (uaconvert-values x y) (mv x (ullong-from-ulong y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-sllongp (implies (and (ullongp x) (sllongp y)) (equal (uaconvert-values x y) (mv x (ullong-from-sllong y)))))
Theorem:
(defthm uaconvert-values-when-ullongp-and-ullongp (implies (and (ullongp x) (ullongp y)) (equal (uaconvert-values x y) (mv x y))))