theorem HackersDelight.Ch2Basics.xor_ule_or {x : BitVec 32} {y : BitVec 32} : (x ||| y ≥ᵤ x ^^^ y) = true

theorem HackersDelight.Ch2Basics.and_ule_not_xor {x : BitVec 32} {y : BitVec 32} : (~~~(x ^^^ y) ≥ᵤ x &&& y) = true

def HackersDelight.Ch2Basics.AdditionNoOverflows? {w : ℕ} (x : BitVec w) (y : BitVec w) : Prop

Equations

• HackersDelight.Ch2Basics.AdditionNoOverflows? x y = ((x.adc y false).1 = true)

theorem HackersDelight.Ch2Basics.or_ule_add {x : BitVec 32} {y : BitVec 32} (h : HackersDelight.Ch2Basics.AdditionNoOverflows? x y) : (x + y ≥ᵤ x ||| y) = true

theorem HackersDelight.Ch2Basics.add_ult_or {x : BitVec 32} {y : BitVec 32} (h : ¬HackersDelight.Ch2Basics.AdditionNoOverflows? x y) : (x ||| y >ᵤ x + y) = true

theorem HackersDelight.Ch2Basics.sub_abs_ule_xor {x : BitVec 32} {y : BitVec 32} : (x ^^^ y ≥ᵤ (x - y).abs) = true

theorem HackersDelight.Ch2Basics.eq_iff_abs_sub_sub {x : BitVec 32} {y : BitVec 32} : x = y ↔ ((x - y).abs - 1).msb = true

theorem HackersDelight.Ch2Basics.eq_iff_not_sub_or_sub {x : BitVec 32} {y : BitVec 32} : x = y ↔ (~~~(x - y ||| y - x)).msb = true

theorem HackersDelight.Ch2Basics.neq_iff_sub_or_sub {x : BitVec 32} {y : BitVec 32} : x ≠ y ↔ (x - y ||| y - x).msb = true

theorem HackersDelight.Ch2Basics.neq_iff_neg_sub_abs {x : BitVec 32} {y : BitVec 32} : x ≠ y ↔ (-(x - y).abs).msb = true

theorem HackersDelight.Ch2Basics.lt_iff_sub_xor_xor_and_sub_xor {x : BitVec 32} {y : BitVec 32} : (y >ₛ x) = true ↔ (x - y ^^^ (x ^^^ y) &&& (x - y ^^^ x)).msb = true

theorem HackersDelight.Ch2Basics.slt_iff_and_not_or_not_xor_and_sub {x : BitVec 32} {y : BitVec 32} : (y >ₛ x) = true ↔ (x &&& ~~~y ||| ~~~(x ^^^ y) &&& x - y).msb = true

theorem HackersDelight.Ch2Basics.sle_iff_or_not_and_xor_or_not_sub {x : BitVec 32} {y : BitVec 32} : (y ≥ₛ x) = true ↔ ((x ||| ~~~y) &&& (x ^^^ y ||| ~~~(y - x))).msb = true

theorem HackersDelight.Ch2Basics.ult_iff_not_and_or_not_xor_and_sub {x : BitVec 32} {y : BitVec 32} : (y >ᵤ x) = true ↔ (~~~x &&& y ||| ~~~(x ^^^ y) &&& x - y).msb = true

theorem HackersDelight.Ch2Basics.ule_iff_not_or_and_xor_or_not_sub {x : BitVec 32} {y : BitVec 32} : (y ≥ᵤ x) = true ↔ ((~~~x ||| y) &&& (x ^^^ y ||| ~~~(y - x))).msb = true

theorem HackersDelight.Ch2Basics.eq_zero_iff_abs_sub {x : BitVec 32} : x = 0 ↔ (x.abs - 1).msb = true

theorem HackersDelight.Ch2Basics.eq_zero_iff_not_or_sub {x : BitVec 32} : x = 0 ↔ (~~~(x ||| -x)).msb = true

theorem HackersDelight.Ch2Basics.eq_zero_iff_not_and_sub {x : BitVec 32} : x = 0 ↔ (~~~x &&& x - 1).msb = true

