Rules for executing casts.
Theorem:
(defthm exec-cast-of-schar-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-schar-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x) (schar-from-uchar-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-schar-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x) (schar-from-sshort-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-schar-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x) (schar-from-ushort-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-schar-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x) (schar-from-sint-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-schar-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x) (schar-from-uint-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-schar-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x) (schar-from-slong-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-schar-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x) (schar-from-ulong-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-schar-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x) (schar-from-sllong-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-schar-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x) (schar-from-ullong-okp x)) (equal (exec-cast '(:tyname (tyspec :schar) (declor :none)) (expr-value x objdes)) (expr-value (schar-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-uchar-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-uchar-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x)) (equal (exec-cast '(:tyname (tyspec :uchar) (declor :none)) (expr-value x objdes)) (expr-value (uchar-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x) (sshort-from-uchar-okp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-sshort-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x) (sshort-from-ushort-okp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x) (sshort-from-sint-okp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x) (sshort-from-uint-okp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x) (sshort-from-slong-okp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x) (sshort-from-ulong-okp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x) (sshort-from-sllong-okp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-sshort-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x) (sshort-from-ullong-okp x)) (equal (exec-cast '(:tyname (tyspec :sshort nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sshort-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-ushort-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-ushort-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x)) (equal (exec-cast '(:tyname (tyspec :ushort nil) (declor :none)) (expr-value x objdes)) (expr-value (ushort-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x) (sint-from-uchar-okp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x) (sint-from-ushort-okp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-sint-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x) (sint-from-uint-okp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x) (sint-from-slong-okp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x) (sint-from-ulong-okp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x) (sint-from-sllong-okp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-sint-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x) (sint-from-ullong-okp x)) (equal (exec-cast '(:tyname (tyspec :sint nil t) (declor :none)) (expr-value x objdes)) (expr-value (sint-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-uint-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-uint-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x)) (equal (exec-cast '(:tyname (tyspec :uint t) (declor :none)) (expr-value x objdes)) (expr-value (uint-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x) (slong-from-uchar-okp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x) (slong-from-ushort-okp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x) (slong-from-uint-okp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-slong-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x) (slong-from-ulong-okp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x) (slong-from-sllong-okp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-slong-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x) (slong-from-ullong-okp x)) (equal (exec-cast '(:tyname (tyspec :slong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (slong-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-ulong-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-ulong-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x)) (equal (exec-cast '(:tyname (tyspec :ulong nil) (declor :none)) (expr-value x objdes)) (expr-value (ulong-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x) (sllong-from-uchar-okp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x) (sllong-from-ushort-okp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x) (sllong-from-uint-okp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x) (sllong-from-ulong-okp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-sllong-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value x nil))))
Theorem:
(defthm exec-cast-of-sllong-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x) (sllong-from-ullong-okp x)) (equal (exec-cast '(:tyname (tyspec :sllong nil nil) (declor :none)) (expr-value x objdes)) (expr-value (sllong-from-ullong x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-schar x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-uchar x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-sshort x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-ushort x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-sint x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-uint x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-slong x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-ulong x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value (ullong-from-sllong x) nil))))
Theorem:
(defthm exec-cast-of-ullong-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x)) (equal (exec-cast '(:tyname (tyspec :ullong nil) (declor :none)) (expr-value x objdes)) (expr-value x nil))))