		Search-engine friendly clone of the ACL2 documentation.

Bitops/signed-byte-p

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

Subtopics

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.