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

theorem Std.Tactic.BVDecide.Normalize.if_eq_cond {α : Type 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) : (!decide ((a ^^ b) = (a == b))) = true

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_then (c t e : Bool) : ((bif c then t else e) == t) = (c || t == e)

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_else (c t e : Bool) : ((bif c then t else e) == e) = (!c || t == e)

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_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_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_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_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_then_ite {α : Type 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_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_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_else_ite {α : Type 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_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_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_then_ite' {α : Type 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_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_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_else_ite' {α : Type 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_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_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_then_ite'' {α : Type 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_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_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_else_ite'' {α : Type 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_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_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.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