refactor: split out tactics

leanprover · Jul 15, 2024 · 811cf72 · 811cf72
1 parent 6890bde
commit 811cf72
Show file tree

Hide file tree

Showing 119 changed files with 125 additions and 137 deletions.
diff --git a/Eval/Popcount.lean b/Eval/Popcount.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 /-
 This is based on: https://saw.galois.com/intro/IntroToSAW.html#the-code

diff --git a/Eval/WillOverflow.lean b/Eval/WillOverflow.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 /-
 This file is based on: https://grack.com/blog/2022/12/20/deriving-a-bit-twiddling-hack/

diff --git a/Eval/bitvec_152.lean b/Eval/bitvec_152.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_152 :
  ∀ (x : BitVec 8), x * -1 = 0 - x

diff --git a/Eval/bitvec_160.lean b/Eval/bitvec_160.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_160 :
  ∀ (x C1 C2 : BitVec 7), x <<< C2 * C1 = x * C1 <<< C2

diff --git a/Eval/bitvec_229.lean b/Eval/bitvec_229.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_229 :
  ∀ (X C1 Op1 : BitVec 4), (X + C1) * Op1 = X * Op1 + C1 * Op1

diff --git a/Eval/bitvec_239.lean b/Eval/bitvec_239.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_239 :
  ∀ (Y X : BitVec 8), (0 - X) * (0 - Y) = X * Y

diff --git a/Eval/bitvec_283.lean b/Eval/bitvec_283.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_283 :
  ∀ (Y X : BitVec 1), X * Y = X &&& Y

diff --git a/Eval/bitvec_290__292.lean b/Eval/bitvec_290__292.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 open BitVec
 
 theorem bitvec_290__292 :

diff --git a/Eval/bitvec_AddSub_1043.lean b/Eval/bitvec_AddSub_1043.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1043 :
  ∀ (C1 Z RHS : BitVec 64), (Z &&& C1 ^^^ C1) + 1 + RHS = RHS - (Z ||| ~~~C1)

diff --git a/Eval/bitvec_AddSub_1152.lean b/Eval/bitvec_AddSub_1152.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1152 :
  ∀ (y x : BitVec 1), x + y = x ^^^ y

diff --git a/Eval/bitvec_AddSub_1156.lean b/Eval/bitvec_AddSub_1156.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1156 :
  ∀ (b : BitVec 64), b + b = b <<< 1

diff --git a/Eval/bitvec_AddSub_1164.lean b/Eval/bitvec_AddSub_1164.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1164 :
  ∀ (a b : BitVec 64), 0 - a + b = b - a

diff --git a/Eval/bitvec_AddSub_1165.lean b/Eval/bitvec_AddSub_1165.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1165 :
  ∀ (a b : BitVec 64), 0 - a + (0 - b) = 0 - (a + b)

diff --git a/Eval/bitvec_AddSub_1176.lean b/Eval/bitvec_AddSub_1176.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1176 :
  ∀ (a b : BitVec 64), a + (0 - b) = a - b

diff --git a/Eval/bitvec_AddSub_1202.lean b/Eval/bitvec_AddSub_1202.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1202 :
  ∀ (x C : BitVec 64), (x ^^^ -1) + C = C - 1 - x

diff --git a/Eval/bitvec_AddSub_1295.lean b/Eval/bitvec_AddSub_1295.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1295 :
  ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b

diff --git a/Eval/bitvec_AddSub_1309.lean b/Eval/bitvec_AddSub_1309.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1309 :
  ∀ (a b : BitVec 64), (a &&& b) + (a ||| b) = a + b

diff --git a/Eval/bitvec_AddSub_1539.lean b/Eval/bitvec_AddSub_1539.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1539 :
  ∀ (a x : BitVec 64), x - (0 - a) = x + a

diff --git a/Eval/bitvec_AddSub_1539_2.lean b/Eval/bitvec_AddSub_1539_2.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1539_2 :
  ∀ (x C : BitVec 64), x - C = x + -C

