theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.neg_eq_not_add_one {x : BitVec 32} : -x = ~~~x + 1

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.neg_eq_neg_not_one {x : BitVec 32} : -x = ~~~(x - 1)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.not_eq_neg_sub_one {x : BitVec 32} : ~~~x = -x - 1

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.neg_not_eq_add_one {x : BitVec 32} : -~~~x = x + 1

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.not_neg_eq_sub_one {x : BitVec 32} : ~~~(-x) = x - 1

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.add_eq_sub_not_sub_one {x : BitVec 32} {y : BitVec 32} : x + y = x - ~~~y - 1

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.add_eq_xor_add_mul_and {x : BitVec 32} {y : BitVec 32} : x + y = (x ^^^ y) + 2 * (x &&& y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.add_eq_or_add_and {x : BitVec 32} {y : BitVec 32} : x + y = (x ||| y) + (x &&& y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.add_eq_mul_or_neg_xor {x : BitVec 32} {y : BitVec 32} : x + y = 2 * (x ||| y) - (x ^^^ y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.sub_eq_add_not_add_one {x : BitVec 32} {y : BitVec 32} : x - y = x + ~~~y + 1

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.sub_eq_xor_sub_mul_not_and {x : BitVec 32} {y : BitVec 32} : x - y = (x ^^^ y) - 2 * (~~~x &&& y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.sub_eq_and_not_sub_not_and {x : BitVec 32} {y : BitVec 32} : x - y = (x &&& ~~~y) - (~~~x &&& y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.sub_eq_mul_and_not_sub_xor {x : BitVec 32} {y : BitVec 32} : x - y = 2 * (x &&& ~~~y) - (x ^^^ y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.xor_eq_or_sub_and {x : BitVec 32} {y : BitVec 32} : x ^^^ y = (x ||| y) - (x &&& y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.and_not_eq_or_sub {x : BitVec 32} {y : BitVec 32} : x &&& ~~~y = (x ||| y) - y

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.and_not_eq_sub_add {x : BitVec 32} {y : BitVec 32} : x &&& ~~~y = x - (x &&& y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.not_sub_eq_sub_sub_one {x : BitVec 32} {y : BitVec 32} : ~~~(x - y) = y - x - 1

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.not_sub_eq_not_add {x : BitVec 32} {y : BitVec 32} : ~~~(x - y) = ~~~x + y

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.not_xor_eq_and_sub_or_sub_one {x : BitVec 32} {y : BitVec 32} : ~~~(x ^^^ y) = (x &&& y) - (x ||| y) - 1

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.not_xor_eq_and_add_not_or {x : BitVec 32} {y : BitVec 32} : ~~~(x ^^^ y) = (x &&& y) + ~~~(x ||| y)

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.or_eq_and_not_add {x : BitVec 32} {y : BitVec 32} : x ||| y = (x &&& ~~~y) + y

theorem HackersDelight.Ch2Basics.AdditionCombinedWithLogicalOperations.and_eq_not_or_sub_not {x : BitVec 32} {y : BitVec 32} : x &&& y = (~~~x ||| y) - ~~~x