Move to Generated

teorth · Sep 29, 2024 · eee78e9 · eee78e9
1 parent c2892c0
commit eee78e9
Show file tree

Hide file tree

Showing 113 changed files with 114 additions and 5 deletions.
diff --git a/equational_theories.lean b/equational_theories.lean
@@ -1,7 +1,6 @@
 import equational_theories.FreeMagma
 import equational_theories.Subgraph
 import equational_theories.AllEquations
-import equational_theories.FinitePoly
 import equational_theories.InfModel
 import equational_theories.Generated
 import equational_theories.SmallMagmas
diff --git a/equational_theories/Generated.lean b/equational_theories/Generated.lean
@@ -2,3 +2,4 @@ import equational_theories.Generated.SimpleRewrites
 import equational_theories.Generated.Constant
 import equational_theories.Generated.Singleton
 import equational_theories.Generated.TrivialBruteforce
+import equational_theories.Generated.FinitePoly
diff --git a/equational_theories/Generated/FinitePoly.lean b/equational_theories/Generated/FinitePoly.lean
@@ -0,0 +1,109 @@
+import equational_theories.Generated.FinitePoly.Refutation6
+import equational_theories.Generated.FinitePoly.Refutation8
+import equational_theories.Generated.FinitePoly.Refutation14
+import equational_theories.Generated.FinitePoly.Refutation18
+import equational_theories.Generated.FinitePoly.Refutation20
+import equational_theories.Generated.FinitePoly.Refutation24
+import equational_theories.Generated.FinitePoly.Refutation32
+import equational_theories.Generated.FinitePoly.Refutation34
+import equational_theories.Generated.FinitePoly.Refutation40
+import equational_theories.Generated.FinitePoly.Refutation46
+import equational_theories.Generated.FinitePoly.Refutation50
+import equational_theories.Generated.FinitePoly.Refutation56
+import equational_theories.Generated.FinitePoly.Refutation60
+import equational_theories.Generated.FinitePoly.Refutation66
+import equational_theories.Generated.FinitePoly.Refutation68
+import equational_theories.Generated.FinitePoly.Refutation72
+import equational_theories.Generated.FinitePoly.Refutation74
+import equational_theories.Generated.FinitePoly.Refutation78
+import equational_theories.Generated.FinitePoly.Refutation82
+import equational_theories.Generated.FinitePoly.Refutation84
+import equational_theories.Generated.FinitePoly.Refutation88
+import equational_theories.Generated.FinitePoly.Refutation90
+import equational_theories.Generated.FinitePoly.Refutation94
+import equational_theories.Generated.FinitePoly.Refutation96
+import equational_theories.Generated.FinitePoly.Refutation108
+import equational_theories.Generated.FinitePoly.Refutation112
+import equational_theories.Generated.FinitePoly.Refutation114
+import equational_theories.Generated.FinitePoly.Refutation116
+import equational_theories.Generated.FinitePoly.Refutation120
+import equational_theories.Generated.FinitePoly.Refutation126
+import equational_theories.Generated.FinitePoly.Refutation128
+import equational_theories.Generated.FinitePoly.Refutation132
+import equational_theories.Generated.FinitePoly.Refutation138
+import equational_theories.Generated.FinitePoly.Refutation144
+import equational_theories.Generated.FinitePoly.Refutation146
+import equational_theories.Generated.FinitePoly.Refutation150
+import equational_theories.Generated.FinitePoly.Refutation152
+import equational_theories.Generated.FinitePoly.Refutation154
+import equational_theories.Generated.FinitePoly.Refutation172
+import equational_theories.Generated.FinitePoly.Refutation174
+import equational_theories.Generated.FinitePoly.Refutation176
+import equational_theories.Generated.FinitePoly.Refutation178
+import equational_theories.Generated.FinitePoly.Refutation184
+import equational_theories.Generated.FinitePoly.Refutation190
+import equational_theories.Generated.FinitePoly.Refutation194
+import equational_theories.Generated.FinitePoly.Refutation198
+import equational_theories.Generated.FinitePoly.Refutation200
+import equational_theories.Generated.FinitePoly.Refutation206
+import equational_theories.Generated.FinitePoly.Refutation208
+import equational_theories.Generated.FinitePoly.Refutation212
+import equational_theories.Generated.FinitePoly.Refutation214
+import equational_theories.Generated.FinitePoly.Refutation216
+import equational_theories.Generated.FinitePoly.Refutation218
+import equational_theories.Generated.FinitePoly.Refutation220
+import equational_theories.Generated.FinitePoly.Refutation232
+import equational_theories.Generated.FinitePoly.Refutation234
+import equational_theories.Generated.FinitePoly.Refutation236
+import equational_theories.Generated.FinitePoly.Refutation246
+import equational_theories.Generated.FinitePoly.Refutation250
+import equational_theories.Generated.FinitePoly.Refutation262
+import equational_theories.Generated.FinitePoly.Refutation264
+import equational_theories.Generated.FinitePoly.Refutation268
+import equational_theories.Generated.FinitePoly.Refutation272
+import equational_theories.Generated.FinitePoly.Refutation280
+import equational_theories.Generated.FinitePoly.Refutation284
+import equational_theories.Generated.FinitePoly.Refutation286
+import equational_theories.Generated.FinitePoly.Refutation290
+import equational_theories.Generated.FinitePoly.Refutation302
+import equational_theories.Generated.FinitePoly.Refutation314
+import equational_theories.Generated.FinitePoly.Refutation316
+import equational_theories.Generated.FinitePoly.Refutation318
+import equational_theories.Generated.FinitePoly.Refutation320
+import equational_theories.Generated.FinitePoly.Refutation326
+import equational_theories.Generated.FinitePoly.Refutation328
+import equational_theories.Generated.FinitePoly.Refutation330
+import equational_theories.Generated.FinitePoly.Refutation340
+import equational_theories.Generated.FinitePoly.Refutation342
+import equational_theories.Generated.FinitePoly.Refutation346
+import equational_theories.Generated.FinitePoly.Refutation352
+import equational_theories.Generated.FinitePoly.Refutation356
+import equational_theories.Generated.FinitePoly.Refutation364
+import equational_theories.Generated.FinitePoly.Refutation366
+import equational_theories.Generated.FinitePoly.Refutation370
+import equational_theories.Generated.FinitePoly.Refutation374
+import equational_theories.Generated.FinitePoly.Refutation380
+import equational_theories.Generated.FinitePoly.Refutation386
+import equational_theories.Generated.FinitePoly.Refutation388
+import equational_theories.Generated.FinitePoly.Refutation390
+import equational_theories.Generated.FinitePoly.Refutation394
+import equational_theories.Generated.FinitePoly.Refutation400
+import equational_theories.Generated.FinitePoly.Refutation402
+import equational_theories.Generated.FinitePoly.Refutation404
+import equational_theories.Generated.FinitePoly.Refutation406
+import equational_theories.Generated.FinitePoly.Refutation410
+import equational_theories.Generated.FinitePoly.Refutation418
+import equational_theories.Generated.FinitePoly.Refutation422
+import equational_theories.Generated.FinitePoly.Refutation424
+import equational_theories.Generated.FinitePoly.Refutation426
+import equational_theories.Generated.FinitePoly.Refutation432
+import equational_theories.Generated.FinitePoly.Refutation444
+import equational_theories.Generated.FinitePoly.Refutation454
+import equational_theories.Generated.FinitePoly.Refutation470
+import equational_theories.Generated.FinitePoly.Refutation474
+import equational_theories.Generated.FinitePoly.Refutation476
+import equational_theories.Generated.FinitePoly.Refutation492
+import equational_theories.Generated.FinitePoly.Refutation502
+import equational_theories.Generated.FinitePoly.Refutation532
+import equational_theories.Generated.FinitePoly.Refutation550
+import equational_theories.Generated.FinitePoly.Refutation568
diff --git a/...al_theories/FinitePoly/Refutation108.lean → ...s/Generated/FinitePoly/Refutation108.lean b/...al_theories/FinitePoly/Refutation108.lean → ...s/Generated/FinitePoly/Refutation108.lean
diff --git a/...al_theories/FinitePoly/Refutation112.lean → ...s/Generated/FinitePoly/Refutation112.lean b/...al_theories/FinitePoly/Refutation112.lean → ...s/Generated/FinitePoly/Refutation112.lean
diff --git a/...al_theories/FinitePoly/Refutation114.lean → ...s/Generated/FinitePoly/Refutation114.lean b/...al_theories/FinitePoly/Refutation114.lean → ...s/Generated/FinitePoly/Refutation114.lean
diff --git a/...al_theories/FinitePoly/Refutation116.lean → ...s/Generated/FinitePoly/Refutation116.lean b/...al_theories/FinitePoly/Refutation116.lean → ...s/Generated/FinitePoly/Refutation116.lean
diff --git a/...al_theories/FinitePoly/Refutation120.lean → ...s/Generated/FinitePoly/Refutation120.lean b/...al_theories/FinitePoly/Refutation120.lean → ...s/Generated/FinitePoly/Refutation120.lean
diff --git a/...al_theories/FinitePoly/Refutation126.lean → ...s/Generated/FinitePoly/Refutation126.lean b/...al_theories/FinitePoly/Refutation126.lean → ...s/Generated/FinitePoly/Refutation126.lean
diff --git a/...al_theories/FinitePoly/Refutation128.lean → ...s/Generated/FinitePoly/Refutation128.lean b/...al_theories/FinitePoly/Refutation128.lean → ...s/Generated/FinitePoly/Refutation128.lean
diff --git a/...al_theories/FinitePoly/Refutation132.lean → ...s/Generated/FinitePoly/Refutation132.lean b/...al_theories/FinitePoly/Refutation132.lean → ...s/Generated/FinitePoly/Refutation132.lean
diff --git a/...al_theories/FinitePoly/Refutation138.lean → ...s/Generated/FinitePoly/Refutation138.lean b/...al_theories/FinitePoly/Refutation138.lean → ...s/Generated/FinitePoly/Refutation138.lean
diff --git a/...nal_theories/FinitePoly/Refutation14.lean → ...es/Generated/FinitePoly/Refutation14.lean b/...nal_theories/FinitePoly/Refutation14.lean → ...es/Generated/FinitePoly/Refutation14.lean
diff --git a/...al_theories/FinitePoly/Refutation144.lean → ...s/Generated/FinitePoly/Refutation144.lean b/...al_theories/FinitePoly/Refutation144.lean → ...s/Generated/FinitePoly/Refutation144.lean
diff --git a/...al_theories/FinitePoly/Refutation146.lean → ...s/Generated/FinitePoly/Refutation146.lean b/...al_theories/FinitePoly/Refutation146.lean → ...s/Generated/FinitePoly/Refutation146.lean
diff --git a/...al_theories/FinitePoly/Refutation150.lean → ...s/Generated/FinitePoly/Refutation150.lean b/...al_theories/FinitePoly/Refutation150.lean → ...s/Generated/FinitePoly/Refutation150.lean
diff --git a/...al_theories/FinitePoly/Refutation152.lean → ...s/Generated/FinitePoly/Refutation152.lean b/...al_theories/FinitePoly/Refutation152.lean → ...s/Generated/FinitePoly/Refutation152.lean
diff --git a/...al_theories/FinitePoly/Refutation154.lean → ...s/Generated/FinitePoly/Refutation154.lean b/...al_theories/FinitePoly/Refutation154.lean → ...s/Generated/FinitePoly/Refutation154.lean
diff --git a/...al_theories/FinitePoly/Refutation172.lean → ...s/Generated/FinitePoly/Refutation172.lean b/...al_theories/FinitePoly/Refutation172.lean → ...s/Generated/FinitePoly/Refutation172.lean
diff --git a/...al_theories/FinitePoly/Refutation174.lean → ...s/Generated/FinitePoly/Refutation174.lean b/...al_theories/FinitePoly/Refutation174.lean → ...s/Generated/FinitePoly/Refutation174.lean
diff --git a/...al_theories/FinitePoly/Refutation176.lean → ...s/Generated/FinitePoly/Refutation176.lean b/...al_theories/FinitePoly/Refutation176.lean → ...s/Generated/FinitePoly/Refutation176.lean
diff --git a/...al_theories/FinitePoly/Refutation178.lean → ...s/Generated/FinitePoly/Refutation178.lean b/...al_theories/FinitePoly/Refutation178.lean → ...s/Generated/FinitePoly/Refutation178.lean
diff --git a/...nal_theories/FinitePoly/Refutation18.lean → ...es/Generated/FinitePoly/Refutation18.lean b/...nal_theories/FinitePoly/Refutation18.lean → ...es/Generated/FinitePoly/Refutation18.lean
diff --git a/...al_theories/FinitePoly/Refutation184.lean → ...s/Generated/FinitePoly/Refutation184.lean b/...al_theories/FinitePoly/Refutation184.lean → ...s/Generated/FinitePoly/Refutation184.lean
diff --git a/...al_theories/FinitePoly/Refutation190.lean → ...s/Generated/FinitePoly/Refutation190.lean b/...al_theories/FinitePoly/Refutation190.lean → ...s/Generated/FinitePoly/Refutation190.lean
diff --git a/...al_theories/FinitePoly/Refutation194.lean → ...s/Generated/FinitePoly/Refutation194.lean b/...al_theories/FinitePoly/Refutation194.lean → ...s/Generated/FinitePoly/Refutation194.lean
diff --git a/...al_theories/FinitePoly/Refutation198.lean → ...s/Generated/FinitePoly/Refutation198.lean b/...al_theories/FinitePoly/Refutation198.lean → ...s/Generated/FinitePoly/Refutation198.lean
diff --git a/...nal_theories/FinitePoly/Refutation20.lean → ...es/Generated/FinitePoly/Refutation20.lean b/...nal_theories/FinitePoly/Refutation20.lean → ...es/Generated/FinitePoly/Refutation20.lean
diff --git a/...al_theories/FinitePoly/Refutation200.lean → ...s/Generated/FinitePoly/Refutation200.lean b/...al_theories/FinitePoly/Refutation200.lean → ...s/Generated/FinitePoly/Refutation200.lean
diff --git a/...al_theories/FinitePoly/Refutation206.lean → ...s/Generated/FinitePoly/Refutation206.lean b/...al_theories/FinitePoly/Refutation206.lean → ...s/Generated/FinitePoly/Refutation206.lean
diff --git a/...al_theories/FinitePoly/Refutation208.lean → ...s/Generated/FinitePoly/Refutation208.lean b/...al_theories/FinitePoly/Refutation208.lean → ...s/Generated/FinitePoly/Refutation208.lean
diff --git a/...al_theories/FinitePoly/Refutation212.lean → ...s/Generated/FinitePoly/Refutation212.lean b/...al_theories/FinitePoly/Refutation212.lean → ...s/Generated/FinitePoly/Refutation212.lean
diff --git a/...al_theories/FinitePoly/Refutation214.lean → ...s/Generated/FinitePoly/Refutation214.lean b/...al_theories/FinitePoly/Refutation214.lean → ...s/Generated/FinitePoly/Refutation214.lean
diff --git a/...al_theories/FinitePoly/Refutation216.lean → ...s/Generated/FinitePoly/Refutation216.lean b/...al_theories/FinitePoly/Refutation216.lean → ...s/Generated/FinitePoly/Refutation216.lean
diff --git a/...al_theories/FinitePoly/Refutation218.lean → ...s/Generated/FinitePoly/Refutation218.lean b/...al_theories/FinitePoly/Refutation218.lean → ...s/Generated/FinitePoly/Refutation218.lean
diff --git a/...al_theories/FinitePoly/Refutation220.lean → ...s/Generated/FinitePoly/Refutation220.lean b/...al_theories/FinitePoly/Refutation220.lean → ...s/Generated/FinitePoly/Refutation220.lean
diff --git a/...al_theories/FinitePoly/Refutation232.lean → ...s/Generated/FinitePoly/Refutation232.lean b/...al_theories/FinitePoly/Refutation232.lean → ...s/Generated/FinitePoly/Refutation232.lean
diff --git a/...al_theories/FinitePoly/Refutation234.lean → ...s/Generated/FinitePoly/Refutation234.lean b/...al_theories/FinitePoly/Refutation234.lean → ...s/Generated/FinitePoly/Refutation234.lean
diff --git a/...al_theories/FinitePoly/Refutation236.lean → ...s/Generated/FinitePoly/Refutation236.lean b/...al_theories/FinitePoly/Refutation236.lean → ...s/Generated/FinitePoly/Refutation236.lean
diff --git a/...nal_theories/FinitePoly/Refutation24.lean → ...es/Generated/FinitePoly/Refutation24.lean b/...nal_theories/FinitePoly/Refutation24.lean → ...es/Generated/FinitePoly/Refutation24.lean
diff --git a/...al_theories/FinitePoly/Refutation246.lean → ...s/Generated/FinitePoly/Refutation246.lean b/...al_theories/FinitePoly/Refutation246.lean → ...s/Generated/FinitePoly/Refutation246.lean
diff --git a/...al_theories/FinitePoly/Refutation250.lean → ...s/Generated/FinitePoly/Refutation250.lean b/...al_theories/FinitePoly/Refutation250.lean → ...s/Generated/FinitePoly/Refutation250.lean
diff --git a/...al_theories/FinitePoly/Refutation262.lean → ...s/Generated/FinitePoly/Refutation262.lean b/...al_theories/FinitePoly/Refutation262.lean → ...s/Generated/FinitePoly/Refutation262.lean
diff --git a/...al_theories/FinitePoly/Refutation264.lean → ...s/Generated/FinitePoly/Refutation264.lean b/...al_theories/FinitePoly/Refutation264.lean → ...s/Generated/FinitePoly/Refutation264.lean
diff --git a/...al_theories/FinitePoly/Refutation268.lean → ...s/Generated/FinitePoly/Refutation268.lean b/...al_theories/FinitePoly/Refutation268.lean → ...s/Generated/FinitePoly/Refutation268.lean
diff --git a/...al_theories/FinitePoly/Refutation272.lean → ...s/Generated/FinitePoly/Refutation272.lean b/...al_theories/FinitePoly/Refutation272.lean → ...s/Generated/FinitePoly/Refutation272.lean
diff --git a/...al_theories/FinitePoly/Refutation280.lean → ...s/Generated/FinitePoly/Refutation280.lean b/...al_theories/FinitePoly/Refutation280.lean → ...s/Generated/FinitePoly/Refutation280.lean
diff --git a/...al_theories/FinitePoly/Refutation284.lean → ...s/Generated/FinitePoly/Refutation284.lean b/...al_theories/FinitePoly/Refutation284.lean → ...s/Generated/FinitePoly/Refutation284.lean
diff --git a/...al_theories/FinitePoly/Refutation286.lean → ...s/Generated/FinitePoly/Refutation286.lean b/...al_theories/FinitePoly/Refutation286.lean → ...s/Generated/FinitePoly/Refutation286.lean
diff --git a/...al_theories/FinitePoly/Refutation290.lean → ...s/Generated/FinitePoly/Refutation290.lean b/...al_theories/FinitePoly/Refutation290.lean → ...s/Generated/FinitePoly/Refutation290.lean
diff --git a/...al_theories/FinitePoly/Refutation302.lean → ...s/Generated/FinitePoly/Refutation302.lean b/...al_theories/FinitePoly/Refutation302.lean → ...s/Generated/FinitePoly/Refutation302.lean
diff --git a/...al_theories/FinitePoly/Refutation314.lean → ...s/Generated/FinitePoly/Refutation314.lean b/...al_theories/FinitePoly/Refutation314.lean → ...s/Generated/FinitePoly/Refutation314.lean
diff --git a/...al_theories/FinitePoly/Refutation316.lean → ...s/Generated/FinitePoly/Refutation316.lean b/...al_theories/FinitePoly/Refutation316.lean → ...s/Generated/FinitePoly/Refutation316.lean
diff --git a/...al_theories/FinitePoly/Refutation318.lean → ...s/Generated/FinitePoly/Refutation318.lean b/...al_theories/FinitePoly/Refutation318.lean → ...s/Generated/FinitePoly/Refutation318.lean
diff --git a/...nal_theories/FinitePoly/Refutation32.lean → ...es/Generated/FinitePoly/Refutation32.lean b/...nal_theories/FinitePoly/Refutation32.lean → ...es/Generated/FinitePoly/Refutation32.lean
diff --git a/...al_theories/FinitePoly/Refutation320.lean → ...s/Generated/FinitePoly/Refutation320.lean b/...al_theories/FinitePoly/Refutation320.lean → ...s/Generated/FinitePoly/Refutation320.lean
diff --git a/...al_theories/FinitePoly/Refutation326.lean → ...s/Generated/FinitePoly/Refutation326.lean b/...al_theories/FinitePoly/Refutation326.lean → ...s/Generated/FinitePoly/Refutation326.lean
diff --git a/...al_theories/FinitePoly/Refutation328.lean → ...s/Generated/FinitePoly/Refutation328.lean b/...al_theories/FinitePoly/Refutation328.lean → ...s/Generated/FinitePoly/Refutation328.lean
diff --git a/...al_theories/FinitePoly/Refutation330.lean → ...s/Generated/FinitePoly/Refutation330.lean b/...al_theories/FinitePoly/Refutation330.lean → ...s/Generated/FinitePoly/Refutation330.lean
diff --git a/...nal_theories/FinitePoly/Refutation34.lean → ...es/Generated/FinitePoly/Refutation34.lean b/...nal_theories/FinitePoly/Refutation34.lean → ...es/Generated/FinitePoly/Refutation34.lean
diff --git a/...al_theories/FinitePoly/Refutation340.lean → ...s/Generated/FinitePoly/Refutation340.lean b/...al_theories/FinitePoly/Refutation340.lean → ...s/Generated/FinitePoly/Refutation340.lean
diff --git a/...al_theories/FinitePoly/Refutation342.lean → ...s/Generated/FinitePoly/Refutation342.lean b/...al_theories/FinitePoly/Refutation342.lean → ...s/Generated/FinitePoly/Refutation342.lean
diff --git a/...al_theories/FinitePoly/Refutation346.lean → ...s/Generated/FinitePoly/Refutation346.lean b/...al_theories/FinitePoly/Refutation346.lean → ...s/Generated/FinitePoly/Refutation346.lean
diff --git a/...al_theories/FinitePoly/Refutation352.lean → ...s/Generated/FinitePoly/Refutation352.lean b/...al_theories/FinitePoly/Refutation352.lean → ...s/Generated/FinitePoly/Refutation352.lean
diff --git a/...al_theories/FinitePoly/Refutation356.lean → ...s/Generated/FinitePoly/Refutation356.lean b/...al_theories/FinitePoly/Refutation356.lean → ...s/Generated/FinitePoly/Refutation356.lean
diff --git a/...al_theories/FinitePoly/Refutation364.lean → ...s/Generated/FinitePoly/Refutation364.lean b/...al_theories/FinitePoly/Refutation364.lean → ...s/Generated/FinitePoly/Refutation364.lean
diff --git a/...al_theories/FinitePoly/Refutation366.lean → ...s/Generated/FinitePoly/Refutation366.lean b/...al_theories/FinitePoly/Refutation366.lean → ...s/Generated/FinitePoly/Refutation366.lean
diff --git a/...al_theories/FinitePoly/Refutation370.lean → ...s/Generated/FinitePoly/Refutation370.lean b/...al_theories/FinitePoly/Refutation370.lean → ...s/Generated/FinitePoly/Refutation370.lean
diff --git a/...al_theories/FinitePoly/Refutation374.lean → ...s/Generated/FinitePoly/Refutation374.lean b/...al_theories/FinitePoly/Refutation374.lean → ...s/Generated/FinitePoly/Refutation374.lean
diff --git a/...al_theories/FinitePoly/Refutation380.lean → ...s/Generated/FinitePoly/Refutation380.lean b/...al_theories/FinitePoly/Refutation380.lean → ...s/Generated/FinitePoly/Refutation380.lean
diff --git a/...al_theories/FinitePoly/Refutation386.lean → ...s/Generated/FinitePoly/Refutation386.lean b/...al_theories/FinitePoly/Refutation386.lean → ...s/Generated/FinitePoly/Refutation386.lean
diff --git a/...al_theories/FinitePoly/Refutation388.lean → ...s/Generated/FinitePoly/Refutation388.lean b/...al_theories/FinitePoly/Refutation388.lean → ...s/Generated/FinitePoly/Refutation388.lean
diff --git a/...al_theories/FinitePoly/Refutation390.lean → ...s/Generated/FinitePoly/Refutation390.lean b/...al_theories/FinitePoly/Refutation390.lean → ...s/Generated/FinitePoly/Refutation390.lean
diff --git a/...al_theories/FinitePoly/Refutation394.lean → ...s/Generated/FinitePoly/Refutation394.lean b/...al_theories/FinitePoly/Refutation394.lean → ...s/Generated/FinitePoly/Refutation394.lean
diff --git a/...nal_theories/FinitePoly/Refutation40.lean → ...es/Generated/FinitePoly/Refutation40.lean b/...nal_theories/FinitePoly/Refutation40.lean → ...es/Generated/FinitePoly/Refutation40.lean
diff --git a/...al_theories/FinitePoly/Refutation400.lean → ...s/Generated/FinitePoly/Refutation400.lean b/...al_theories/FinitePoly/Refutation400.lean → ...s/Generated/FinitePoly/Refutation400.lean
diff --git a/...al_theories/FinitePoly/Refutation402.lean → ...s/Generated/FinitePoly/Refutation402.lean b/...al_theories/FinitePoly/Refutation402.lean → ...s/Generated/FinitePoly/Refutation402.lean
diff --git a/...al_theories/FinitePoly/Refutation404.lean → ...s/Generated/FinitePoly/Refutation404.lean b/...al_theories/FinitePoly/Refutation404.lean → ...s/Generated/FinitePoly/Refutation404.lean
diff --git a/...al_theories/FinitePoly/Refutation406.lean → ...s/Generated/FinitePoly/Refutation406.lean b/...al_theories/FinitePoly/Refutation406.lean → ...s/Generated/FinitePoly/Refutation406.lean
diff --git a/...al_theories/FinitePoly/Refutation410.lean → ...s/Generated/FinitePoly/Refutation410.lean b/...al_theories/FinitePoly/Refutation410.lean → ...s/Generated/FinitePoly/Refutation410.lean
diff --git a/...al_theories/FinitePoly/Refutation418.lean → ...s/Generated/FinitePoly/Refutation418.lean b/...al_theories/FinitePoly/Refutation418.lean → ...s/Generated/FinitePoly/Refutation418.lean
diff --git a/...al_theories/FinitePoly/Refutation422.lean → ...s/Generated/FinitePoly/Refutation422.lean b/...al_theories/FinitePoly/Refutation422.lean → ...s/Generated/FinitePoly/Refutation422.lean
diff --git a/...al_theories/FinitePoly/Refutation424.lean → ...s/Generated/FinitePoly/Refutation424.lean b/...al_theories/FinitePoly/Refutation424.lean → ...s/Generated/FinitePoly/Refutation424.lean
diff --git a/...al_theories/FinitePoly/Refutation426.lean → ...s/Generated/FinitePoly/Refutation426.lean b/...al_theories/FinitePoly/Refutation426.lean → ...s/Generated/FinitePoly/Refutation426.lean
diff --git a/...al_theories/FinitePoly/Refutation432.lean → ...s/Generated/FinitePoly/Refutation432.lean b/...al_theories/FinitePoly/Refutation432.lean → ...s/Generated/FinitePoly/Refutation432.lean
diff --git a/...al_theories/FinitePoly/Refutation444.lean → ...s/Generated/FinitePoly/Refutation444.lean b/...al_theories/FinitePoly/Refutation444.lean → ...s/Generated/FinitePoly/Refutation444.lean
diff --git a/...al_theories/FinitePoly/Refutation454.lean → ...s/Generated/FinitePoly/Refutation454.lean b/...al_theories/FinitePoly/Refutation454.lean → ...s/Generated/FinitePoly/Refutation454.lean
diff --git a/...nal_theories/FinitePoly/Refutation46.lean → ...es/Generated/FinitePoly/Refutation46.lean b/...nal_theories/FinitePoly/Refutation46.lean → ...es/Generated/FinitePoly/Refutation46.lean
diff --git a/...al_theories/FinitePoly/Refutation470.lean → ...s/Generated/FinitePoly/Refutation470.lean b/...al_theories/FinitePoly/Refutation470.lean → ...s/Generated/FinitePoly/Refutation470.lean
diff --git a/...al_theories/FinitePoly/Refutation474.lean → ...s/Generated/FinitePoly/Refutation474.lean b/...al_theories/FinitePoly/Refutation474.lean → ...s/Generated/FinitePoly/Refutation474.lean
diff --git a/...al_theories/FinitePoly/Refutation476.lean → ...s/Generated/FinitePoly/Refutation476.lean b/...al_theories/FinitePoly/Refutation476.lean → ...s/Generated/FinitePoly/Refutation476.lean
diff --git a/...al_theories/FinitePoly/Refutation492.lean → ...s/Generated/FinitePoly/Refutation492.lean b/...al_theories/FinitePoly/Refutation492.lean → ...s/Generated/FinitePoly/Refutation492.lean
diff --git a/...nal_theories/FinitePoly/Refutation50.lean → ...es/Generated/FinitePoly/Refutation50.lean b/...nal_theories/FinitePoly/Refutation50.lean → ...es/Generated/FinitePoly/Refutation50.lean
diff --git a/...al_theories/FinitePoly/Refutation502.lean → ...s/Generated/FinitePoly/Refutation502.lean b/...al_theories/FinitePoly/Refutation502.lean → ...s/Generated/FinitePoly/Refutation502.lean
diff --git a/...al_theories/FinitePoly/Refutation532.lean → ...s/Generated/FinitePoly/Refutation532.lean b/...al_theories/FinitePoly/Refutation532.lean → ...s/Generated/FinitePoly/Refutation532.lean
diff --git a/...al_theories/FinitePoly/Refutation550.lean → ...s/Generated/FinitePoly/Refutation550.lean b/...al_theories/FinitePoly/Refutation550.lean → ...s/Generated/FinitePoly/Refutation550.lean
diff --git a/...nal_theories/FinitePoly/Refutation56.lean → ...es/Generated/FinitePoly/Refutation56.lean b/...nal_theories/FinitePoly/Refutation56.lean → ...es/Generated/FinitePoly/Refutation56.lean
diff --git a/...al_theories/FinitePoly/Refutation568.lean → ...s/Generated/FinitePoly/Refutation568.lean b/...al_theories/FinitePoly/Refutation568.lean → ...s/Generated/FinitePoly/Refutation568.lean
diff --git a/...onal_theories/FinitePoly/Refutation6.lean → ...ies/Generated/FinitePoly/Refutation6.lean b/...onal_theories/FinitePoly/Refutation6.lean → ...ies/Generated/FinitePoly/Refutation6.lean
diff --git a/...nal_theories/FinitePoly/Refutation60.lean → ...es/Generated/FinitePoly/Refutation60.lean b/...nal_theories/FinitePoly/Refutation60.lean → ...es/Generated/FinitePoly/Refutation60.lean
diff --git a/...nal_theories/FinitePoly/Refutation66.lean → ...es/Generated/FinitePoly/Refutation66.lean b/...nal_theories/FinitePoly/Refutation66.lean → ...es/Generated/FinitePoly/Refutation66.lean
diff --git a/...nal_theories/FinitePoly/Refutation68.lean → ...es/Generated/FinitePoly/Refutation68.lean b/...nal_theories/FinitePoly/Refutation68.lean → ...es/Generated/FinitePoly/Refutation68.lean
diff --git a/...nal_theories/FinitePoly/Refutation72.lean → ...es/Generated/FinitePoly/Refutation72.lean b/...nal_theories/FinitePoly/Refutation72.lean → ...es/Generated/FinitePoly/Refutation72.lean
diff --git a/...nal_theories/FinitePoly/Refutation74.lean → ...es/Generated/FinitePoly/Refutation74.lean b/...nal_theories/FinitePoly/Refutation74.lean → ...es/Generated/FinitePoly/Refutation74.lean
diff --git a/...nal_theories/FinitePoly/Refutation78.lean → ...es/Generated/FinitePoly/Refutation78.lean b/...nal_theories/FinitePoly/Refutation78.lean → ...es/Generated/FinitePoly/Refutation78.lean
diff --git a/...onal_theories/FinitePoly/Refutation8.lean → ...ies/Generated/FinitePoly/Refutation8.lean b/...onal_theories/FinitePoly/Refutation8.lean → ...ies/Generated/FinitePoly/Refutation8.lean
diff --git a/...nal_theories/FinitePoly/Refutation82.lean → ...es/Generated/FinitePoly/Refutation82.lean b/...nal_theories/FinitePoly/Refutation82.lean → ...es/Generated/FinitePoly/Refutation82.lean
diff --git a/...nal_theories/FinitePoly/Refutation84.lean → ...es/Generated/FinitePoly/Refutation84.lean b/...nal_theories/FinitePoly/Refutation84.lean → ...es/Generated/FinitePoly/Refutation84.lean
diff --git a/...nal_theories/FinitePoly/Refutation88.lean → ...es/Generated/FinitePoly/Refutation88.lean b/...nal_theories/FinitePoly/Refutation88.lean → ...es/Generated/FinitePoly/Refutation88.lean
diff --git a/...nal_theories/FinitePoly/Refutation90.lean → ...es/Generated/FinitePoly/Refutation90.lean b/...nal_theories/FinitePoly/Refutation90.lean → ...es/Generated/FinitePoly/Refutation90.lean
diff --git a/...nal_theories/FinitePoly/Refutation94.lean → ...es/Generated/FinitePoly/Refutation94.lean b/...nal_theories/FinitePoly/Refutation94.lean → ...es/Generated/FinitePoly/Refutation94.lean
diff --git a/...nal_theories/FinitePoly/Refutation96.lean → ...es/Generated/FinitePoly/Refutation96.lean b/...nal_theories/FinitePoly/Refutation96.lean → ...es/Generated/FinitePoly/Refutation96.lean
diff --git a/scripts/finite_poly_generate_lean.py b/scripts/finite_poly_generate_lean.py
@@ -5,7 +5,7 @@
 
 #
 # This script reads the file `finite_poly_refutations.txt` and turns each line into a
-# a file `equational_theories/FinitePoly/Refutation<n>.lean`
+# a file `equational_theories/Generated/FinitePoly/Refutation<n>.lean`
 #
 
 
@@ -72,13 +72,13 @@ def «{name}» : Magma (Fin {div}) where
 
 
 with open("data/finite_poly_refutations.txt") as f:
-    with open("equational_theories/FinitePoly.lean", "w") as main:
+    with open("equational_theories/Generated/FinitePoly.lean", "w") as main:
       lines = f.readlines()
       for i, line in enumerate(lines):
-          leanfile = f"equational_theories/FinitePoly/Refutation{i}.lean"
+          leanfile = f"equational_theories/Generated/FinitePoly/Refutation{i}.lean"
           data = parse_row(line)
           if data and data["div"] < 5:
             print(f"Writing {leanfile}")
-            main.write(f"import equational_theories.FinitePoly.Refutation{i}\n")
+            main.write(f"import equational_theories.Generated.FinitePoly.Refutation{i}\n")
             with open(leanfile, "w") as f:
                   f.write(generate_lean(data))