theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.not_and_eq_not_or_not {w : ℕ} {x : BitVec w} {y : BitVec w} : ~~~(x &&& y) = ~~~x ||| ~~~y

theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.not_or_eq_not_and_not {w : ℕ} {x : BitVec w} {y : BitVec w} : ~~~(x ||| y) = ~~~x &&& ~~~y

theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.not_add_one_eq_not_sub_one {w : ℕ} {x : BitVec w} : ~~~(x + 1) = ~~~x - 1

theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.not_sub_one_eq_not_add_one {w : ℕ} {x : BitVec w} : ~~~(x - 1) = ~~~x + 1

theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.not_neg_eq_sub_one {w : ℕ} {x : BitVec w} : ~~~(-x) = x - 1

theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.not_xor_eq_not_xor {w : ℕ} {x : BitVec w} {y : BitVec w} : ~~~(x ^^^ y) = ~~~x ^^^ y

theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.q_not_xor {w : ℕ} {x : BitVec w} {y : BitVec w} : ~~~(x ^^^ y) = ~~~x ^^^ y

theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.not_add_eq_not_sub {w : ℕ} {x : BitVec w} {y : BitVec w} : ~~~(x + y) = ~~~x - y

theorem HackersDelight.Ch2Basics.DeMorgansLawsExtended.not_sub_eq_not_add {w : ℕ} {x : BitVec w} {y : BitVec w} : ~~~(x - y) = ~~~x + y