theorem HackersDelight.Ch2Basics.neq_zero_iff_or_neg {x : BitVec 32} : x ≠ 0 ↔ (x ||| -x).msb = true

theorem HackersDelight.Ch2Basics.neq_zero_iff_neg_abs {x : BitVec 32} : x ≠ 0 ↔ (-x.abs).msb = true

theorem HackersDelight.Ch2Basics.slt_zero_iff {x : BitVec 32} : (0 >ₛ x) = true ↔ x.msb = true

theorem HackersDelight.Ch2Basics.sle_zero_iff_or_sub_one {x : BitVec 32} : (0 ≥ₛ x) = true ↔ (x ||| x - 1).msb = true

theorem HackersDelight.Ch2Basics.sle_zero_iff_or_not_sub {x : BitVec 32} : (0 ≥ₛ x) = true ↔ (x ||| ~~~(-x)).msb = true

theorem HackersDelight.Ch2Basics.zero_slt_iff_neg_and_not {x : BitVec 32} : (x >ₛ 0) = true ↔ (-x &&& ~~~x).msb = true

theorem HackersDelight.Ch2Basics.zero_sle_iff_neg_and_not {x : BitVec 32} : (x ≥ₛ 0) = true ↔ (~~~x).msb = true

theorem HackersDelight.Ch2Basics.slt_iff_add_two_pow_ult_add_two_pow {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y >ₛ x) = true ↔ (y + 2 ^ (w - 1) >ₛ x + 2 ^ (w - 1)) = true

theorem HackersDelight.Ch2Basics.ult_iff_sub_two_pow_ult_sub_two_pow {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y >ᵤ x) = true ↔ (y - 2 ^ (w - 1) >ₛ x - 2 ^ (w - 1)) = true

theorem HackersDelight.Ch2Basics.slt_iff_not_add_two_pow_ule_add_two_pow {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y >ₛ x) = true ↔ ¬(x + 2 ^ (w - 1) ≥ᵤ y + 2 ^ (w - 1)) = true

theorem HackersDelight.Ch2Basics.sle_iff_add_two_pow_ule_add_two_pow {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y ≥ₛ x) = true ↔ (y + 2 ^ (w - 1) ≥ᵤ x + 2 ^ (w - 1)) = true

theorem HackersDelight.Ch2Basics.ult_iff_not_ule {x : BitVec 32} {y : BitVec 32} : (y >ᵤ x) = true ↔ ¬(x ≥ᵤ y) = true

theorem HackersDelight.Ch2Basics.eq_iff_adc_not_add {x : BitVec 32} {y : BitVec 32} {w : ℕ} : x = y ↔ BitVec.carry w x (~~~y + 1) false = true

theorem HackersDelight.Ch2Basics.neq_iff_adc_not {x : BitVec 32} {y : BitVec 32} {w : ℕ} : x ≠ y ↔ BitVec.carry w x (~~~y) false = true

theorem HackersDelight.Ch2Basics.slt_iff_not_adc_add_sub_neg_add_sub {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y >ₛ x) = true ↔ ¬BitVec.carry w (x + 2 ^ (w - 1)) (~~~(y + 2 ^ (w - 1)) + 1) false = true

def HackersDelight.Ch2Basics.instHXorBool_sSA : HXor Bool Bool Bool

Equations

• HackersDelight.Ch2Basics.instHXorBool_sSA = { hXor := xor }

theorem HackersDelight.Ch2Basics.sle_iff_not_adc_not_add_sub_xor_sub {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y >ₛ x) = true ↔ (!BitVec.carry w x (~~~y + 1) false ^^^ x.getMsbD (w - 1) ^^^ y.getMsbD (w - 1)) = true

theorem HackersDelight.Ch2Basics.sle_iff_adc_add_sub_neg_add_sub {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y ≥ₛ x) = true ↔ BitVec.carry w (y + 2 ^ (w - 1)) (~~~(x + 2 ^ (w - 1)) + 1) false = true

