		Search-engine friendly clone of the ACL2 documentation.

Logops

Logops-lemmas

A book of lemmas about logical operations on numbers.

Subtopics

Logops-recursive-definitions-theory: Recursive equivalents of logical operations.
Ihs/logbitp-lemmas: Lemmas about logbitp and logbit from the logops-lemmas book.
Ihs/logtail-lemmas: Lemmas about logtail from the logops-lemmas book.
Ihs/loghead-lemmas: Lemmas about loghead from the logops-lemmas book.
Ihs/logrpl-lemmas: Lemmas about logrpl from the logops-lemmas book.
Ihs/logand-lemmas: Lemmas about logand from the logops-lemmas book.
Ihs/logapp-lemmas: Lemmas about logapp from the logops-lemmas book.
Ihs/logcar-lemmas: Lemmas about logcar from the logops-lemmas book.
Ihs/integer-length-lemmas: Lemmas about integer-length from the logops-lemmas book.
Ihs/unsigned-byte-p-lemmas: Lemmas about unsigned-byte-p from the logops-lemmas book.
Ihs/logcons-lemmas: Basic lemmas relating logcons to logcar and logcdr, from the logops-lemmas book.
Signed-byte-p-logops: Lemmas showing the basic preservation of signed-byte-p by operations like logand, logior, etc.
Ihs/logxor-lemmas: Lemmas about logxor from the logops-lemmas book.
Ihs/logior-lemmas: Lemmas about logior from the logops-lemmas book.
Ihs/logext-lemmas: Lemmas about logext from the logops-lemmas book.
Ihs/logextu-lemmas: Lemmas about logextu from the logops-lemmas book.
Ihs/signed-byte-p-lemmas: Lemmas about signed-byte-p from the logops-lemmas book.
Ihs/lognotu-lemmas: Lemmas about lognotu from the logops-lemmas book.
Ihs/lognot-lemmas: Lemmas about lognot from the logops-lemmas book.
Ihs/logmaskp-lemmas: Lemmas about logmaskp from the logops-lemmas book.
Ihs/ash-lemmas: Lemmas about ash from the logops-lemmas book.
Logops-lemmas-theory: The "minimal" theory for the logops-lemmas book.
Ihs/wrb-lemmas
Ihs/logite-lemmas: Lemmas about logite from the logops-lemmas book.