• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
      • Lispfloat
      • Arithmetic-1
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
        • Nat-equiv
        • Bit->bool
        • Bit-equiv
        • Int-equiv
        • Negp
        • Bool->bit
      • Include-an-arithmetic-book
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra
  • Testing-utilities

• Arithmetic
• Std/basic

Arith-equivs

Definitions for congruence reasoning about integers/naturals/bits.

Note: to use this book at full strength, do:

(include-book "std/basic/arith-equivs" :dir :system)
(local (in-theory (enable* arith-equiv-forwarding)))

You can also load just the definitions and bare-minimum theorems using

(include-book "std/basic/arith-equiv-defs" :dir :system)

Subtopics

Nat-equiv

Equivalence under nfix, i.e., natural number equivalence.

Bit->bool

Coerce a bit into a Boolean.

Bit-equiv

Equivalence under bfix, i.e., bit equivalence.

Int-equiv

Equivalence under ifix, i.e., integer equivalence.

Negp

Recognizer for negative integers.

Bool->bit

Coerce a Boolean into a bitp.