theorem HackersDelight.Ch2Basics.sle_iff_adc_not_add_sub_sub {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y ≥ₛ x) = true ↔ BitVec.carry w y (~~~x + 1) false ^^^ x.getMsbD (w - 1) ^^^ y.getMsbD (w - 1) = true

theorem HackersDelight.Ch2Basics.ult_iff_not_adc_not_add {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y >ᵤ x) = true ↔ ¬BitVec.carry w x (~~~y + 1) false = true

theorem HackersDelight.Ch2Basics.ult_iff_adc_not_add {x : BitVec 32} {y : BitVec 32} {w : ℕ} : (y ≥ᵤ x) = true ↔ BitVec.carry w y (~~~x + 1) false = true

theorem HackersDelight.Ch2Basics.eq_zero_iff_adc_not_add {x : BitVec 32} {w : ℕ} : x = 0 ↔ BitVec.carry w (~~~x) 1 false = true

theorem HackersDelight.Ch2Basics.neq_zero_iff_adc_neg {x : BitVec 32} {w : ℕ} : x ≠ 0 ↔ BitVec.carry w x (-1) false = true

theorem HackersDelight.Ch2Basics.slt_iff_adc {x : BitVec 32} {w : ℕ} : (0 >ₛ x) = true ↔ BitVec.carry w x x false = true

theorem HackersDelight.Ch2Basics.sle_iff_adc_two_pow_sub_neg_add_two_pow_sub {x : BitVec 32} {w : ℕ} : (0 ≥ₛ x) = true ↔ BitVec.carry w (2 ^ (w - 1)) (-(x + 2 ^ (w - 1))) false = true

