Lemmas about signed-byte-p and unsigned-byte-p that are often useful when optimizing definitions with ACL2::type-spec declarations.

- Basic-signed-byte-p-of-binary-minus
- Subtracting N-bit signeds creates an N+1 bit signed.
- Basic-unsigned-byte-p-of-*
- Multiplying constant N * N bit unsigneds creates an N+N bit unsigned.
- Basic-signed-byte-p-of-*
- Multiplying constant N * N bit signeds creates an N+N bit signed.
- Basic-signed-byte-p-of-unary-minus
- Negative N-bit signed is an N+1 bit signed.
- Basic-signed-byte-p-of-mixed-*
- Multiplying constant N-bit signed * N-bit unsigned creates an N+N bit signed.
- Basic-unsigned-byte-p-of-+-with-cin
- Adding N-bit unsigneds with a carry bit creates an N+1 bit unsigned.
- Lousy-signed-byte-p-of-*
- Multiplying N * N bit signeds creates an N+N bit signed.
- Lousy-signed-byte-p-of-mixed-*
- Multiplying N-bit signed * N-bit unsigned creates an N+N bit signed.
- Basic-signed-byte-p-of-+-with-cin
- Adding N+1 bit signeds with a carry bit creates an N+1 bit signed.
- Basic-signed-byte-p-of-unary-minus-2
- Negative N-bit unsigned is an N+1 bit signed.
- Lousy-unsigned-byte-p-of-*-mixed
- Multiplying N1 * N2 bit unsigneds creates an N1+N2 bit unsigned.
- Lousy-unsigned-byte-p-of-*
- Multiplying N * N bit unsigneds creates an N+N bit unsigned.
- Basic-signed-byte-p-of-+
- Adding N-bit signeds creates an N+1 bit signed.
- Basic-signed-byte-p-of-truncate-split
- Truncate of an N-bit signed by an integer is
**usually**an N-bit signed. (Strong form, case splitting, disabled by default). - Basic-unsigned-byte-p-of-+
- Adding N-bit unsigneds creates an N+1 bit unsigned.
- Basic-signed-byte-p-of-floor-split
- Floor of an N-bit signed by an integer is
**usually**an N-bit signed. (Strong form, case splitting, disabled by default). - Basic-signed-byte-p-of-truncate
- Truncating an N-bit signed by an integer is
**usually**an N-bit signed. (Weak form, enabled by default). - Basic-signed-byte-p-of-floor
- Floor of an N-bit signed by an integer is
**usually**an N-bit signed. (Weak form, enabled by default). - Unsigned-byte-p-of-minus-when-signed-byte-p
- Negating an N-bit signed creates an N-bit unsigned exactly when it was negative.
- Signed-byte-p-of-decrement-when-natural-signed-byte-p
- Decrementing a positive N-bit signed creates an N-bit signed.
- Unsigned-byte-p-of-abs-when-signed-byte-p
- Absolute value of an N-bit signed is an N-bit unsigned.
- Signed-byte-p-when-unsigned-byte-p-smaller
- An N-bit unsigned is an M-big signed for any
M < N . - Signed-byte-p-when-signed-byte-p-smaller
- An N-bit signed is an M-bit signed for any
M >= N . - Signed-byte-p-of-loghead
- An N-bit loghead is an M-bit signed for any
M > N . - Basic-unsigned-byte-p-of-truncate
- Truncate an N-bit unsigned by a natural creates an N-bit unsigned.
- Basic-unsigned-byte-p-of-rem
- Remainder of an N-bit unsigned by a natural creates an N-bit unsigned.
- Basic-unsigned-byte-p-of-mod
- Mod an N-bit unsigned by a natural creates an N-bit unsigned.
- Basic-unsigned-byte-p-of-floor
- Floor an N-bit unsigned by a natural creates an N-bit unsigned.
- Basic-signed-byte-p-of-rem
- Rem of N-bit signed by N-bit signed creates an N-bit signed.
- Basic-signed-byte-p-of-mod
- Mod of N-bit signed by N-bit signed creates an N-bit signed.
- Basic-signed-byte-p-of-lognot
- Lognot of an N-bit unsigned is an N+1 bit signed.
- Basic-signed-byte-p-of-1+lognot
- Lognot+1 (two's complement) of an N-bit unsigned is an N+1 bit signed.