This contains theorems responsible for turning both Bool and BitVec goals into the x = true normal form (where x consists of only Bool and BitVec) expected by bv_decide.

theorem Std.Tactic.BVDecide.Normalize.BitVec.eq_to_beq {w : Nat} (a b : BitVec w) : (a = b) = ((a == b) = true)

theorem Std.Tactic.BVDecide.Normalize.BitVec.ne_to_beq {w : Nat} (a b : BitVec w) : (a ≠ b) = ((!a == b) = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.eq_to_beq (a b : Bool) : (a = b) = ((a == b) = true)

theorem Std.Tactic.BVDecide.Normalize.BitVec.bne_to_beq {w : Nat} (a b : BitVec w) : (a != b) = !a == b

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

theorem Std.Tactic.BVDecide.Normalize.Bool.neg_to_not (a : Bool) : (¬a = true) = ((!a) = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.ne_to_beq (a b : Bool) : (a ≠ b) = ((!a == b) = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.imp_to_or (a b : Bool) : (a = true → b = true) = ((!a || b) = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.or_to_or (a b : Bool) : (a = true ∨ b = true) = ((a || b) = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.and_to_and (a b : Bool) : (a = true ∧ b = true) = ((a && b) = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.iff_to_beq (a b : Bool) : (a = true ↔ b = true) = ((a == b) = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.eq_false (a : Bool) : ((a = true) = False) = ((!a) = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.decide_eq_true (a : Bool) : decide (a = true) = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.lt_ult {w : Nat} (x y : BitVec w) : (x < y) = (x.ult y = true)

theorem Std.Tactic.BVDecide.Normalize.Bool.or_elim (a b : Bool) : (a || b) = !(!a && !b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.or_elim {w : Nat} (x y : BitVec w) : x ||| y = ~~~(~~~x &&& ~~~y)