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

source
theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.not_beq_not (a b : Bool) :
((!a) == !b) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_beq_not {w : Nat} (a b : BitVec w) :
(~~~a == ~~~b) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_beq_zero_iff {w : Nat} (a b : BitVec w) :
(a ^^^ b == 0#w) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.zero_beq_xor_iff {w : Nat} (a b : BitVec w) :
(0#w == a ^^^ b) = (a == b)
source
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)
source
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)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_left_inj {w : Nat} (a b c : BitVec w) :
(a ^^^ c == b ^^^ c) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_left_inj' {w : Nat} (a b c : BitVec w) :
(a ^^^ c == c ^^^ b) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_right_inj {w : Nat} (a b c : BitVec w) :
(c ^^^ a == c ^^^ b) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_right_inj' {w : Nat} (a b c : BitVec w) :
(c ^^^ a == b ^^^ c) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_inj {w : Nat} (a b c : BitVec w) :
(a + c == b + c) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_inj' {w : Nat} (a b c : BitVec w) :
(a + c == c + b) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_inj {w : Nat} (a b c : BitVec w) :
(c + a == c + b) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_inj' {w : Nat} (a b c : BitVec w) :
(c + a == b + c) = (a == b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_eq_self {w : Nat} (a b : BitVec w) :
(a + b == b) = (a == 0#w)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_eq_self {w : Nat} (a b : BitVec w) :
(a + b == a) = (b == 0#w)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.self_eq_add_right {w : Nat} (a b : BitVec w) :
(a == a + b) = (b == 0#w)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.self_eq_add_left {w : Nat} (a b : BitVec w) :
(a == b + a) = (b == 0#w)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
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)
source
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
source
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
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm {w : Nat} (a b : BitVec w) :
(~~~a == b) = (a == ~~~b)
source
theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm' {w : Nat} (a b : BitVec w) :
(a == ~~~b) = (b == ~~~a)