diff --git a/Eval/bitvec_AddSub_1556.lean b/Eval/bitvec_AddSub_1556.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1556 :
  ∀ (y x : BitVec 1), x - y = x ^^^ y

diff --git a/Eval/bitvec_AddSub_1560.lean b/Eval/bitvec_AddSub_1560.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1560 :
  ∀ (a : BitVec 64), -1 - a = a ^^^ -1

diff --git a/Eval/bitvec_AddSub_1564.lean b/Eval/bitvec_AddSub_1564.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1564 :
  ∀ (x C : BitVec 64), C - (x ^^^ -1) = x + (C + 1)

diff --git a/Eval/bitvec_AddSub_1574.lean b/Eval/bitvec_AddSub_1574.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1574 :
  ∀ (X C C2 : BitVec 64), C - (X + C2) = C - C2 - X

diff --git a/Eval/bitvec_AddSub_1614.lean b/Eval/bitvec_AddSub_1614.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1614 :
  ∀ (Y X : BitVec 64), X - (X + Y) = 0 - Y

diff --git a/Eval/bitvec_AddSub_1619.lean b/Eval/bitvec_AddSub_1619.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1619 :
  ∀ (Y X : BitVec 64), X - Y - X = 0 - Y

diff --git a/Eval/bitvec_AddSub_1624.lean b/Eval/bitvec_AddSub_1624.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AddSub_1624 :
  ∀ (A B : BitVec 64), (A ||| B) - (A ^^^ B) = A &&& B

diff --git a/Eval/bitvec_AndOrXor_1230__A__B___A__B.lean b/Eval/bitvec_AndOrXor_1230__A__B___A__B.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1230__A__B___A__B :
  ∀ (notOp0 notOp1 : BitVec 64), (notOp0 ^^^ -1) &&& (notOp1 ^^^ -1) = (notOp0 ||| notOp1) ^^^ -1

diff --git a/Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean b/Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1241_AB__AB__AB :
  ∀ (A B : BitVec 64), (A ||| B) &&& (A &&& B ^^^ -1) = A ^^^ B

diff --git a/Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean b/Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1247_AB__AB__AB :
  ∀ (A B : BitVec 64), (A &&& B ^^^ -1) &&& (A ||| B) = A ^^^ B

diff --git a/Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean b/Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1253_A__AB___A__B :
  ∀ (A B : BitVec 64), (A ^^^ B) &&& A = A &&& (B ^^^ -1)

diff --git a/Eval/bitvec_AndOrXor_1280_ABA___AB.lean b/Eval/bitvec_AndOrXor_1280_ABA___AB.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1280_ABA___AB :
  ∀ (A B : BitVec 64), (A ^^^ -1 ||| B) &&& A = A &&& B

diff --git a/Eval/bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C.lean b/Eval/bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C :
  ∀ (A C B : BitVec 64), (A ^^^ B) &&& (B ^^^ C ^^^ A) = (A ^^^ B) &&& (C ^^^ -1)

diff --git a/Eval/bitvec_AndOrXor_1294_A__B__A__B___A__B.lean b/Eval/bitvec_AndOrXor_1294_A__B__A__B___A__B.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1294_A__B__A__B___A__B :
  ∀ (A B : BitVec 64), (A ||| B) &&& (A ^^^ -1 ^^^ B) = A &&& B

diff --git a/Eval/bitvec_AndOrXor_135.lean b/Eval/bitvec_AndOrXor_135.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_135 :
  ∀ (X C1 C2 : BitVec 64), (X ^^^ C1) &&& C2 = X &&& C2 ^^^ C1 &&& C2

diff --git a/Eval/bitvec_AndOrXor_144.lean b/Eval/bitvec_AndOrXor_144.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_144 :
  ∀ (X C1 C2 : BitVec 64), (X ||| C1) &&& C2 = (X ||| C1 &&& C2) &&& C2

diff --git a/Eval/bitvec_AndOrXor_1683_1.lean b/Eval/bitvec_AndOrXor_1683_1.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 open BitVec
 

