Lemmas validating Decidable.decide simplifications rules on Eq

Lemmas validating simplification rules decide e1 = e2 | e2 = decide e1 ===> e1 = (true = e2).

theorem Blaster.decide_eq_bool (p : Prop) (b : Bool) [Decidable p] : decide p = b ↔ p = (true = b)

theorem Blaster.decide_eq_not_bool (p : Prop) (b : Bool) [Decidable p] : decide p = !b ↔ p = (false = b)

Lemmas validating simplification rule c = (a == b) ===> (true = c) = (a = b) (if isCompatibleBeqType Type(a))`.

theorem Blaster.bool_eq_bool_beq_iff_eq_eq (a b c : Bool) : c = (a == b) ↔ (true = c) = (a = b)

theorem Blaster.bool_eq_nat_beq_iff_eq_eq (x y : Nat) (c : Bool) : c = (x == y) ↔ (true = c) = (x = y)

theorem Blaster.bool_eq_int_beq_iff_eq_eq (x y : Int) (c : Bool) : c = (x == y) ↔ (true = c) = (x = y)

theorem Blaster.bool_eq_string_beq_iff_eq_eq (s t : String) (c : Bool) : c = (s == t) ↔ (true = c) = (s = t)

Lemmas validating simplification rule false = (a == b) ===> ¬ (a = b) (if isCompatibleBeqType Type(a))`.

theorem Blaster.false_eq_bool_beq_iff_eq_eq (a b : Bool) : false = (a == b) ↔ ¬a = b

theorem Blaster.false_eq_nat_beq_iff_eq_eq (x y : Nat) : false = (x == y) ↔ ¬x = y

theorem Blaster.false_eq_int_beq_iff_eq_eq (x y : Int) : false = (x == y) ↔ ¬x = y

theorem Blaster.false_eq_string_beq_iff_eq_eq (s t : String) : false = (s == t) ↔ ¬s = t

Lemmas validating simplification rules - B1 = e1 ∧ B2 = e2 ==> true = (NOP(B1, e1) && NOP(B2, e2)) (if B1 ∨ B2) - B1 = e1 ∧ B2 = e2 ==> false = (e1 || e2) (if ¬ B1 ∧ ¬ B2)

theorem Blaster.and_iff_eq_prop_1 (a b : Bool) : (a && b) = true ↔ true = a ∧ true = b

theorem Blaster.and_iff_eq_prop_2 (a b : Bool) : (a && !b) = true ↔ true = a ∧ false = b

theorem Blaster.and_iff_eq_prop_3 (a b : Bool) : (!a && b) = true ↔ false = a ∧ true = b

theorem Blaster.and_iff_eq_prop_4 (a b : Bool) : (!(a || b)) = true ↔ false = a ∧ false = b

Lemmas validating simplification rules: - B1 = e1 ∨ B2 = e2 ==> true = (NOP(B1, e1) || NOP(B2, e2)) (if B1 ∨ B2) - B1 = e1 ∨ B2 = e2 ==> false = (e1 && e2) (if ¬ B1 ∧ ¬ B2)

theorem Blaster.or_iff_eq_prop_1 (a b : Bool) : (a || b) = true ↔ true = a ∨ true = b

theorem Blaster.or_iff_eq_prop_2 (a b : Bool) : (a || !b) = true ↔ true = a ∨ false = b

theorem Blaster.or_iff_eq_prop_3 (a b : Bool) : (!a || b) = true ↔ false = a ∨ true = b

theorem Blaster.or_iff_eq_prop_4 (a b : Bool) : (!(a && b)) = true ↔ false = a ∨ false = b