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

theorem Std.Tactic.BVDecide.Normalize.Bool.eq_false_of_not_eq_true {b : Bool} (h : (!b) = true) : b = false

theorem Std.Tactic.BVDecide.Normalize.ite_eq_cond {α : Sort u_1} {b : Bool} {x y : α} : (if b = true then x else y) = bif b then x else y

@[deprecated Std.Tactic.BVDecide.Normalize.ite_eq_cond (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.if_eq_cond {α : Sort u_1} {b : Bool} {x y : α} : (if b = true then x else y) = bif b then x else y

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

theorem Std.Tactic.BVDecide.Normalize.Bool.not_beq_one (a : BitVec 1) : (!a == 1#1) = (a == 0#1)

theorem Std.Tactic.BVDecide.Normalize.Bool.not_beq_zero (a : BitVec 1) : (!a == 0#1) = (a == 1#1)

theorem Std.Tactic.BVDecide.Normalize.Bool.not_one_beq (a : BitVec 1) : (!1#1 == a) = (a == 0#1)

theorem Std.Tactic.BVDecide.Normalize.Bool.not_zero_beq (a : BitVec 1) : (!0#1 == a) = (a == 1#1)

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_left (c t e : Bool) : ((bif c then t else e) == t) = (c || t == e)

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_same_left (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_then (c t e : Bool) : ((bif c then t else e) == t) = (c || t == e)

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_left' (c t e : Bool) : (t == bif c then t else e) = (c || t == e)

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_same_left' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_then' (c t e : Bool) : (t == bif c then t else e) = (c || t == e)

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_right (c t e : Bool) : ((bif c then t else e) == e) = (!c || t == e)

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_same_right (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_else (c t e : Bool) : ((bif c then t else e) == e) = (!c || t == e)

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_right' (c t e : Bool) : (e == bif c then t else e) = (!c || t == e)

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_same_right' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_same_else' (c t e : Bool) : (e == bif c then t else e) = (!c || t == e)

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_left {w : Nat} (c : Bool) (t e : BitVec w) : ((bif c then t else e) == t) = (c || t == e)

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_same_left (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_then {w : Nat} (c : Bool) (t e : BitVec w) : ((bif c then t else e) == t) = (c || t == e)

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_left' {w : Nat} (c : Bool) (t e : BitVec w) : (t == bif c then t else e) = (c || t == e)

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_same_left' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_then' {w : Nat} (c : Bool) (t e : BitVec w) : (t == bif c then t else e) = (c || t == e)

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_right {w : Nat} (c : Bool) (t e : BitVec w) : ((bif c then t else e) == e) = (!c || t == e)

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_same_right (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_else {w : Nat} (c : Bool) (t e : BitVec w) : ((bif c then t else e) == e) = (!c || t == e)

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_right' {w : Nat} (c : Bool) (t e : BitVec w) : (e == bif c then t else e) = (!c || t == e)

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_same_right' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_same_else' {w : Nat} (c : Bool) (t e : BitVec w) : (e == bif c then t else e) = (!c || t == e)

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_ite_left {α : Sort u_1} (cond : Bool) {a b c : α} : (bif cond then bif cond then a else b else c) = bif cond then a else c

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_ite_left (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite {α : Sort u_1} (cond : Bool) {a b c : α} : (bif cond then bif cond then a else b else c) = bif cond then a else c

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_left (cond : Bool) {a b c : Bool} : (bif cond then !bif cond then a else b else c) = bif cond then !a else c

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_left (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite (cond : Bool) {a b c : Bool} : (bif cond then !bif cond then a else b else c) = bif cond then !a else c

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

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_left (since := "2026-07-21")]

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

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_ite_right {α : Sort u_1} (cond : Bool) {a b c : α} : (bif cond then a else bif cond then b else c) = bif cond then a else c

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_ite_right (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite {α : Sort u_1} (cond : Bool) {a b c : α} : (bif cond then a else bif cond then b else c) = bif cond then a else c

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_right (cond : Bool) {a b c : Bool} : (bif cond then a else !bif cond then b else c) = bif cond then a else !c

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_right (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite (cond : Bool) {a b c : Bool} : (bif cond then a else !bif cond then b else c) = bif cond then a else !c

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

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_right (since := "2026-07-21")]

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

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_ite_left' {α : Sort u_1} (c0 c1 : Bool) {a b : α} : (bif c0 then bif c1 then a else b else a) = bif c0 && !c1 then b else a

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_ite_left' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite' {α : Sort u_1} (c0 c1 : Bool) {a b : α} : (bif c0 then bif c1 then a else b else a) = bif c0 && !c1 then b else a

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_left' (c0 c1 : Bool) {a b : Bool} : (bif c0 then !bif c1 then !a else b else a) = bif c0 && !c1 then !b else a

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_left' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite' (c0 c1 : Bool) {a b : Bool} : (bif c0 then !bif c1 then !a else b else a) = bif c0 && !c1 then !b else a

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_left' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} : (bif c0 then ~~~bif c1 then ~~~a else b else a) = bif c0 && !c1 then ~~~b else a

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_left' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_then_not_ite' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} : (bif c0 then ~~~bif c1 then ~~~a else b else a) = bif c0 && !c1 then ~~~b else a

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_ite_right' {α : Sort u_1} (c0 c1 : Bool) {a b : α} : (bif c0 then a else bif c1 then a else b) = bif !c0 && !c1 then b else a

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_ite_right' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite' {α : Sort u_1} (c0 c1 : Bool) {a b : α} : (bif c0 then a else bif c1 then a else b) = bif !c0 && !c1 then b else a

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_right' (c0 c1 : Bool) {a b : Bool} : (bif c0 then a else !bif c1 then !a else b) = bif !c0 && !c1 then !b else a

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_right' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite' (c0 c1 : Bool) {a b : Bool} : (bif c0 then a else !bif c1 then !a else b) = bif !c0 && !c1 then !b else a

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_right' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} : (bif c0 then a else ~~~bif c1 then ~~~a else b) = bif !c0 && !c1 then ~~~b else a

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_right' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_else_not_ite' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} : (bif c0 then a else ~~~bif c1 then ~~~a else b) = bif !c0 && !c1 then ~~~b else a

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_ite_left'' {α : Sort u_1} (c0 c1 : Bool) {a b : α} : (bif c0 then bif c1 then b else a else a) = bif c0 && c1 then b else a

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_ite_left'' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite'' {α : Sort u_1} (c0 c1 : Bool) {a b : α} : (bif c0 then bif c1 then b else a else a) = bif c0 && c1 then b else a

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_left'' (c0 c1 : Bool) {a b : Bool} : (bif c0 then !bif c1 then b else !a else a) = bif c0 && c1 then !b else a

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_left'' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite'' (c0 c1 : Bool) {a b : Bool} : (bif c0 then !bif c1 then b else !a else a) = bif c0 && c1 then !b else a

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_left'' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} : (bif c0 then ~~~bif c1 then b else ~~~a else a) = bif c0 && c1 then ~~~b else a

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_left'' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_then_not_ite'' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} : (bif c0 then ~~~bif c1 then b else ~~~a else a) = bif c0 && c1 then ~~~b else a

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_ite_right'' {α : Sort u_1} (c0 c1 : Bool) {a b : α} : (bif c0 then a else bif c1 then b else a) = bif !c0 && c1 then b else a

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_ite_right'' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_ite'' {α : Sort u_1} (c0 c1 : Bool) {a b : α} : (bif c0 then a else bif c1 then b else a) = bif !c0 && c1 then b else a

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_right'' (c0 c1 : Bool) {a b : Bool} : (bif c0 then a else !bif c1 then b else !a) = bif !c0 && c1 then !b else a

@[deprecated Std.Tactic.BVDecide.Normalize.Bool.ite_not_ite_right'' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite'' (c0 c1 : Bool) {a b : Bool} : (bif c0 then a else !bif c1 then b else !a) = bif !c0 && c1 then !b else a

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_right'' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} : (bif c0 then a else ~~~bif c1 then b else ~~~a) = bif !c0 && c1 then ~~~b else a

@[deprecated Std.Tactic.BVDecide.Normalize.BitVec.ite_not_ite_right'' (since := "2026-07-21")]

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_else_not_ite'' {w : Nat} (c0 c1 : Bool) {a b : BitVec w} : (bif c0 then a else ~~~bif c1 then b else ~~~a) = bif !c0 && c1 then ~~~b else a

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero {w : Nat} {c : Bool} {a e : BitVec w} : (a * bif c then 0#w else e) = bif c then 0#w else a * e

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero' {w : Nat} {c : Bool} {a t : BitVec w} : (a * bif c then t else 0#w) = bif c then a * t else 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero'' {w : Nat} {c : Bool} {a e : BitVec w} : (bif c then 0#w else e) * a = bif c then 0#w else e * a

theorem Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero''' {w : Nat} {c : Bool} {a t : BitVec w} : (bif c then t else 0#w) * a = bif c then t * a else 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_one_eq_ite {b : Bool} {a : BitVec 1} : ((a == 1#1) == b) = (a == bif b then 1#1 else 0#1)

theorem Std.Tactic.BVDecide.Normalize.BitVec.one_beq_eq_ite {b : Bool} {a : BitVec 1} : ((1#1 == a) == b) = (a == bif b then 1#1 else 0#1)

theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_one_eq_ite' {b : Bool} {a : BitVec 1} : (b == (a == 1#1)) = (a == bif b then 1#1 else 0#1)

theorem Std.Tactic.BVDecide.Normalize.BitVec.one_beq_eq_ite' {b : Bool} {a : BitVec 1} : (b == (1#1 == a)) = (a == bif b then 1#1 else 0#1)

theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_zero_eq_ite {b : Bool} {a : BitVec 1} : ((a == 0#1) == b) = (a == bif b then 0#1 else 1#1)

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_beq_eq_ite {b : Bool} {a : BitVec 1} : ((0#1 == a) == b) = (a == bif b then 0#1 else 1#1)

theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_zero_eq_ite' {b : Bool} {a : BitVec 1} : (b == (a == 0#1)) = (a == bif b then 0#1 else 1#1)

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_beq_eq_ite' {b : Bool} {a : BitVec 1} : (b == (0#1 == a)) = (a == bif b then 0#1 else 1#1)

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_beq_zero (t : BitVec 1) : (bif t == 0#1 then 0#1 else 1#1) = t

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_zero_beq (t : BitVec 1) : (bif 0#1 == t then 0#1 else 1#1) = t

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_beq_one (t : BitVec 1) : (bif t == 1#1 then 1#1 else 0#1) = t

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_one_beq (t : BitVec 1) : (bif 1#1 == t then 1#1 else 0#1) = t

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_beq_zero_not (t : BitVec 1) : (bif t == 0#1 then 1#1 else 0#1) = ~~~t

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_zero_beq_not (t : BitVec 1) : (bif 0#1 == t then 1#1 else 0#1) = ~~~t

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_beq_one_not (t : BitVec 1) : (bif t == 1#1 then 0#1 else 1#1) = ~~~t

theorem Std.Tactic.BVDecide.Normalize.BitVec.ite_one_beq_not (t : BitVec 1) : (bif 1#1 == t then 0#1 else 1#1) = ~~~t

theorem Std.Tactic.BVDecide.Normalize.Bool.beq_not_ite {a b c : Bool} : (a == !bif c then a else b) = (!c && a == !b)

theorem Std.Tactic.BVDecide.Normalize.Bool.beq_not_ite' {a b c : Bool} : (a == !bif c then b else a) = (c && a == !b)

theorem Std.Tactic.BVDecide.Normalize.Bool.not_ite_beq {a b c : Bool} : ((!bif c then a else b) == a) = (!c && a == !b)

theorem Std.Tactic.BVDecide.Normalize.Bool.not_ite_beq' {a b c : Bool} : ((!bif c then b else a) == a) = (c && a == !b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_not_ite {w : Nat} {a b : BitVec (w + 1)} {c : Bool} : (a == ~~~bif c then a else b) = (!c && a == ~~~b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.beq_not_ite' {w : Nat} {a b : BitVec (w + 1)} {c : Bool} : (a == ~~~bif c then b else a) = (c && a == ~~~b)

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_ite_beq {w : Nat} {a b : BitVec (w + 1)} {c : Bool} : ((~~~bif c then a else b) == a) = (!c && ~~~b == a)

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_ite_beq' {w : Nat} {a b : BitVec (w + 1)} {c : Bool} : ((~~~bif c then b else a) == a) = (c && ~~~b == a)

theorem Std.Tactic.BVDecide.Normalize.Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) : lhs = true

theorem Std.Tactic.BVDecide.Normalize.Bool.and_right (lhs rhs : Bool) (h : (lhs && rhs) = true) : rhs = true

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