diff --git a/Eval/bitvec_AndOrXor_1683_2.lean b/Eval/bitvec_AndOrXor_1683_2.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1683_2 :
  ∀ (a b : BitVec 64), (b ≤ a) || (a != b) = true

diff --git a/Eval/bitvec_AndOrXor_1704.lean b/Eval/bitvec_AndOrXor_1704.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1704 :
  ∀ (A B : BitVec 64), ((B == 0) || (A < B)) = (A ≤ B + -1)

diff --git a/Eval/bitvec_AndOrXor_1705.lean b/Eval/bitvec_AndOrXor_1705.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1705 :
 ∀ (A B : BitVec 64), ((B == 0) || (A < B)) = (A ≤ B + -1)

diff --git a/Eval/bitvec_AndOrXor_1733.lean b/Eval/bitvec_AndOrXor_1733.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_1733 :
  ∀ (A B : BitVec 64), (A != 0) ∨ (B != 0) = (A ||| B != 0)

diff --git a/Eval/bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2.lean b/Eval/bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2 :
  ∀ (x C1 C : BitVec 64), x ^^^ C1 ||| C = (x ||| C) ^^^ C1 &&& ~~~C

diff --git a/Eval/bitvec_AndOrXor_2113___A__B__A___A__B.lean b/Eval/bitvec_AndOrXor_2113___A__B__A___A__B.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2113___A__B__A___A__B :
  ∀ (A B : BitVec 64), (A ^^^ -1) &&& B ||| A = A ||| B

diff --git a/Eval/bitvec_AndOrXor_2118___A__B__A___A__B.lean b/Eval/bitvec_AndOrXor_2118___A__B__A___A__B.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2118___A__B__A___A__B :
  ∀ (A B : BitVec 64), A &&& B ||| A ^^^ -1 = A ^^^ -1 ||| B

diff --git a/Eval/bitvec_AndOrXor_2123___A__B__A__B___A__B.lean b/Eval/bitvec_AndOrXor_2123___A__B__A__B___A__B.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2123___A__B__A__B___A__B :
  ∀ (A B : BitVec 64), A &&& (B ^^^ -1) ||| A ^^^ B = A ^^^ B

diff --git a/Eval/bitvec_AndOrXor_2188.lean b/Eval/bitvec_AndOrXor_2188.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2188 :
  ∀ (A D : BitVec 64), A &&& (D ^^^ -1) ||| (A ^^^ -1) &&& D = A ^^^ D

diff --git a/Eval/bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C.lean b/Eval/bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C :
  ∀ (A C B : BitVec 64), A ^^^ B ||| B ^^^ C ^^^ A = A ^^^ B ||| C

diff --git a/Eval/bitvec_AndOrXor_2243__B__C__A__B___B__A__C.lean b/Eval/bitvec_AndOrXor_2243__B__C__A__B___B__A__C.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2243__B__C__A__B___B__A__C :
  ∀ (A C B : BitVec 64), (B ||| C) &&& A ||| B = B ||| A &&& C

diff --git a/Eval/bitvec_AndOrXor_2247__A__B__A__B.lean b/Eval/bitvec_AndOrXor_2247__A__B__A__B.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2247__A__B__A__B :
  ∀ (A B : BitVec 64), A ^^^ -1 ||| B ^^^ -1 = A &&& B ^^^ -1

diff --git a/Eval/bitvec_AndOrXor_2263.lean b/Eval/bitvec_AndOrXor_2263.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2263 :
  ∀ (B op0 : BitVec 64), op0 ||| op0 ^^^ B = op0 ||| B

diff --git a/Eval/bitvec_AndOrXor_2264.lean b/Eval/bitvec_AndOrXor_2264.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2264 :
  ∀ (A B : BitVec 64), A ||| A ^^^ -1 ^^^ B = A ||| B ^^^ -1

diff --git a/Eval/bitvec_AndOrXor_2265.lean b/Eval/bitvec_AndOrXor_2265.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2265 :
  ∀ (A B : BitVec 64), A &&& B ||| A ^^^ B = A ||| B

