From 4af5af55617d6eafa71d6cd00145cebfbb8117b6 Mon Sep 17 00:00:00 2001
From: Yui5427 <785369607@qq.com>
Date: Sat, 28 Dec 2024 21:03:25 +0800
Subject: [PATCH] Add or_sub_xor_eq_and

---
 SSA/Projects/InstCombine/ForLean.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index f1eb1b98a..2a42ce25b 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -357,6 +357,11 @@ theorem and_add_xor_eq_or {a b : BitVec w} : (a &&& b) + (a ^^^ b) = a ||| b :=
   simp only [Bool.bne_assoc]
   cases a.getLsbD ↑i <;> simp [carry_and_xor_false]
 
+@[simp]
+theorem or_sub_xor_eq_and {a b : BitVec w} : (a ||| b) - (a ^^^ b) = a &&& b := by
+  symm
+  rw [eq_sub_iff_add_eq, and_add_xor_eq_or]
+
 attribute [bv_ofBool] ofBool_or_ofBool
 attribute [bv_ofBool] ofBool_and_ofBool
 attribute [bv_ofBool] ofBool_xor_ofBool