Logops-bit-functions
Versions of the standard logical operations that operate on single bits.
We provide versions of the non-trivial standard logical operations
that operate on single bits.
One reason that it is useful to introduce these operations separately from
the standard operations is the fact that lognot applied to a bitp
object never returns a bitp.
All arguments to these functions must be bitp, and we prove that
each returns a bitp integer, i.e., 0 or 1. We define each function
explicitly in terms of 0 and 1 to simplify reasoning.
Subtopics
- Simplify-bit-functions
- Rewrite: Simplification rules for all binary b- functions
including commutative rules, reductions with 1 explicit value, and reductions
for identical agruments and complemented arguments.
- B-eqv
- Equivalence (a.k.a. if and only if, xnor) for bitps.
- B-orc2
- Inclusive or of bitps, complementing the second.
- B-orc1
- Inclusive or of bitps, complementing the first.
- B-nor
- Negated or for bitps.
- B-nand
- Negated and for bitps.
- B-ite
- If-then-else for bitps.
- B-ior
- Inclusive or for bitps.
- B-andc2
- And of bitps, complementing the second.
- B-andc1
- And of bitps, complementing the first.
- B-and
- Conjunction for bitps.
- B-xor
- Exclusive or for bitps.
- B-not
- Negation for bitps.