diff --git a/Eval/bitvec_AndOrXor_2284.lean b/Eval/bitvec_AndOrXor_2284.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2284 :
  ∀ (A B : BitVec 64), A ||| (A ||| B) ^^^ -1 = A ||| B ^^^ -1

diff --git a/Eval/bitvec_AndOrXor_2285.lean b/Eval/bitvec_AndOrXor_2285.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2285 :
  ∀ (A B : BitVec 64), A ||| A ^^^ B ^^^ -1 = A ||| B ^^^ -1

diff --git a/Eval/bitvec_AndOrXor_2297.lean b/Eval/bitvec_AndOrXor_2297.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2297 :
  ∀ (A B : BitVec 64), A &&& B ||| A ^^^ -1 ^^^ B = A ^^^ -1 ^^^ B

diff --git a/Eval/bitvec_AndOrXor_2367.lean b/Eval/bitvec_AndOrXor_2367.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2367 :
  ∀ (A C1 op1 : BitVec 64), A ||| C1 ||| op1 = A ||| op1 ||| C1

diff --git a/Eval/bitvec_AndOrXor_2416.lean b/Eval/bitvec_AndOrXor_2416.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2416 :
  ∀ (nx y : BitVec 64), (nx ^^^ -1) &&& y ^^^ -1 = nx ||| y ^^^ -1

diff --git a/Eval/bitvec_AndOrXor_2417.lean b/Eval/bitvec_AndOrXor_2417.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2417 :
  ∀ (nx y : BitVec 64), (nx ^^^ -1 ||| y) ^^^ -1 = nx &&& (y ^^^ -1)

diff --git a/Eval/bitvec_AndOrXor_2429.lean b/Eval/bitvec_AndOrXor_2429.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2429 :
  ∀ (y x : BitVec 64), x &&& y ^^^ -1 = x ^^^ -1 ||| y ^^^ -1

diff --git a/Eval/bitvec_AndOrXor_2430.lean b/Eval/bitvec_AndOrXor_2430.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2430 :
  ∀ (y x : BitVec 64), (x ||| y) ^^^ -1 = (x ^^^ -1) &&& (y ^^^ -1)

diff --git a/Eval/bitvec_AndOrXor_2443.lean b/Eval/bitvec_AndOrXor_2443.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 open BitVec
 

diff --git a/Eval/bitvec_AndOrXor_2475.lean b/Eval/bitvec_AndOrXor_2475.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2475 :
  ∀ (x C : BitVec 64), C - x ^^^ -1 = x + (-1 - C)

diff --git a/Eval/bitvec_AndOrXor_2486.lean b/Eval/bitvec_AndOrXor_2486.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2486 :
  ∀ (x C : BitVec 64), x + C ^^^ -1 = -1 - C - x

diff --git a/Eval/bitvec_AndOrXor_2581__BAB___A__B.lean b/Eval/bitvec_AndOrXor_2581__BAB___A__B.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2581__BAB___A__B :
  ∀ (a op1 : BitVec 64), (a ||| op1) ^^^ op1 = a &&& (op1 ^^^ -1)

diff --git a/Eval/bitvec_AndOrXor_2587__BAA___B__A.lean b/Eval/bitvec_AndOrXor_2587__BAA___B__A.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2587__BAA___B__A :
  ∀ (a op1 : BitVec 64), a &&& op1 ^^^ op1 = (a ^^^ -1) &&& op1

diff --git a/Eval/bitvec_AndOrXor_2595.lean b/Eval/bitvec_AndOrXor_2595.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2595 :
  ∀ (a b : BitVec 64), a &&& b ^^^ (a ||| b) = a ^^^ b

diff --git a/Eval/bitvec_AndOrXor_2607.lean b/Eval/bitvec_AndOrXor_2607.lean
@@ -1,4 +1,4 @@
-import LeanSAT.Reflect.Tactics.BVDecide
+import LeanSAT.Tactics.BVDecide
 
 theorem bitvec_AndOrXor_2607 :
  ∀ (a b : BitVec 64), (a ||| b ^^^ -1) ^^^ (a ^^^ -1 ||| b) = a ^^^ b