16.3. Addition is Commutative
theorem add_comm (a b : DWord) : a + b = b + a := BitVec.add_comm a b
These properties let us reason about program behavior, not just encoding correctness.
theorem add_comm (a b : DWord) : a + b = b + a := BitVec.add_comm a b
These properties let us reason about program behavior, not just encoding correctness.