This module contains the equality simplifying part of the bv_normalize simp set.

theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.not_beq_not (a b : Bool) : ((!a) == !b) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_beq_not {w : Nat} (a b : BitVec w) : (~~~a == ~~~b) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_beq_zero_iff {w : Nat} (a b : BitVec w) : (a ^^^ b == 0#w) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.zero_beq_xor_iff {w : Nat} (a b : BitVec w) : (0#w == a ^^^ b) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.and_eq_allOnes {w : Nat} (a b : BitVec w) : (a &&& b == -1#w) = (a == -1#w && b == -1#w)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.allOnes_eq_and {w : Nat} (a b : BitVec w) : (-1#w == a &&& b) = (a == -1#w && b == -1#w)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_left_inj {w : Nat} (a b c : BitVec w) : (a ^^^ c == b ^^^ c) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_left_inj' {w : Nat} (a b c : BitVec w) : (a ^^^ c == c ^^^ b) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_right_inj {w : Nat} (a b c : BitVec w) : (c ^^^ a == c ^^^ b) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_right_inj' {w : Nat} (a b c : BitVec w) : (c ^^^ a == b ^^^ c) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_inj {w : Nat} (a b c : BitVec w) : (a + c == b + c) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_inj' {w : Nat} (a b c : BitVec w) : (a + c == c + b) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_inj {w : Nat} (a b c : BitVec w) : (c + a == c + b) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_inj' {w : Nat} (a b c : BitVec w) : (c + a == b + c) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_eq_self {w : Nat} (a b : BitVec w) : (a + b == b) = (a == 0#w)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_eq_self {w : Nat} (a b : BitVec w) : (a + b == a) = (b == 0#w)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.self_eq_add_right {w : Nat} (a b : BitVec w) : (a == a + b) = (b == 0#w)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.self_eq_add_left {w : Nat} (a b : BitVec w) : (a == b + a) = (b == 0#w)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.eq_sub_iff_add_eq {w : Nat} (a b c : BitVec w) : (a == c + (~~~b + 1#w)) = (a + b == c)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.eq_neg_add_iff_add_eq {w : Nat} (a b c : BitVec w) : (a == ~~~b + 1#w + c) = (a + b == c)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.sub_eq_iff_eq_add {w : Nat} (a b c : BitVec w) : (a + (~~~b + 1#w) == c) = (a == c + b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.neg_add_eq_iff_eq_add {w : Nat} (a b c : BitVec w) : (~~~a + 1#w + b == c) = (b == c + a)

theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.bif_eq_bif (d a b c : Bool) : ((bif d then a else b) == bif d then a else c) = (d || b == c)

theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.not_bif_eq_bif (d a b c : Bool) : ((!bif d then a else b) == bif d then a else c) = (!d && (!b) == c)

theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.bif_eq_not_bif (d a b c : Bool) : ((bif d then a else b) == !bif d then a else c) = (!d && b == !c)

theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.bif_eq_bif' (d a b c : Bool) : ((bif d then a else c) == bif d then b else c) = (!d || a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.not_bif_eq_bif' (d a b c : Bool) : ((!bif d then a else c) == bif d then b else c) = (d && (!a) == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.bif_eq_not_bif' (d a b c : Bool) : ((bif d then a else c) == !bif d then b else c) = (d && a == !b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.bif_eq_bif {w : Nat} (d : Bool) (a b c : BitVec w) : ((bif d then a else b) == bif d then a else c) = (d || b == c)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_bif_eq_bif {w : Nat} (d : Bool) (a b c : BitVec w) : ((~~~bif d then a else b) == bif d then a else c) = bif d then ~~~a == a else ~~~b == c

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.bif_eq_not_bif {w : Nat} (d : Bool) (a b c : BitVec w) : ((bif d then a else b) == ~~~bif d then a else c) = bif d then a == ~~~a else b == ~~~c

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.bif_eq_bif' {w : Nat} (d : Bool) (a b c : BitVec w) : ((bif d then a else c) == bif d then b else c) = (!d || a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_bif_eq_bif' {w : Nat} (d : Bool) (a b c : BitVec w) : ((~~~bif d then a else c) == bif d then b else c) = bif d then ~~~a == b else ~~~c == c

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.bif_eq_not_bif' {w : Nat} (d : Bool) (a b c : BitVec w) : ((bif d then a else c) == ~~~bif d then b else c) = bif d then a == ~~~b else c == ~~~c

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm {w : Nat} (a b : BitVec w) : (~~~a == b) = (a == ~~~b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm' {w : Nat} (a b : BitVec w) : (a == ~~~b) = (b == ~~~a)