theorem HackersDelight.Ch2Basics.add_iff_not_ult {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.AdditionNoOverflows? x y ↔ (y >ᵤ ~~~x) = true

theorem HackersDelight.Ch2Basics.add_iff_add_ult {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.AdditionNoOverflows? x y ↔ (x >ᵤ x + y) = true

theorem HackersDelight.Ch2Basics.add_add_iff_not_ule {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.AdditionNoOverflows? x (y + 1) ↔ (y ≥ᵤ ~~~x) = true

theorem HackersDelight.Ch2Basics.add_add_iff_add_add_ule {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.AdditionNoOverflows? x (y + 1) ↔ (x ≥ᵤ x + y + 1) = true

theorem HackersDelight.Ch2Basics.add_not_add_iff_ult {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.AdditionNoOverflows? x (~~~y + 1) ↔ (y >ᵤ x) = true

theorem HackersDelight.Ch2Basics.add_not_add_iff_ult_sub {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.AdditionNoOverflows? x (~~~y + 1) ↔ (x - y >ᵤ x) = true

theorem HackersDelight.Ch2Basics.add_not_iff_ult {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.AdditionNoOverflows? x (~~~y) ↔ (y ≥ᵤ x) = true

theorem HackersDelight.Ch2Basics.add_not_iff_ule_sub_sub {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.AdditionNoOverflows? x (~~~y) ↔ (x - y - 1 ≥ᵤ x) = true

def HackersDelight.Ch2Basics.UnsignedMultiplicationOverflows? {w : ℕ} (x : BitVec w) (y : BitVec w) : Prop

Equations

• HackersDelight.Ch2Basics.UnsignedMultiplicationOverflows? x y = (x.toNat * y.toNat > 2 ^ w)

def HackersDelight.Ch2Basics.SignedMultiplicationOverflows? {w : ℕ} (x : BitVec w) (y : BitVec w) : Prop

Equations

• HackersDelight.Ch2Basics.SignedMultiplicationOverflows? x y = (x.toInt * y.toInt > 2 ^ (w - 1))

def HackersDelight.Ch2Basics.last32Bits (x : BitVec 64) : BitVec 32

Equations

• HackersDelight.Ch2Basics.last32Bits x = BitVec.ofNat 32 x.toNat

def HackersDelight.Ch2Basics.first32Bits (x : BitVec 64) : BitVec 32

Equations

• HackersDelight.Ch2Basics.first32Bits x = BitVec.ofNat 32 (x >>> 32).toNat

theorem HackersDelight.Ch2Basics.unsigned_mul_overflow_iff_mul_neq_zero {x : BitVec 64} {y : BitVec 64} : HackersDelight.Ch2Basics.UnsignedMultiplicationOverflows? x y ↔ HackersDelight.Ch2Basics.first32Bits (x * y) ≠ 0#32

theorem HackersDelight.Ch2Basics.signed_mul_overflow_iff_mul_neq_mul_RightShift {x : BitVec 64} {y : BitVec 64} : HackersDelight.Ch2Basics.SignedMultiplicationOverflows? x y ↔ HackersDelight.Ch2Basics.first32Bits (x * y) ≠ HackersDelight.Ch2Basics.last32Bits (x * y) >>> 31

theorem HackersDelight.Ch2Basics.mul_div_neq_imp_unsigned_mul_overflow {x : BitVec 32} {y : BitVec 32} {z : BitVec 32} (h : y.toNat ≠ 0) : x * y / z ≠ x → HackersDelight.Ch2Basics.UnsignedMultiplicationOverflows? x y

theorem HackersDelight.Ch2Basics.lt_and_eq_neg_pow_two_or_mul_div_neq_imp_unsigned_mul_overflow {x : BitVec 32} {y : BitVec 32} {z : BitVec 32} (h : y.toNat ≠ 0) : y < 0 ∧ x.toInt = -2 ^ 31 ∨ x * y / z ≠ x → HackersDelight.Ch2Basics.SignedMultiplicationOverflows? x y

def HackersDelight.Ch2Basics.numberOfLeadingZeros {w : ℕ} (x : BitVec w) : ℕ

Equations

• HackersDelight.Ch2Basics.numberOfLeadingZeros x = HackersDelight.Ch2Basics.numberOfLeadingZeros.countLeadingZeros x w 0

def HackersDelight.Ch2Basics.numberOfLeadingZeros.countLeadingZeros {w : ℕ} (x : BitVec w) (i : ℕ) (count : ℕ) : ℕ

Equations

• One or more equations did not get rendered due to their size.
• HackersDelight.Ch2Basics.numberOfLeadingZeros.countLeadingZeros x Nat.zero count = count

theorem HackersDelight.Ch2Basics.le_nlz_add_nlz_not_unsigned_mul_overflow {x : BitVec 64} {y : BitVec 64} : 32 ≤ HackersDelight.Ch2Basics.numberOfLeadingZeros x + HackersDelight.Ch2Basics.numberOfLeadingZeros y ↔ ¬HackersDelight.Ch2Basics.UnsignedMultiplicationOverflows? x y

theorem HackersDelight.Ch2Basics.nlz_add_nlz_le_unsigned_mul_overflow {x : BitVec 64} {y : BitVec 64} : HackersDelight.Ch2Basics.numberOfLeadingZeros x + HackersDelight.Ch2Basics.numberOfLeadingZeros y ≤ 30 ↔ HackersDelight.Ch2Basics.UnsignedMultiplicationOverflows? x y

def HackersDelight.Ch2Basics.SignedDivisionOverflows?? {w : ℕ} (x : BitVec w) (y : BitVec w) : Prop

Equations

• HackersDelight.Ch2Basics.SignedDivisionOverflows?? x y = (y = 0 ∨ w ≠ 1 ∧ x = 2 ^ (w - 1) ∧ y = -1)

theorem HackersDelight.Ch2Basics.div_overflow_iff_eq_zero_or_eq_neg_pow_two_and_eq_neg {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.SignedDivisionOverflows?? x y ↔ y = 0 ∨ x.toInt = -2 ^ 31 ∧ y = -1

theorem HackersDelight.Ch2Basics.div_overflow_iff_neq_and_ult_LeftShift {x : BitVec 64} {y : BitVec 32} : HackersDelight.Ch2Basics.SignedDivisionOverflows?? x (BitVec.zeroExtend 64 y) ↔ y ≠ 0 ∧ x < BitVec.zeroExtend 64 y <<< 32

theorem HackersDelight.Ch2Basics.div_overflow_iff_neq_and_RightShift_lt {x : BitVec 64} {y : BitVec 64} {y : BitVec 32} : HackersDelight.Ch2Basics.SignedDivisionOverflows?? x (BitVec.zeroExtend 64 y) ↔ y ≠ 0 ∧ x >>> 32 < BitVec.zeroExtend 64 y

def HackersDelight.Ch2Basics.signedDifferenceOrZero {w : ℕ} (x : BitVec w) (y : BitVec w) : BitVec w

Equations

• HackersDelight.Ch2Basics.signedDifferenceOrZero x y = if (x ≥ₛ y) = true then x - y else 0#w

def HackersDelight.Ch2Basics.unsignedDifferenceOrZero {w : ℕ} (x : BitVec w) (y : BitVec w) : BitVec w

Equations

• HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y = if (x ≥ᵤ y) = true then x - y else 0#w

def HackersDelight.Ch2Basics.unsignedMaxBitVec {w : ℕ} (x : BitVec w) (y : BitVec w) : BitVec w

Equations

• HackersDelight.Ch2Basics.unsignedMaxBitVec x y = if (x ≥ᵤ y) = true then x else y

def HackersDelight.Ch2Basics.unsignedMinBitVec {w : ℕ} (x : BitVec w) (y : BitVec w) : BitVec w

Equations

• HackersDelight.Ch2Basics.unsignedMinBitVec x y = if (y ≥ᵤ x) = true then x else y

def HackersDelight.Ch2Basics.signedMaxBitVec {w : ℕ} (x : BitVec w) (y : BitVec w) : BitVec w

Equations

• HackersDelight.Ch2Basics.signedMaxBitVec x y = if (x ≥ₛ y) = true then x else y

def HackersDelight.Ch2Basics.signedMinBitVec {w : ℕ} (x : BitVec w) (y : BitVec w) : BitVec w

Equations

• HackersDelight.Ch2Basics.signedMinBitVec x y = if (y ≥ₛ x) = true then x else y

theorem HackersDelight.Ch2Basics.signed_max_eq_add_doz {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedMaxBitVec x y = y + HackersDelight.Ch2Basics.signedDifferenceOrZero x y

theorem HackersDelight.Ch2Basics.signed_min_eq_sub_doz {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedMinBitVec x y = x - HackersDelight.Ch2Basics.signedDifferenceOrZero x y

theorem HackersDelight.Ch2Basics.unsigned_max_eq_add_dozu {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.unsignedMaxBitVec x y = y + HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y

theorem HackersDelight.Ch2Basics.unsigned_min_eq_sub_dozu {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.unsignedMinBitVec x y = x - HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y

def HackersDelight.Ch2Basics.leBitmask {w : ℕ} (x : BitVec w) (y : BitVec w) : BitVec w

Equations

• HackersDelight.Ch2Basics.leBitmask x y = if y ≤ x then -1#w else 0#w

theorem HackersDelight.Ch2Basics.signed_doz_eq_sub_and_bitmask {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedDifferenceOrZero x y = x - y &&& HackersDelight.Ch2Basics.leBitmask x y

theorem HackersDelight.Ch2Basics.signed_max_xor_and_bitmask_xor {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedMaxBitVec x y = (x ^^^ y) &&& HackersDelight.Ch2Basics.leBitmask x y ^^^ y

theorem HackersDelight.Ch2Basics.signed_min_xor_and_bitmask_xor {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedMinBitVec x y = (x ^^^ y) &&& HackersDelight.Ch2Basics.leBitmask y x ^^^ y

def HackersDelight.Ch2Basics.carryBitmask {w : ℕ} (x : BitVec w) (y : BitVec w) : BitVec w

Equations

• HackersDelight.Ch2Basics.carryBitmask x y = if BitVec.carry w x (~~~y) false = true then -1#w else 0#w

theorem HackersDelight.Ch2Basics.unsigned_doz_sub_and_not_carry {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y = x - y &&& ~~~HackersDelight.Ch2Basics.carryBitmask x y

theorem HackersDelight.Ch2Basics.unsigned_max_eq_sub_sub_and_carry {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.unsignedMaxBitVec x y = x - (x - y &&& HackersDelight.Ch2Basics.carryBitmask x y)

theorem HackersDelight.Ch2Basics.unsigned_min_eq_add_sub_and_carry {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.unsignedMinBitVec x y = y + (x - y &&& HackersDelight.Ch2Basics.carryBitmask x y)

theorem HackersDelight.Ch2Basics.signed_doz_and_not_xor_xor_and_and_rightShift {x : BitVec 32} {y : BitVec 32} {d : BitVec 32} (h : d = x - y) : HackersDelight.Ch2Basics.signedDifferenceOrZero x y = d &&& (~~~d ^^^ ((x ^^^ y) &&& (d ^^^ x)) >>> 31)

theorem HackersDelight.Ch2Basics.unsigned_doz_and_not_xor_xor_and_and_rightShift {x : BitVec 32} {y : BitVec 32} {d : BitVec 32} (h : d = x - y) : HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y = d &&& ~~~((~~~x &&& y ||| ~~~(x ^^^ y) &&& d) >>> 31)

theorem HackersDelight.Ch2Basics.signed_doz_eq_sub_and_not_sub_rightShift {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedDifferenceOrZero x y = x - y &&& ~~~((x - y) >>> 31)

theorem HackersDelight.Ch2Basics.signed_max_eq_sub_sub_and_sub_rightShift {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedMaxBitVec x y = x - (x - y &&& (x - y) >>> 31)

theorem HackersDelight.Ch2Basics.signed_min_eq_add_sub_and_sub_rightShift {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedMinBitVec x y = y + (x - y &&& (x - y) >>> 31)

theorem HackersDelight.Ch2Basics.lt_sdoz_or_neg_sdoz {x : BitVec 32} {y : BitVec 32} : (x >ₛ y) = true ↔ (HackersDelight.Ch2Basics.signedDifferenceOrZero x y ||| -HackersDelight.Ch2Basics.signedDifferenceOrZero x y).msb = true

theorem HackersDelight.Ch2Basics.lt_udoz_or_neg_udoz {x : BitVec 32} {y : BitVec 32} : (x >ᵤ y) = true ↔ (HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y ||| -HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y).msb = true

theorem HackersDelight.Ch2Basics.carry_iff_udoz_not_or_neg_udoz_not {x : BitVec 32} {y : BitVec 32} {w : ℕ} : BitVec.carry w x y false = true ↔ (HackersDelight.Ch2Basics.unsignedDifferenceOrZero x (~~~y) ||| -HackersDelight.Ch2Basics.unsignedDifferenceOrZero x (~~~y)).msb = true

theorem HackersDelight.Ch2Basics.abs_sub_sdoz_add_sdoz {x : BitVec 32} {y : BitVec 32} : (x - y).abs = HackersDelight.Ch2Basics.signedDifferenceOrZero x y + HackersDelight.Ch2Basics.signedDifferenceOrZero y x

theorem HackersDelight.Ch2Basics.abs_sub_udoz_add_udoz {x : BitVec 32} {y : BitVec 32} : (x - y).abs = HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y + HackersDelight.Ch2Basics.unsignedDifferenceOrZero y x

theorem HackersDelight.Ch2Basics.carry_iff_not_ult {x : BitVec 32} {y : BitVec 32} {w : ℕ} : BitVec.carry w x y false = true ↔ (x >ᵤ ~~~y) = true

theorem HackersDelight.Ch2Basics.sdoz_not_not_eq_sdoz {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.signedDifferenceOrZero (~~~x) (~~~y) = HackersDelight.Ch2Basics.signedDifferenceOrZero x y

theorem HackersDelight.Ch2Basics.udoz_not_not_eq_udoz {x : BitVec 32} {y : BitVec 32} : HackersDelight.Ch2Basics.unsignedDifferenceOrZero (~~~x) (~~~y) = HackersDelight.Ch2Basics.unsignedDifferenceOrZero x y