From f0eabb922e1f3e818558209591129c2cbaace783 Mon Sep 17 00:00:00 2001
From: 0art0 <18333981+0art0@users.noreply.github.com>
Date: Tue, 8 Oct 2024 11:09:19 +0100
Subject: [PATCH] Revert "Merge branch 'main' into
equations-command-modification"
This reverts commit a3cf909476d3fc649c08148ae47c000baa7fab22, reversing
changes made to fd25f3fed82d33f4643ddf60bd56efee9ee1142c.
---
.github/workflows/blueprint.yml | 1 -
.vscode/extensions.json | 9 +-
blueprint/.vscode/settings.json | 5 -
commentary/Equation1.md | 2 -
commentary/Equation14.md | 2 -
commentary/Equation1571.md | 2 -
commentary/Equation168.md | 2 -
commentary/Equation1689.md | 2 -
commentary/Equation2.md | 2 -
commentary/Equation26302.md | 2 -
commentary/Equation28770.md | 2 -
commentary/Equation345169.md | 2 -
commentary/Equation3588.md | 2 -
commentary/Equation374794.md | 2 -
commentary/Equation381.md | 2 -
commentary/Equation387.md | 2 -
commentary/Equation43.md | 2 -
commentary/Equation4512.md | 2 -
commentary/Equation46.md | 2 -
commentary/Equation477.md | 2 -
commentary/Equation5105.md | 2 -
commentary/Equation65.md | 2 -
.../EquationLawConversion.lean | 142 --------------
equational_theories/EquationsCommand.lean | 36 +---
equational_theories/FreeMagma.lean | 6 -
.../All4x4Tables/src/check_correct.py | 0
.../All4x4Tables/src/check_redundant.py | 0
.../All4x4Tables/src/double_check_3x3.py | 0
.../All4x4Tables/src/drive_c_parallel.py | 0
.../Generated/All4x4Tables/src/dump_tables.py | 0
.../src/generate_combined_refutations.sh | 0
.../All4x4Tables/src/generate_lean.py | 0
.../Generated/All4x4Tables/src/prune.py | 0
.../All4x4Tables/src/write_equations.py | 0
.../Generated/FinSearch/src/finite_magma.py | 0
.../Generated/FinSearch/src/finsearch.py | 0
.../Generated/FinSearch/src/generate_lean.py | 0
.../Generated/FinSearch/src/parser.py | 0
.../src/finite_poly_generate_lean.py | 0
.../FinitePoly/src/generate_refutations.py | 0
.../Generated/FinitePoly/src/utils.py | 0
.../Generated/LinearOps/src/check_correct.py | 0
.../LinearOps/src/write_equations.py | 0
.../SimpleRewrites/src/find_redundant.py | 0
.../src/find_simple_rewrites.py | 0
.../Generated/SimpleRewrites/src/utils.py | 0
.../src/generate_refutations.py | 0
.../Generated/VampireProven/Conjectures.lean | 181 ------------------
.../Generated/VampireProven/Disproofs2.lean | 8 -
.../src/vampire_fin_counterexamples.py | 0
.../VampireProven/src/vampire_proofs.py | 0
.../VampireProven/src/vampire_proofs_cyc.py | 5 +-
equational_theories/MagmaLaw.lean | 17 +-
equational_theories/Preorder.lean | 10 +-
home_page/implications/index.html | 1 -
home_page/implications/script.js | 26 +--
paper/README.md | 147 ++++++++++++++
paper/main.pdf | Bin 74469 -> 0 bytes
paper/main.tex | 2 +-
scripts/customize_template.py | 0
scripts/explore_magma.py | 0
scripts/find_dual.py | 0
scripts/find_equation_id.py | 0
scripts/find_powerful_theorems.py | 39 ++--
scripts/generate_dashboard.py | 0
scripts/generate_eqs_list.py | 0
scripts/generate_equation_implication_js.py | 11 --
scripts/generate_image.py | 0
scripts/generate_most_wanted_list.py | 0
scripts/generate_z3_counterexample.py | 0
scripts/install_pre-push.sh | 0
scripts/outcomes_to_image.py | 0
scripts/pre-push.sh | 0
scripts/process_implications.py | 0
scripts/run_before_push.sh | 0
scripts/update_mathlib.sh | 0
76 files changed, 198 insertions(+), 486 deletions(-)
delete mode 100644 blueprint/.vscode/settings.json
delete mode 100644 commentary/Equation1.md
delete mode 100644 commentary/Equation14.md
delete mode 100644 commentary/Equation1571.md
delete mode 100644 commentary/Equation168.md
delete mode 100644 commentary/Equation1689.md
delete mode 100644 commentary/Equation2.md
delete mode 100644 commentary/Equation26302.md
delete mode 100644 commentary/Equation28770.md
delete mode 100644 commentary/Equation345169.md
delete mode 100644 commentary/Equation3588.md
delete mode 100644 commentary/Equation374794.md
delete mode 100644 commentary/Equation381.md
delete mode 100644 commentary/Equation387.md
delete mode 100644 commentary/Equation43.md
delete mode 100644 commentary/Equation4512.md
delete mode 100644 commentary/Equation46.md
delete mode 100644 commentary/Equation477.md
delete mode 100644 commentary/Equation5105.md
delete mode 100644 commentary/Equation65.md
delete mode 100644 equational_theories/EquationLawConversion.lean
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/check_correct.py
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/check_redundant.py
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/double_check_3x3.py
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/drive_c_parallel.py
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/dump_tables.py
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/generate_combined_refutations.sh
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/generate_lean.py
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/prune.py
mode change 100755 => 100644 equational_theories/Generated/All4x4Tables/src/write_equations.py
mode change 100755 => 100644 equational_theories/Generated/FinSearch/src/finite_magma.py
mode change 100755 => 100644 equational_theories/Generated/FinSearch/src/finsearch.py
mode change 100755 => 100644 equational_theories/Generated/FinSearch/src/generate_lean.py
mode change 100755 => 100644 equational_theories/Generated/FinSearch/src/parser.py
mode change 100755 => 100644 equational_theories/Generated/FinitePoly/src/finite_poly_generate_lean.py
mode change 100755 => 100644 equational_theories/Generated/FinitePoly/src/generate_refutations.py
mode change 100755 => 100644 equational_theories/Generated/FinitePoly/src/utils.py
mode change 100755 => 100644 equational_theories/Generated/LinearOps/src/check_correct.py
mode change 100755 => 100644 equational_theories/Generated/LinearOps/src/write_equations.py
mode change 100755 => 100644 equational_theories/Generated/SimpleRewrites/src/find_redundant.py
mode change 100755 => 100644 equational_theories/Generated/SimpleRewrites/src/find_simple_rewrites.py
mode change 100755 => 100644 equational_theories/Generated/SimpleRewrites/src/utils.py
mode change 100755 => 100644 equational_theories/Generated/TrivialBruteforce/src/generate_refutations.py
mode change 100755 => 100644 equational_theories/Generated/VampireProven/src/vampire_fin_counterexamples.py
mode change 100755 => 100644 equational_theories/Generated/VampireProven/src/vampire_proofs.py
create mode 100644 paper/README.md
delete mode 100644 paper/main.pdf
mode change 100755 => 100644 scripts/customize_template.py
mode change 100755 => 100644 scripts/explore_magma.py
mode change 100755 => 100644 scripts/find_dual.py
mode change 100755 => 100644 scripts/find_equation_id.py
mode change 100755 => 100644 scripts/find_powerful_theorems.py
mode change 100755 => 100644 scripts/generate_dashboard.py
mode change 100755 => 100644 scripts/generate_eqs_list.py
mode change 100755 => 100644 scripts/generate_equation_implication_js.py
mode change 100755 => 100644 scripts/generate_image.py
mode change 100755 => 100644 scripts/generate_most_wanted_list.py
mode change 100755 => 100644 scripts/generate_z3_counterexample.py
mode change 100755 => 100644 scripts/install_pre-push.sh
mode change 100755 => 100644 scripts/outcomes_to_image.py
mode change 100755 => 100644 scripts/pre-push.sh
mode change 100755 => 100644 scripts/process_implications.py
mode change 100755 => 100644 scripts/run_before_push.sh
mode change 100755 => 100644 scripts/update_mathlib.sh
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
index 2ead3f994..ebeadb92c 100644
--- a/.github/workflows/blueprint.yml
+++ b/.github/workflows/blueprint.yml
@@ -139,7 +139,6 @@ jobs:
- name: Generate home_page/implications/implications.js
run: |
~/.elan/bin/lake exe extract_implications outcomes > /tmp/out.json
- pip install markdown
python scripts/generate_equation_implication_js.py /tmp/out.json
- name: Bundle dependencies
diff --git a/.vscode/extensions.json b/.vscode/extensions.json
index 7501714dc..acf12cdca 100644
--- a/.vscode/extensions.json
+++ b/.vscode/extensions.json
@@ -1,7 +1,12 @@
{
+ // Learn about workspace recommendations at:
+ // https://go.microsoft.com/fwlink/?LinkId=827846
+
+ // The extension identifier format is ${publisher}.${name}
+ // Example: vscode.csharp
+
// List of extensions that should be recommended for users of this workspace
"recommendations": [
- "leanprover.lean4", // Extension for Lean 4 support
- "James-Yu.latex-workshop" // LaTeX Workshop extension for LaTeX support
+ "leanprover.lean4" // Extension for Lean 4 support
]
}
diff --git a/blueprint/.vscode/settings.json b/blueprint/.vscode/settings.json
deleted file mode 100644
index f635b15ea..000000000
--- a/blueprint/.vscode/settings.json
+++ /dev/null
@@ -1,5 +0,0 @@
-{
- // This setting disables the LaTeX Workshop extension for the current workspace (folder).
- // It ensures that LaTeX Workshop will not run for any .tex files of the blueprint.
- "latex-workshop.enabled": false
-}
diff --git a/commentary/Equation1.md b/commentary/Equation1.md
deleted file mode 100644
index 2c4735e5e..000000000
--- a/commentary/Equation1.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [1 `x = x`](https://teorth.github.io/equational_theories/implications/?1): the trivial law
-This is the weakest law, satisfied by all magmas. No other law is equivalent to this law.
diff --git a/commentary/Equation14.md b/commentary/Equation14.md
deleted file mode 100644
index 5479efd0d..000000000
--- a/commentary/Equation14.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equations [14 `x = y ◇ (x ◇ y)`](https://teorth.github.io/equational_theories/implications/?14), [29 `x = (y ◇ x) ◇ y`](https://teorth.github.io/equational_theories/implications/?29): 2001 Putnam laws
-Problem A1 of the 2001 Putnam asked to show (in our language) that [Equation 14 implies Equation 29](https://teorth.github.io/equational_theories/blueprint/implications-chapter.html#14_implies_29). In fact, the two laws are equivalent.
diff --git a/commentary/Equation1571.md b/commentary/Equation1571.md
deleted file mode 100644
index b81998b43..000000000
--- a/commentary/Equation1571.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [1571 `x = (y ◇ z) ◇ (y ◇ (x ◇ z))`](https://teorth.github.io/equational_theories/implications/?1571): a law for abelian groups of exponent 2
-It was shown [by Mendelsohn and Padmanabhan](https://teorth.github.io/equational_theories/blueprint/sect0001.html#mendelsohn-padmanabhan) that [this law characterizes abelian groups of exponent 2](https://teorth.github.io/equational_theories/blueprint/implications-chapter.html#1571_impl).
diff --git a/commentary/Equation168.md b/commentary/Equation168.md
deleted file mode 100644
index b19a4b71c..000000000
--- a/commentary/Equation168.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [168 `x = (y ◇ x) ◇ (x ◇ z)`](https://teorth.github.io/equational_theories/implications/?168): the central groupoid law
-This law defines central groupoids, which are magmas with some interesting combinatorial structure. For instance, all finite central groupoids have a cardinality that is necessarily a square number. [This paper of Knuth](https://teorth.github.io/equational_theories/blueprint/sect0001.html#knuth) establishes many of the basic properties of these objects.
diff --git a/commentary/Equation1689.md b/commentary/Equation1689.md
deleted file mode 100644
index b45509366..000000000
--- a/commentary/Equation1689.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [1689 `x = (y ◇ x) ◇ ((x ◇ z) ◇ z)`](https://teorth.github.io/equational_theories/implications/?1689): a non-trivially singleton law
-This law was [identified by Kisielewicz](https://teorth.github.io/equational_theories/blueprint/sect0001.html#Kisielewicz2) as a law that collapses to the singleton law 2, but all known proofs are [surprisingly lengthy](https://teorth.github.io/equational_theories/blueprint/implications-chapter.html#1689_equiv_2).
diff --git a/commentary/Equation2.md b/commentary/Equation2.md
deleted file mode 100644
index cec77d640..000000000
--- a/commentary/Equation2.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [2 `x = y`](https://teorth.github.io/equational_theories/implications/?2): the singleton law
-This is the strongest law, satisfied only by the trivial magmas: the singleton and empty magmas. Many laws are equivalent to this law; informally, they are so "overdetermined" that they can only be satisfied by trivial magmas. In fact, from our list of 4694 laws, exactly 1495 other laws are equivalent to this one.
diff --git a/commentary/Equation26302.md b/commentary/Equation26302.md
deleted file mode 100644
index 0125dc4c4..000000000
--- a/commentary/Equation26302.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation 26302 `x = (y ◇ ((z ◇ x) ◇ w)) ◇ (x ◇ w)`: the natural central groupoid law
-It was shown [by Knuth](https://teorth.github.io/equational_theories/blueprint/sect0001.html#knuth) that [this law characterizes](https://teorth.github.io/equational_theories/blueprint/implications-chapter.html#natural-central-groupoid) "natural central groupoids", which, up to isomorphisms, are Cartesian squares `S × S` with magma operation `(a,b) ∘ (c,d) = (b,c)`. These are special cases of central groupoids (Equation 168).
diff --git a/commentary/Equation28770.md b/commentary/Equation28770.md
deleted file mode 100644
index 40630f74d..000000000
--- a/commentary/Equation28770.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation 28770 `x = (((y ◇ y) ◇ y) ◇ x) ◇ (y ◇ z)`: An Austin law
-[Kisielewicz showed](https://teorth.github.io/equational_theories/blueprint/sect0001.html#Kisielewicz2) that this law is an Austin law: [it has no non-trivial finite models, but it has an infinite model](https://teorth.github.io/equational_theories/blueprint/infinite-model-chapter.html#kis-thm2). He also showed there is no shorter Austin law.
diff --git a/commentary/Equation345169.md b/commentary/Equation345169.md
deleted file mode 100644
index 6d65b4d31..000000000
--- a/commentary/Equation345169.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation 345169 `x = y ◇ ((x ◇ y) ◇ y) ◇ (x ◇ (z ◇ y))`: the Sheffer stroke law
-It was shown [by McCune, Veroff, Fitelson, Harris, Feist, and Wos](https://teorth.github.io/equational_theories/blueprint/sect0001.html#mccune_et_al) that [this law defines](https://teorth.github.io/equational_theories/blueprint/implications-chapter.html#sheffer) the [Sheffer stroke](https://en.wikipedia.org/wiki/Sheffer_stroke).
diff --git a/commentary/Equation3588.md b/commentary/Equation3588.md
deleted file mode 100644
index 7f877343e..000000000
--- a/commentary/Equation3588.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equations [3588 `x ◇ y = z ◇ ((x ◇ y) ◇ z)`](https://teorth.github.io/equational_theories/implications/?3588), [3994 `x ◇ y = (z ◇ (x ◇ y)) ◇ z`](https://teorth.github.io/equational_theories/implications/?3944): An Austin pair
-It was shown as part of this project that Equation 3944 implies Equation 3588 [for finite magmas](https://teorth.github.io/equational_theories/blueprint/infinite-model-chapter.html#finite_imp_3994_3588), but [not for infinite magmas](https://teorth.github.io/equational_theories/blueprint/infinite-model-chapter.html#non_imp_3994_3588_thm).
diff --git a/commentary/Equation374794.md b/commentary/Equation374794.md
deleted file mode 100644
index 6b40febe0..000000000
--- a/commentary/Equation374794.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation 374794 `x = (((y ◇ y) ◇ y) ◇ x) ◇ ((y ◇ y) ◇ z)`: An Austin law
-It was shown [by Kisielewicz](https://teorth.github.io/equational_theories/blueprint/sect0001.html#Kisielewicz) that this law is an Austin law: [it has no non-trivial finite models, but it has an infinite model](https://teorth.github.io/equational_theories/blueprint/infinite-model-chapter.html#kis-thm).
diff --git a/commentary/Equation381.md b/commentary/Equation381.md
deleted file mode 100644
index 82af46108..000000000
--- a/commentary/Equation381.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equations [381 `x ◇ y = (x ◇ z) ◇ y`](https://teorth.github.io/equational_theories/implications/?381), [3722 `x ◇ y = (x ◇ y) ◇ (x ◇ y)`](https://teorth.github.io/equational_theories/implications/?3722), [3744 `x ◇ y = (x ◇ z) ◇ (w ◇ y)`](https://teorth.github.io/equational_theories/implications/?3744): 1978 Putnam laws
-Problem A4 of the 1978 Putnam asked to show (in our language) that [Equation 3744 implies Equations 3722 and 381](https://teorth.github.io/equational_theories/blueprint/implications-chapter.html#3744_implies_3722_381). This Putnam question referred to 3744 as a "bypass law".
diff --git a/commentary/Equation387.md b/commentary/Equation387.md
deleted file mode 100644
index dc0851fa6..000000000
--- a/commentary/Equation387.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [387 `x ◇ y = (y ◇ y) ◇ x`](https://teorth.github.io/equational_theories/implications/?387): a law from MathOverflow
-[This response by pastebee](https://mathoverflow.net/a/450905/766) to a [MathOverflow question](https://mathoverflow.net/questions/450890/is-there-an-identity-between-the-commutative-identity-and-the-constant-identity) established that there was an equational law strictly between the constant law 46 and the commutative law 43, namely Equation 387.
diff --git a/commentary/Equation43.md b/commentary/Equation43.md
deleted file mode 100644
index 57241a180..000000000
--- a/commentary/Equation43.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [43 `x ◇ y = y ◇ x`](https://teorth.github.io/equational_theories/implications/?43): the commutative law
-One of the most famous laws in all of algebra.
diff --git a/commentary/Equation4512.md b/commentary/Equation4512.md
deleted file mode 100644
index 6c0b99666..000000000
--- a/commentary/Equation4512.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [4512 `x ◇ (y ◇ z) = (x ◇ y) ◇ z`](https://teorth.github.io/equational_theories/implications/?4512): the associative law
-One of the most famous laws in all of algebra.
diff --git a/commentary/Equation46.md b/commentary/Equation46.md
deleted file mode 100644
index 47e8c4e24..000000000
--- a/commentary/Equation46.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [46 `x ◇ y = z ◇ w`](https://teorth.github.io/equational_theories/implications/?46): the constant law
-A very strong law, that makes the entire multiplication table constant.
diff --git a/commentary/Equation477.md b/commentary/Equation477.md
deleted file mode 100644
index 9cc9399c7..000000000
--- a/commentary/Equation477.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation [477 `x = y ◇ (x ◇ (y ◇ (y ◇ y)))`](https://teorth.github.io/equational_theories/implications/?477): a confluent law
-This law is a non-trivial example of a *confluent law*: a law in which every word has a unique shortest reduction using the law. This makes it possible to easily determine which other equations are implied by this law, giving anti-implications that were not obtainable by other means. See [this discussion](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Equation.20477).
diff --git a/commentary/Equation5105.md b/commentary/Equation5105.md
deleted file mode 100644
index 2d1c68609..000000000
--- a/commentary/Equation5105.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equation 5105 `x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ y))))`: A conjectural Austin law
-An Austin law is a law which has infinite models, but no non-trivial finite models. [Kisielewicz showed](https://teorth.github.io/equational_theories/blueprint/sect0001.html#Kisielewicz2) that [this law has no non-trivial finite models](https://teorth.github.io/equational_theories/blueprint/infinite-model-chapter.html#5105-nontrivial), but it remains open whether there is an infinite model.
diff --git a/commentary/Equation65.md b/commentary/Equation65.md
deleted file mode 100644
index 15df99cdc..000000000
--- a/commentary/Equation65.md
+++ /dev/null
@@ -1,2 +0,0 @@
-## Equations [65 `x = y ◇ (x ◇ (y ◇ x))`](https://teorth.github.io/equational_theories/implications/?65), [1491 `x = (y ◇ x) ◇ (y ◇ (y ◇ x))`](https://teorth.github.io/equational_theories/implications/?1491): "Asterix and Oberlix"
-Equation 65 is one of the simplest equations for which several outgoing implications remain unresolved, see [this ongoing discussion](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Equation.2065.20-.3E.20Equation.20359). In particular, it is unknown whether either of these equations implies the other, although 1491 implies all seven equations for which it is unknown whether 65 implies it. One of the issues is that there seems to be a difference of behavior between the finite and infinite models of these equations.
diff --git a/equational_theories/EquationLawConversion.lean b/equational_theories/EquationLawConversion.lean
deleted file mode 100644
index ae404fb74..000000000
--- a/equational_theories/EquationLawConversion.lean
+++ /dev/null
@@ -1,142 +0,0 @@
-import equational_theories.MagmaLaw
-
-open Law
-
-/-! Zero variables -/
-
-@[simp] theorem Fin0.match_eq (X : Sort _) (f : Fin 0 → X) : Fin.elim0 = f := by
- funext i
- cases i
- contradiction
-
-theorem Fin0.uncurry {X : Type _} (P : (Fin 0 → X) → Prop) : (∀ f : Fin 0 → X, P f) ↔
- P Fin.elim0 := by
- constructor
- · intro h
- apply h
- · intro h f
- simpa only [← match_eq]
-
-theorem models_iff_0 (law : MagmaLaw (Fin 0)) (G : Type _) [Magma G] : G ⊧ law ↔
- satisfiesPhi (Fin.elim0 (α := G)) law := by
- rw [satisfies, Fin0.uncurry]
-
-/-! One variable -/
-
-@[simp] theorem Fin1.match_eq (X : Sort _) (f : Fin 1 → X) : (fun | 0 => f 0) = f := by
- funext i
- match i with
- | 0 => rfl
-
-theorem Fin1.uncurry {X : Type _} (P : (Fin 1 → X) → Prop) : (∀ f : Fin 1 → X, P f) ↔
- ∀ x : X, P (fun | 0 => x) := by
- constructor
- · intro h _
- apply h
- · intro h f
- have := h (f 0)
- simpa only [match_eq]
-
-theorem models_iff_1 (law : MagmaLaw (Fin 1)) (G : Type _) [Magma G] : G ⊧ law ↔
- ∀ x : G, satisfiesPhi (fun | 0 => x) law := by
- rw [satisfies, Fin1.uncurry]
-
-/-! Two variables -/
-
-@[simp] theorem Fin2.match_eq (X : Sort _) (f : Fin 2 → X) : (fun | 0 => f 0 | 1 => f 1) = f := by
- funext i
- match i with
- | 0 | 1 => rfl
-
-theorem Fin2.uncurry {X : Type _} (P : (Fin 2 → X) → Prop) : (∀ f : Fin 2 → X, P f) ↔
- ∀ x y : X, P (fun | 0 => x | 1 => y) := by
- constructor
- · intro h _ _
- apply h
- · intro h f
- have := h (f 0) (f 1)
- simpa only [match_eq]
-
-theorem models_iff_2 (law : MagmaLaw (Fin 2)) (G : Type _) [Magma G] : G ⊧ law ↔
- ∀ x y : G, satisfiesPhi (fun | 0 => x | 1 => y) law := by
- rw [satisfies, Fin2.uncurry]
-
-/-! Three variables -/
-
-@[simp] theorem Fin3.match_eq (X : Sort _) (f : Fin 3 → X) : (fun | 0 => f 0 | 1 => f 1 | 2 => f 2) = f := by
- funext i
- match i with
- | 0 | 1 | 2 => rfl
-
-theorem Fin3.uncurry {X : Type _} (P : (Fin 3 → X) → Prop) : (∀ f : Fin 3 → X, P f) ↔
- ∀ x y z : X, P (fun | 0 => x | 1 => y | 2 => z) := by
- constructor
- · intro h _ _ _
- apply h
- · intro h f
- have := h (f 0) (f 1) (f 2)
- simpa only [match_eq]
-
-theorem models_iff_3 (law : MagmaLaw (Fin 3)) (G : Type _) [Magma G] : G ⊧ law ↔
- ∀ x y z : G, satisfiesPhi (fun | 0 => x | 1 => y | 2 => z) law := by
- rw [satisfies, Fin3.uncurry]
-
-/-! Four variables -/
-
-@[simp] theorem Fin4.match_eq (X : Sort _) (f : Fin 4 → X) : (fun | 0 => f 0 | 1 => f 1 | 2 => f 2 | 3 => f 3) = f := by
- funext i
- match i with
- | 0 | 1 | 2 | 3 => rfl
-
-theorem Fin4.uncurry {X : Type _} (P : (Fin 4 → X) → Prop) : (∀ f : Fin 4 → X, P f) ↔
- ∀ x y z w : X, P (fun | 0 => x | 1 => y | 2 => z | 3 => w) := by
- constructor
- · intro h _ _ _ _
- apply h
- · intro h f
- have := h (f 0) (f 1) (f 2) (f 3)
- simpa only [match_eq]
-
-theorem models_iff_4 (law : MagmaLaw (Fin 4)) (G : Type _) [Magma G] : G ⊧ law ↔
- ∀ x y z w : G, satisfiesPhi (fun | 0 => x | 1 => y | 2 => z | 3 => w) law := by
- rw [satisfies, Fin4.uncurry]
-
-/-! Five variables -/
-
-@[simp] theorem Fin5.match_eq (X : Sort _) (f : Fin 5 → X) : (fun | 0 => f 0 | 1 => f 1 | 2 => f 2 | 3 => f 3 | 4 => f 4) = f := by
- funext i
- match i with
- | 0 | 1 | 2 | 3 | 4 => rfl
-
-theorem Fin5.uncurry {X : Type _} (P : (Fin 5 → X) → Prop) : (∀ f : Fin 5 → X, P f) ↔
- ∀ x y z w v : X, P (fun | 0 => x | 1 => y | 2 => z | 3 => w | 4 => v) := by
- constructor
- · intro h _ _ _ _ _
- apply h
- · intro h f
- have := h (f 0) (f 1) (f 2) (f 3) (f 4)
- simpa only [match_eq]
-
-theorem models_iff_5 (law : MagmaLaw (Fin 5)) (G : Type _) [Magma G] : G ⊧ law ↔
- ∀ x y z w v : G, satisfiesPhi (fun | 0 => x | 1 => y | 2 => z | 3 => w | 4 => v) law := by
- rw [satisfies, Fin5.uncurry]
-
-/-! Six variables -/
-
-@[simp] theorem Fin6.match_eq (X : Sort _) (f : Fin 6 → X) : (fun | 0 => f 0 | 1 => f 1 | 2 => f 2 | 3 => f 3 | 4 => f 4 | 5 => f 5) = f := by
- funext i
- match i with
- | 0 | 1 | 2 | 3 | 4 | 5 => rfl
-
-theorem Fin6.uncurry {X : Type _} (P : (Fin 6 → X) → Prop) : (∀ f : Fin 6 → X, P f) ↔
- ∀ x y z w v u : X, P (fun | 0 => x | 1 => y | 2 => z | 3 => w | 4 => v | 5 => u) := by
- constructor
- · intro h _ _ _ _ _ _
- apply h
- · intro h f
- have := h (f 0) (f 1) (f 2) (f 3) (f 4) (f 5)
- simpa only [match_eq]
-
-theorem models_iff_6 (law : MagmaLaw (Fin 6)) (G : Type _) [Magma G] : G ⊧ law ↔
- ∀ x y z w v u : G, satisfiesPhi (fun | 0 => x | 1 => y | 2 => z | 3 => w | 4 => v | 5 => u) law := by
- rw [satisfies, Fin6.uncurry]
diff --git a/equational_theories/EquationsCommand.lean b/equational_theories/EquationsCommand.lean
index 57c5ab752..acb774948 100644
--- a/equational_theories/EquationsCommand.lean
+++ b/equational_theories/EquationsCommand.lean
@@ -1,24 +1,8 @@
import Lean
import equational_theories.Magma
import equational_theories.MagmaLaw
-import equational_theories.EquationLawConversion
-open Lean Elab Command Law
-
-def mkNatMagmaLaw (declName : Name) : ImportM NatMagmaLaw := do
- let { env, opts, .. } ← read
- IO.ofExcept <| unsafe env.evalConstCheck NatMagmaLaw opts ``NatMagmaLaw declName
-
-initialize magmaLawExt : PersistentEnvExtension Name (Name × NatMagmaLaw) (Array (Name × NatMagmaLaw)) ←
- registerPersistentEnvExtension {
- mkInitial := pure .empty
- addImportedFn := Array.concatMapM <| Array.mapM <| fun n ↦ do return (n, ← mkNatMagmaLaw n)
- addEntryFn := Array.push
- exportEntriesFn := .map Prod.fst
- }
-
-def getMagmaLaws {M} [Monad M] [MonadEnv M] : M (Array (Name × NatMagmaLaw)) := do
- return magmaLawExt.getState (← getEnv)
+open Lean Elab Command
/--
For a more concise syntax, but more importantly to speed up elaboration (where type inference
@@ -29,10 +13,7 @@ elab mods:declModifiers tk:"equation " i:num " := " tsyn:term : command => do
let G := mkIdent (← MonadQuotation.addMacroScope `G)
let inst := mkIdent (← MonadQuotation.addMacroScope `inst)
let eqName := mkIdent (.mkSimple s!"Equation{i.getNat}")
- let finLawName := mkIdent (.mkSimple s!"FinLaw{i.getNat}")
let lawName := mkIdent (.mkSimple s!"Law{i.getNat}")
- let finThmName := mkIdent (.str finLawName.getId "models_iff")
- let thmName := mkIdent (.str lawName.getId "models_iff")
let mut is := #[]
let t := tsyn.raw
-- Collect all identifiers to introduce them as parameters
@@ -60,20 +41,7 @@ elab mods:declModifiers tk:"equation " i:num " := " tsyn:term : command => do
| some idx => `(FreeMagma.Leaf $(quote idx.val))
| none => pure s
let mut tl : Term := ⟨tl⟩
- let freeMagmaSize := Syntax.mkNumLit (toString is.size)
- -- define law over `Fin n`
- elabCommand (← `(command| abbrev%$tk $finLawName : Law.MagmaLaw (Fin $freeMagmaSize) := $tl))
- -- compatibility between the `finLaw` and the original equation
- let modelsIffLemma : Ident := mkIdent (.mkSimple s!"models_iff_{is.size}")
- elabCommand (← `(command| abbrev%$tk $finThmName : ∀ (G : Type _) [$inst : Magma G], G ⊧ $finLawName ↔ $eqName G := $modelsIffLemma $finLawName))
- -- define the actual law over `Nat`
- elabCommand (← `(command| abbrev%$tk $lawName : Law.NatMagmaLaw := $tl))
- -- compatibility between the law and the original equation
- elabCommand (← `(command| abbrev%$tk $thmName : ∀ (G : Type _) [$inst : Magma G], G ⊧ $lawName ↔ $eqName G :=
- fun G _ ↦ Iff.trans (Law.satisfies_fin_satisfies_nat G $finLawName).symm ($finThmName G)))
- -- register the law
- modifyEnv (magmaLawExt.addEntry · (lawName.getId, ← (mkNatMagmaLaw lawName.getId).run
- { env := (← getEnv), opts := (← getOptions) }))
+ elabCommand (← `(command| abbrev%$tk $lawName : Law.MagmaLaw Nat := $tl))
Command.liftTermElabM do
let declMods ← elabModifiers mods
-- Create a decl named `declName`
diff --git a/equational_theories/FreeMagma.lean b/equational_theories/FreeMagma.lean
index 1c5da7c10..a855b0e6d 100644
--- a/equational_theories/FreeMagma.lean
+++ b/equational_theories/FreeMagma.lean
@@ -63,10 +63,4 @@ theorem evalInMagma_comp {α β} {G} [Magma G] (f : α → β) (g : β → G) :
intro x
induction x <;> simp [fmapFreeMagma, evalInMagma, *]
-lemma Fin0_impossible (x : FreeMagma (Fin 0)) : False := by
- induction x
- case Leaf l =>
- cases l; contradiction
- case Fork => assumption
-
end FreeMagma
diff --git a/equational_theories/Generated/All4x4Tables/src/check_correct.py b/equational_theories/Generated/All4x4Tables/src/check_correct.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/All4x4Tables/src/check_redundant.py b/equational_theories/Generated/All4x4Tables/src/check_redundant.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/All4x4Tables/src/double_check_3x3.py b/equational_theories/Generated/All4x4Tables/src/double_check_3x3.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/All4x4Tables/src/drive_c_parallel.py b/equational_theories/Generated/All4x4Tables/src/drive_c_parallel.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/All4x4Tables/src/dump_tables.py b/equational_theories/Generated/All4x4Tables/src/dump_tables.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/All4x4Tables/src/generate_combined_refutations.sh b/equational_theories/Generated/All4x4Tables/src/generate_combined_refutations.sh
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/All4x4Tables/src/generate_lean.py b/equational_theories/Generated/All4x4Tables/src/generate_lean.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/All4x4Tables/src/prune.py b/equational_theories/Generated/All4x4Tables/src/prune.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/All4x4Tables/src/write_equations.py b/equational_theories/Generated/All4x4Tables/src/write_equations.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/FinSearch/src/finite_magma.py b/equational_theories/Generated/FinSearch/src/finite_magma.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/FinSearch/src/finsearch.py b/equational_theories/Generated/FinSearch/src/finsearch.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/FinSearch/src/generate_lean.py b/equational_theories/Generated/FinSearch/src/generate_lean.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/FinSearch/src/parser.py b/equational_theories/Generated/FinSearch/src/parser.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/FinitePoly/src/finite_poly_generate_lean.py b/equational_theories/Generated/FinitePoly/src/finite_poly_generate_lean.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/FinitePoly/src/generate_refutations.py b/equational_theories/Generated/FinitePoly/src/generate_refutations.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/FinitePoly/src/utils.py b/equational_theories/Generated/FinitePoly/src/utils.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/LinearOps/src/check_correct.py b/equational_theories/Generated/LinearOps/src/check_correct.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/LinearOps/src/write_equations.py b/equational_theories/Generated/LinearOps/src/write_equations.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/SimpleRewrites/src/find_redundant.py b/equational_theories/Generated/SimpleRewrites/src/find_redundant.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/SimpleRewrites/src/find_simple_rewrites.py b/equational_theories/Generated/SimpleRewrites/src/find_simple_rewrites.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/SimpleRewrites/src/utils.py b/equational_theories/Generated/SimpleRewrites/src/utils.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/TrivialBruteforce/src/generate_refutations.py b/equational_theories/Generated/TrivialBruteforce/src/generate_refutations.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/VampireProven/Conjectures.lean b/equational_theories/Generated/VampireProven/Conjectures.lean
index 3c559f341..f96f07cb6 100644
--- a/equational_theories/Generated/VampireProven/Conjectures.lean
+++ b/equational_theories/Generated/VampireProven/Conjectures.lean
@@ -36,184 +36,3 @@ import Mathlib.Tactic.TypeStar
@[equational_result] conjecture Equation1486_not_implies_Equation1480 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1480 G
@[equational_result] conjecture Equation1486_not_implies_Equation167 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation167 G
@[equational_result] conjecture Equation219_not_implies_Equation880 : ∃ (G: Type) (_: Magma G), Equation219 G ∧ ¬ Equation880 G
-@[equational_result] conjecture Equation1884_not_implies_Equation4587 : ∃ (G: Type) (_: Magma G), Equation1884 G ∧ ¬ Equation4587 G
-@[equational_result] conjecture Equation2040_not_implies_Equation4584 : ∃ (G: Type) (_: Magma G), Equation2040 G ∧ ¬ Equation4584 G
-@[equational_result] conjecture Equation1958_not_implies_Equation4587 : ∃ (G: Type) (_: Magma G), Equation1958 G ∧ ¬ Equation4587 G
-@[equational_result] conjecture Equation2093_not_implies_Equation4587 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation4587 G
-@[equational_result] conjecture Equation1431_not_implies_Equation4269 : ∃ (G: Type) (_: Magma G), Equation1431 G ∧ ¬ Equation4269 G
-@[equational_result] conjecture Equation2291_not_implies_Equation4588 : ∃ (G: Type) (_: Magma G), Equation2291 G ∧ ¬ Equation4588 G
-@[equational_result] conjecture Equation1276_not_implies_Equation4273 : ∃ (G: Type) (_: Magma G), Equation1276 G ∧ ¬ Equation4273 G
-@[equational_result] conjecture Equation3161_not_implies_Equation1492 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation1492 G
-@[equational_result] conjecture Equation481_not_implies_Equation1492 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation1492 G
-@[equational_result] conjecture Equation115_not_implies_Equation4273 : ∃ (G: Type) (_: Magma G), Equation115 G ∧ ¬ Equation4273 G
-@[equational_result] conjecture Equation1630_not_implies_Equation4268 : ∃ (G: Type) (_: Magma G), Equation1630 G ∧ ¬ Equation4268 G
-@[equational_result] conjecture Equation1633_not_implies_Equation4268 : ∃ (G: Type) (_: Magma G), Equation1633 G ∧ ¬ Equation4268 G
-@[equational_result] conjecture Equation1443_not_implies_Equation4268 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation4268 G
-@[equational_result] conjecture Equation2126_not_implies_Equation152 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation152 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1483 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1483 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1485 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1485 G
-@[equational_result] conjecture Equation1486_not_implies_Equation166 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation166 G
-@[equational_result] conjecture Equation1486_not_implies_Equation152 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation152 G
-@[equational_result] conjecture Equation1486_not_implies_Equation1483 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1483 G
-@[equational_result] conjecture Equation1486_not_implies_Equation1485 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1485 G
-@[equational_result] conjecture Equation219_not_implies_Equation4588 : ∃ (G: Type) (_: Magma G), Equation219 G ∧ ¬ Equation4588 G
-@[equational_result] conjecture Equation3994_not_implies_Equation3456 : ∃ (G: Type) (_: Magma G), Equation3994 G ∧ ¬ Equation3456 G
-@[equational_result] conjecture Equation3994_not_implies_Equation3549 : ∃ (G: Type) (_: Magma G), Equation3994 G ∧ ¬ Equation3549 G
-@[equational_result] conjecture Equation3994_not_implies_Equation3511 : ∃ (G: Type) (_: Magma G), Equation3994 G ∧ ¬ Equation3511 G
-@[equational_result] conjecture Equation3994_not_implies_Equation3472 : ∃ (G: Type) (_: Magma G), Equation3994 G ∧ ¬ Equation3472 G
-@[equational_result] conjecture Equation3588_not_implies_Equation3862 : ∃ (G: Type) (_: Magma G), Equation3588 G ∧ ¬ Equation3862 G
-@[equational_result] conjecture Equation3588_not_implies_Equation3955 : ∃ (G: Type) (_: Magma G), Equation3588 G ∧ ¬ Equation3955 G
-@[equational_result] conjecture Equation3588_not_implies_Equation3917 : ∃ (G: Type) (_: Magma G), Equation3588 G ∧ ¬ Equation3917 G
-@[equational_result] conjecture Equation3588_not_implies_Equation3878 : ∃ (G: Type) (_: Magma G), Equation3588 G ∧ ¬ Equation3878 G
-@[equational_result] conjecture Equation2040_not_implies_Equation2050 : ∃ (G: Type) (_: Magma G), Equation2040 G ∧ ¬ Equation2050 G
-@[equational_result] conjecture Equation2093_not_implies_Equation3915 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation3915 G
-@[equational_result] conjecture Equation2093_not_implies_Equation3253 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation3253 G
-@[equational_result] conjecture Equation2093_not_implies_Equation3319 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation3319 G
-@[equational_result] conjecture Equation2093_not_implies_Equation3258 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation3258 G
-@[equational_result] conjecture Equation2093_not_implies_Equation1832 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation1832 G
-@[equational_result] conjecture Equation2093_not_implies_Equation1020 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation1020 G
-@[equational_result] conjecture Equation2093_not_implies_Equation411 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation411 G
-@[equational_result] conjecture Equation2093_not_implies_Equation8 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation8 G
-@[equational_result] conjecture Equation2093_not_implies_Equation1884 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation1884 G
-@[equational_result] conjecture Equation1431_not_implies_Equation1428 : ∃ (G: Type) (_: Magma G), Equation1431 G ∧ ¬ Equation1428 G
-@[equational_result] conjecture Equation2947_not_implies_Equation1832 : ∃ (G: Type) (_: Magma G), Equation2947 G ∧ ¬ Equation1832 G
-@[equational_result] conjecture Equation2947_not_implies_Equation1629 : ∃ (G: Type) (_: Magma G), Equation2947 G ∧ ¬ Equation1629 G
-@[equational_result] conjecture Equation2947_not_implies_Equation614 : ∃ (G: Type) (_: Magma G), Equation2947 G ∧ ¬ Equation614 G
-@[equational_result] conjecture Equation680_not_implies_Equation2847 : ∃ (G: Type) (_: Magma G), Equation680 G ∧ ¬ Equation2847 G
-@[equational_result] conjecture Equation680_not_implies_Equation1832 : ∃ (G: Type) (_: Magma G), Equation680 G ∧ ¬ Equation1832 G
-@[equational_result] conjecture Equation680_not_implies_Equation1629 : ∃ (G: Type) (_: Magma G), Equation680 G ∧ ¬ Equation1629 G
-@[equational_result] conjecture Equation680_not_implies_Equation2947 : ∃ (G: Type) (_: Magma G), Equation680 G ∧ ¬ Equation2947 G
-@[equational_result] conjecture Equation2128_not_implies_Equation1426 : ∃ (G: Type) (_: Magma G), Equation2128 G ∧ ¬ Equation1426 G
-@[equational_result] conjecture Equation1519_not_implies_Equation2035 : ∃ (G: Type) (_: Magma G), Equation1519 G ∧ ¬ Equation2035 G
-@[equational_result] conjecture Equation1519_not_implies_Equation2128 : ∃ (G: Type) (_: Magma G), Equation1519 G ∧ ¬ Equation2128 G
-@[equational_result] conjecture Equation1086_not_implies_Equation2644 : ∃ (G: Type) (_: Magma G), Equation1086 G ∧ ¬ Equation2644 G
-@[equational_result] conjecture Equation1086_not_implies_Equation1832 : ∃ (G: Type) (_: Magma G), Equation1086 G ∧ ¬ Equation1832 G
-@[equational_result] conjecture Equation1086_not_implies_Equation2710 : ∃ (G: Type) (_: Magma G), Equation1086 G ∧ ¬ Equation2710 G
-@[equational_result] conjecture Equation2132_not_implies_Equation1426 : ∃ (G: Type) (_: Magma G), Equation2132 G ∧ ¬ Equation1426 G
-@[equational_result] conjecture Equation2132_not_implies_Equation1515 : ∃ (G: Type) (_: Magma G), Equation2132 G ∧ ¬ Equation1515 G
-@[equational_result] conjecture Equation2132_not_implies_Equation1519 : ∃ (G: Type) (_: Magma G), Equation2132 G ∧ ¬ Equation1519 G
-@[equational_result] conjecture Equation3161_not_implies_Equation1426 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation1426 G
-@[equational_result] conjecture Equation3161_not_implies_Equation411 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation411 G
-@[equational_result] conjecture Equation3161_not_implies_Equation473 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation473 G
-@[equational_result] conjecture Equation3161_not_implies_Equation1515 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation1515 G
-@[equational_result] conjecture Equation3161_not_implies_Equation1488 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation1488 G
-@[equational_result] conjecture Equation3161_not_implies_Equation1519 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation1519 G
-@[equational_result] conjecture Equation3161_not_implies_Equation477 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation477 G
-@[equational_result] conjecture Equation1523_not_implies_Equation2035 : ∃ (G: Type) (_: Magma G), Equation1523 G ∧ ¬ Equation2035 G
-@[equational_result] conjecture Equation1523_not_implies_Equation2124 : ∃ (G: Type) (_: Magma G), Equation1523 G ∧ ¬ Equation2124 G
-@[equational_result] conjecture Equation1523_not_implies_Equation2128 : ∃ (G: Type) (_: Magma G), Equation1523 G ∧ ¬ Equation2128 G
-@[equational_result] conjecture Equation1523_not_implies_Equation2038 : ∃ (G: Type) (_: Magma G), Equation1523 G ∧ ¬ Equation2038 G
-@[equational_result] conjecture Equation1523_not_implies_Equation2132 : ∃ (G: Type) (_: Magma G), Equation1523 G ∧ ¬ Equation2132 G
-@[equational_result] conjecture Equation481_not_implies_Equation3050 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation3050 G
-@[equational_result] conjecture Equation481_not_implies_Equation3139 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation3139 G
-@[equational_result] conjecture Equation481_not_implies_Equation2035 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation2035 G
-@[equational_result] conjecture Equation481_not_implies_Equation2124 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation2124 G
-@[equational_result] conjecture Equation481_not_implies_Equation1488 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation1488 G
-@[equational_result] conjecture Equation481_not_implies_Equation3150 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation3150 G
-@[equational_result] conjecture Equation481_not_implies_Equation2128 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation2128 G
-@[equational_result] conjecture Equation481_not_implies_Equation3056 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation3056 G
-@[equational_result] conjecture Equation481_not_implies_Equation2038 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation2038 G
-@[equational_result] conjecture Equation481_not_implies_Equation2132 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation2132 G
-@[equational_result] conjecture Equation481_not_implies_Equation3161 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation3161 G
-@[equational_result] conjecture Equation481_not_implies_Equation2041 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation2041 G
-@[equational_result] conjecture Equation2541_not_implies_Equation1629 : ∃ (G: Type) (_: Magma G), Equation2541 G ∧ ¬ Equation1629 G
-@[equational_result] conjecture Equation2541_not_implies_Equation817 : ∃ (G: Type) (_: Magma G), Equation2541 G ∧ ¬ Equation817 G
-@[equational_result] conjecture Equation2497_not_implies_Equation4065 : ∃ (G: Type) (_: Magma G), Equation2497 G ∧ ¬ Equation4065 G
-@[equational_result] conjecture Equation2497_not_implies_Equation4118 : ∃ (G: Type) (_: Magma G), Equation2497 G ∧ ¬ Equation4118 G
-@[equational_result] conjecture Equation2497_not_implies_Equation3456 : ∃ (G: Type) (_: Magma G), Equation2497 G ∧ ¬ Equation3456 G
-@[equational_result] conjecture Equation2497_not_implies_Equation3522 : ∃ (G: Type) (_: Magma G), Equation2497 G ∧ ¬ Equation3522 G
-@[equational_result] conjecture Equation2497_not_implies_Equation3050 : ∃ (G: Type) (_: Magma G), Equation2497 G ∧ ¬ Equation3050 G
-@[equational_result] conjecture Equation2497_not_implies_Equation1832 : ∃ (G: Type) (_: Magma G), Equation2497 G ∧ ¬ Equation1832 G
-@[equational_result] conjecture Equation2497_not_implies_Equation1629 : ∃ (G: Type) (_: Magma G), Equation2497 G ∧ ¬ Equation1629 G
-@[equational_result] conjecture Equation2497_not_implies_Equation23 : ∃ (G: Type) (_: Magma G), Equation2497 G ∧ ¬ Equation23 G
-@[equational_result] conjecture Equation1443_not_implies_Equation4065 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation4065 G
-@[equational_result] conjecture Equation1443_not_implies_Equation4118 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation4118 G
-@[equational_result] conjecture Equation1443_not_implies_Equation4067 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation4067 G
-@[equational_result] conjecture Equation1443_not_implies_Equation3522 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation3522 G
-@[equational_result] conjecture Equation1443_not_implies_Equation3050 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation3050 G
-@[equational_result] conjecture Equation1443_not_implies_Equation2441 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation2441 G
-@[equational_result] conjecture Equation1443_not_implies_Equation1629 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation1629 G
-@[equational_result] conjecture Equation1443_not_implies_Equation23 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation23 G
-@[equational_result] conjecture Equation1443_not_implies_Equation3055 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation3055 G
-@[equational_result] conjecture Equation1443_not_implies_Equation1630 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation1630 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3862 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3862 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3877 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3877 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3955 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3955 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3918 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3918 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3993 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3993 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3456 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3456 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3511 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3511 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3512 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3512 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3457 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3457 G
-@[equational_result] conjecture Equation2126_not_implies_Equation3513 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation3513 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1426 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1426 G
-@[equational_result] conjecture Equation2126_not_implies_Equation151 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation151 G
-@[equational_result] conjecture Equation2126_not_implies_Equation2087 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation2087 G
-@[equational_result] conjecture Equation2126_not_implies_Equation2050 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation2050 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1478 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1478 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1481 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1481 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1428 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1428 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1484 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1484 G
-@[equational_result] conjecture Equation2126_not_implies_Equation2051 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation2051 G
-@[equational_result] conjecture Equation2126_not_implies_Equation2088 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation2088 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1479 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1479 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1429 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1429 G
-@[equational_result] conjecture Equation2126_not_implies_Equation2052 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation2052 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1427 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1427 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1482 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1482 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3862 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3862 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3877 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3877 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3955 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3955 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3918 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3918 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3993 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3993 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3456 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3456 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3511 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3511 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3512 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3512 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3457 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3457 G
-@[equational_result] conjecture Equation1486_not_implies_Equation3513 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation3513 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2035 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2035 G
-@[equational_result] conjecture Equation1486_not_implies_Equation151 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation151 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2087 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2087 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2050 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2050 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2124 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2124 G
-@[equational_result] conjecture Equation1486_not_implies_Equation1481 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1481 G
-@[equational_result] conjecture Equation1486_not_implies_Equation1428 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1428 G
-@[equational_result] conjecture Equation1486_not_implies_Equation1484 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1484 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2051 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2051 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2088 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2088 G
-@[equational_result] conjecture Equation1486_not_implies_Equation1479 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1479 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2036 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2036 G
-@[equational_result] conjecture Equation1486_not_implies_Equation1427 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1427 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2125 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2125 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2126 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2126 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2089 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2089 G
-@[equational_result] conjecture Equation1110_not_implies_Equation3862 : ∃ (G: Type) (_: Magma G), Equation1110 G ∧ ¬ Equation3862 G
-@[equational_result] conjecture Equation1110_not_implies_Equation3915 : ∃ (G: Type) (_: Magma G), Equation1110 G ∧ ¬ Equation3915 G
-@[equational_result] conjecture Equation1110_not_implies_Equation3253 : ∃ (G: Type) (_: Magma G), Equation1110 G ∧ ¬ Equation3253 G
-@[equational_result] conjecture Equation1110_not_implies_Equation3319 : ∃ (G: Type) (_: Magma G), Equation1110 G ∧ ¬ Equation3319 G
-@[equational_result] conjecture Equation1110_not_implies_Equation1832 : ∃ (G: Type) (_: Magma G), Equation1110 G ∧ ¬ Equation1832 G
-@[equational_result] conjecture Equation1110_not_implies_Equation1629 : ∃ (G: Type) (_: Magma G), Equation1110 G ∧ ¬ Equation1629 G
-@[equational_result] conjecture Equation1110_not_implies_Equation411 : ∃ (G: Type) (_: Magma G), Equation1110 G ∧ ¬ Equation411 G
-@[equational_result] conjecture Equation1110_not_implies_Equation8 : ∃ (G: Type) (_: Magma G), Equation1110 G ∧ ¬ Equation8 G
-@[equational_result] conjecture Equation1884_not_implies_Equation4666 : ∃ (G: Type) (_: Magma G), Equation1884 G ∧ ¬ Equation4666 G
-@[equational_result] conjecture Equation2040_not_implies_Equation4631 : ∃ (G: Type) (_: Magma G), Equation2040 G ∧ ¬ Equation4631 G
-@[equational_result] conjecture Equation1958_not_implies_Equation4666 : ∃ (G: Type) (_: Magma G), Equation1958 G ∧ ¬ Equation4666 G
-@[equational_result] conjecture Equation2093_not_implies_Equation4666 : ∃ (G: Type) (_: Magma G), Equation2093 G ∧ ¬ Equation4666 G
-@[equational_result] conjecture Equation1431_not_implies_Equation4316 : ∃ (G: Type) (_: Magma G), Equation1431 G ∧ ¬ Equation4316 G
-@[equational_result] conjecture Equation2291_not_implies_Equation4647 : ∃ (G: Type) (_: Magma G), Equation2291 G ∧ ¬ Equation4647 G
-@[equational_result] conjecture Equation1276_not_implies_Equation4332 : ∃ (G: Type) (_: Magma G), Equation1276 G ∧ ¬ Equation4332 G
-@[equational_result] conjecture Equation3161_not_implies_Equation2135 : ∃ (G: Type) (_: Magma G), Equation3161 G ∧ ¬ Equation2135 G
-@[equational_result] conjecture Equation481_not_implies_Equation2135 : ∃ (G: Type) (_: Magma G), Equation481 G ∧ ¬ Equation2135 G
-@[equational_result] conjecture Equation115_not_implies_Equation4332 : ∃ (G: Type) (_: Magma G), Equation115 G ∧ ¬ Equation4332 G
-@[equational_result] conjecture Equation1630_not_implies_Equation4282 : ∃ (G: Type) (_: Magma G), Equation1630 G ∧ ¬ Equation4282 G
-@[equational_result] conjecture Equation1633_not_implies_Equation4282 : ∃ (G: Type) (_: Magma G), Equation1633 G ∧ ¬ Equation4282 G
-@[equational_result] conjecture Equation1443_not_implies_Equation4282 : ∃ (G: Type) (_: Magma G), Equation1443 G ∧ ¬ Equation4282 G
-@[equational_result] conjecture Equation2126_not_implies_Equation2161 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation2161 G
-@[equational_result] conjecture Equation2126_not_implies_Equation1430 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation1430 G
-@[equational_result] conjecture Equation2126_not_implies_Equation2163 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation2163 G
-@[equational_result] conjecture Equation2126_not_implies_Equation2162 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation2162 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2161 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2161 G
-@[equational_result] conjecture Equation1486_not_implies_Equation1430 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation1430 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2163 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2163 G
-@[equational_result] conjecture Equation1486_not_implies_Equation2162 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2162 G
-@[equational_result] conjecture Equation219_not_implies_Equation4647 : ∃ (G: Type) (_: Magma G), Equation219 G ∧ ¬ Equation4647 G
diff --git a/equational_theories/Generated/VampireProven/Disproofs2.lean b/equational_theories/Generated/VampireProven/Disproofs2.lean
index 90755eee2..2448b63e2 100644
--- a/equational_theories/Generated/VampireProven/Disproofs2.lean
+++ b/equational_theories/Generated/VampireProven/Disproofs2.lean
@@ -81,11 +81,3 @@ theorem Equation854_not_implies_Equation1225 : ∃ (G: Type) (_: Magma G), Equat
@[equational_result]
theorem Equation3964_not_implies_Equation3456 : ∃ (G: Type) (_: Magma G), Equation3964 G ∧ ¬ Equation3456 G :=
⟨Fin 17, ⟨memoFinOp fun x y => [[1, 13, 0, 14, 16, 3, 9, 13, 1, 1, 2, 2, 8, 0, 3, 8, 4], [2, 5, 9, 11, 7, 6, 4, 5, 13, 2, 5, 5, 4, 8, 6, 4, 12], [0, 8, 1, 3, 4, 14, 2, 8, 0, 0, 9, 9, 13, 1, 14, 13, 16], [16, 7, 4, 0, 0, 15, 6, 7, 14, 16, 11, 11, 12, 3, 15, 12, 15], [3, 6, 14, 15, 0, 0, 12, 6, 16, 3, 7, 7, 11, 4, 0, 11, 15], [4, 12, 16, 15, 15, 0, 11, 12, 3, 4, 6, 6, 7, 14, 0, 7, 0], [13, 5, 8, 7, 6, 12, 5, 5, 9, 13, 4, 4, 4, 2, 12, 4, 11], [2, 5, 9, 11, 7, 6, 4, 5, 13, 2, 5, 5, 4, 8, 6, 4, 12], [0, 9, 1, 4, 14, 16, 8, 9, 1, 0, 13, 13, 2, 0, 16, 2, 3], [1, 13, 0, 14, 16, 3, 9, 13, 1, 1, 2, 2, 8, 0, 3, 8, 4], [8, 4, 13, 12, 11, 7, 4, 4, 2, 8, 5, 5, 5, 9, 7, 5, 6], [8, 4, 13, 12, 11, 7, 4, 4, 2, 8, 5, 5, 5, 9, 7, 5, 6], [9, 4, 2, 6, 12, 11, 5, 4, 8, 9, 4, 4, 5, 13, 11, 5, 7], [1, 2, 0, 16, 3, 4, 13, 2, 0, 1, 8, 8, 9, 1, 4, 9, 14], [4, 12, 16, 15, 15, 0, 11, 12, 3, 4, 6, 6, 7, 14, 0, 7, 0], [9, 4, 2, 6, 12, 11, 5, 4, 8, 9, 4, 4, 5, 13, 11, 5, 7], [14, 11, 3, 0, 15, 15, 7, 11, 4, 14, 12, 12, 6, 16, 15, 6, 0]][x.val]![y.val]!⟩, by decideFin!⟩
-
-@[equational_result]
-theorem Equation2126_not_implies_Equation166 : ∃ (G: Type) (_: Magma G), Equation2126 G ∧ ¬ Equation166 G :=
- ⟨Fin 21, ⟨memoFinOp fun x y => [[1, 1, 19, 1, 19, 1, 1, 19, 16, 19, 16, 1, 19, 16, 19, 1, 1, 16, 19, 16, 19], [15, 1, 5, 5, 5, 1, 11, 11, 16, 5, 16, 1, 15, 11, 15, 1, 1, 11, 5, 16, 11], [15, 1, 5, 5, 5, 1, 11, 11, 16, 5, 16, 1, 15, 11, 15, 1, 1, 11, 5, 16, 11], [17, 20, 7, 7, 7, 20, 17, 7, 17, 17, 20, 20, 17, 7, 17, 20, 20, 20, 20, 20, 7], [14, 0, 12, 9, 9, 8, 9, 12, 14, 14, 9, 8, 14, 12, 14, 8, 0, 12, 9, 0, 12], [4, 2, 18, 9, 9, 2, 9, 3, 4, 4, 9, 2, 4, 18, 4, 2, 2, 3, 9, 18, 3], [15, 1, 5, 5, 5, 1, 11, 11, 16, 5, 16, 1, 15, 11, 15, 1, 1, 11, 5, 16, 11], [4, 2, 7, 13, 7, 2, 13, 7, 4, 4, 20, 2, 4, 7, 4, 2, 2, 20, 20, 13, 7], [15, 15, 5, 5, 5, 11, 11, 11, 5, 5, 5, 5, 15, 11, 15, 15, 5, 11, 5, 11, 11], [4, 6, 18, 10, 10, 6, 10, 3, 4, 4, 10, 6, 4, 18, 4, 6, 6, 3, 10, 18, 3], [4, 6, 18, 10, 10, 6, 10, 3, 4, 4, 10, 6, 4, 18, 4, 6, 6, 3, 10, 18, 3], [17, 6, 7, 13, 7, 6, 13, 7, 17, 17, 20, 6, 17, 7, 17, 6, 6, 20, 20, 13, 7], [17, 2, 7, 13, 7, 2, 13, 7, 17, 17, 20, 2, 17, 7, 17, 2, 2, 20, 20, 13, 7], [19, 6, 19, 6, 19, 6, 6, 3, 6, 19, 6, 6, 19, 6, 19, 6, 6, 3, 19, 19, 3], [14, 0, 12, 9, 9, 8, 9, 12, 14, 14, 9, 8, 14, 12, 14, 8, 0, 12, 9, 0, 12], [14, 0, 12, 0, 14, 12, 0, 12, 14, 14, 0, 0, 14, 12, 14, 14, 0, 12, 0, 0, 12], [10, 19, 19, 10, 10, 8, 10, 10, 8, 19, 10, 8, 19, 10, 19, 8, 10, 19, 10, 19, 10], [14, 0, 12, 9, 9, 8, 9, 12, 14, 14, 9, 8, 14, 12, 14, 8, 0, 12, 9, 0, 12], [13, 2, 19, 13, 19, 2, 13, 13, 2, 19, 13, 2, 19, 2, 19, 2, 2, 13, 2, 13, 19], [14, 2, 12, 9, 9, 2, 9, 12, 14, 14, 9, 2, 14, 12, 14, 2, 2, 12, 9, 12, 12], [17, 10, 18, 10, 10, 17, 10, 18, 17, 17, 10, 18, 17, 18, 17, 17, 10, 17, 10, 18, 17]][x.val]![y.val]!⟩, by decideFin!⟩
-
-@[equational_result]
-theorem Equation1486_not_implies_Equation2052 : ∃ (G: Type) (_: Magma G), Equation1486 G ∧ ¬ Equation2052 G :=
- ⟨Fin 21, ⟨memoFinOp fun x y => [[1, 12, 12, 7, 7, 6, 14, 12, 18, 7, 18, 12, 0, 6, 19, 11, 18, 7, 6, 6, 18], [2, 8, 8, 10, 10, 19, 0, 0, 20, 10, 20, 8, 0, 19, 19, 8, 10, 20, 0, 19, 20], [1, 2, 2, 13, 13, 11, 0, 0, 1, 13, 1, 2, 0, 2, 11, 11, 11, 13, 0, 1, 1], [1, 2, 2, 10, 15, 11, 14, 12, 1, 15, 1, 2, 15, 2, 11, 11, 11, 15, 6, 1, 1], [2, 12, 12, 7, 4, 6, 4, 12, 9, 4, 9, 12, 4, 6, 19, 3, 11, 9, 6, 6, 9], [1, 2, 2, 7, 7, 11, 14, 5, 1, 7, 1, 2, 0, 2, 11, 11, 11, 7, 17, 1, 1], [2, 5, 5, 13, 13, 19, 4, 5, 18, 13, 18, 5, 4, 19, 19, 3, 18, 13, 6, 19, 18], [2, 3, 3, 7, 4, 17, 4, 5, 9, 4, 9, 3, 4, 17, 16, 3, 18, 9, 17, 17, 9], [1, 2, 2, 7, 15, 11, 0, 12, 1, 15, 1, 2, 15, 2, 11, 11, 11, 15, 0, 1, 1], [1, 8, 8, 10, 10, 17, 4, 0, 20, 10, 20, 8, 4, 17, 19, 8, 10, 20, 17, 17, 20], [2, 3, 3, 10, 4, 16, 4, 5, 9, 4, 9, 3, 4, 16, 16, 3, 10, 9, 6, 16, 9], [1, 5, 5, 13, 15, 16, 14, 5, 14, 15, 14, 5, 15, 16, 16, 8, 11, 15, 17, 16, 14], [1, 2, 2, 7, 7, 11, 0, 0, 1, 7, 1, 2, 4, 2, 11, 11, 11, 7, 0, 1, 1], [1, 3, 3, 7, 4, 17, 4, 12, 9, 4, 9, 3, 4, 17, 11, 3, 18, 9, 17, 17, 9], [1, 8, 8, 10, 10, 6, 0, 0, 20, 10, 20, 8, 4, 6, 19, 8, 10, 20, 6, 6, 20], [2, 12, 12, 13, 4, 17, 4, 12, 9, 4, 9, 12, 4, 17, 11, 11, 18, 9, 17, 17, 9], [1, 5, 5, 13, 13, 19, 14, 5, 14, 13, 14, 5, 4, 19, 19, 3, 10, 13, 6, 19, 14], [1, 5, 5, 13, 13, 19, 14, 5, 18, 13, 18, 5, 4, 19, 19, 11, 18, 13, 0, 19, 18], [1, 8, 8, 10, 10, 16, 0, 0, 20, 10, 20, 8, 4, 16, 16, 8, 10, 20, 17, 16, 20], [1, 5, 5, 13, 13, 19, 14, 5, 14, 13, 14, 5, 4, 19, 19, 3, 11, 13, 0, 19, 14], [1, 8, 8, 10, 10, 17, 0, 5, 20, 10, 20, 8, 4, 17, 19, 8, 10, 20, 17, 17, 20]][x.val]![y.val]!⟩, by decideFin!⟩
diff --git a/equational_theories/Generated/VampireProven/src/vampire_fin_counterexamples.py b/equational_theories/Generated/VampireProven/src/vampire_fin_counterexamples.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/VampireProven/src/vampire_proofs.py b/equational_theories/Generated/VampireProven/src/vampire_proofs.py
old mode 100755
new mode 100644
diff --git a/equational_theories/Generated/VampireProven/src/vampire_proofs_cyc.py b/equational_theories/Generated/VampireProven/src/vampire_proofs_cyc.py
index 61c2bdab8..94d4bac03 100644
--- a/equational_theories/Generated/VampireProven/src/vampire_proofs_cyc.py
+++ b/equational_theories/Generated/VampireProven/src/vampire_proofs_cyc.py
@@ -100,7 +100,6 @@ def leanify(proof, problem):
def get_problem(matrix, bad):
# ts = time.perf_counter()
impls = find_most_useful_implication(matrix, -1)
- print('Returned', impls)
# print('Time to get implications', time.perf_counter() - ts)
# if not impls:
# raise KeyboardInterrupt('No remaining pairs')
@@ -148,12 +147,12 @@ def get_problem(matrix, bad):
try:
out = subprocess.check_output(['~/Downloads/vampire', '--mode', 'casc_sat', '--cores', '0',
- '/proc/self/fd/0', '-t', '0.2'], input=pr.encode()).decode()
+ '/proc/self/fd/0', '-t', '2.5'], input=pr.encode()).decode()
except subprocess.CalledProcessError as e:
assert e.returncode == 1
try:
out = subprocess.check_output(['~/Downloads/vampire', '--mode', 'casc', '--cores', '0',
- '/proc/self/fd/0', '-t', '0.2'], input=pr.encode()).decode()
+ '/proc/self/fd/0', '-t', '2.5'], input=pr.encode()).decode()
except subprocess.CalledProcessError as e:
assert e.returncode == 1
tqdm.write(f'Could\'nt handle {problem}')
diff --git a/equational_theories/MagmaLaw.lean b/equational_theories/MagmaLaw.lean
index d7df86db4..796ec89cd 100644
--- a/equational_theories/MagmaLaw.lean
+++ b/equational_theories/MagmaLaw.lean
@@ -12,8 +12,6 @@ deriving DecidableEq
infix:60 " ≃ " => MagmaLaw.mk
-abbrev NatMagmaLaw := MagmaLaw Nat
-
end Law
open Law
@@ -143,20 +141,15 @@ private def fin_split {n} {α} (hn : n ≠ 0) (f : Fin n → α) : ∃ g : ℕ
unfold g
simp
-theorem satisfies_fin_satisfies_nat {n : Nat} (G : Type) [Magma G] (E : MagmaLaw (Fin n))
+theorem satisfies_fin_satisfies_nat {n : Nat} (hn : n ≠ 0) (G : Type) [Magma G] (E : MagmaLaw (Fin n))
: G ⊧ E ↔ G ⊧ E.fmap Fin.val := by
apply Iff.intro <;> intro h φ; simp only [ne_eq, satisfies, satisfiesPhi, MagmaLaw.fmap] at *
· repeat rw [← evalInMagma_comp Fin.val φ]
exact h (φ ∘ Fin.val)
· simp only [ne_eq, satisfies, satisfiesPhi, MagmaLaw.fmap] at *
- if hn:n=0 then
- subst hn
- have := FreeMagma.Fin0_impossible E.lhs
- contradiction
- else
- obtain ⟨φ', hφ'_val_eq_phi⟩ := fin_split hn φ
- have hφ' := h φ'
- repeat rw [← evalInMagma_comp Fin.val φ', hφ'_val_eq_phi] at hφ'
- exact hφ'
+ obtain ⟨φ', hφ'_val_eq_phi⟩ := fin_split hn φ
+ have hφ' := h φ'
+ repeat rw [← evalInMagma_comp Fin.val φ', hφ'_val_eq_phi] at hφ'
+ exact hφ'
end Law
diff --git a/equational_theories/Preorder.lean b/equational_theories/Preorder.lean
index 08c041717..6557c1780 100644
--- a/equational_theories/Preorder.lean
+++ b/equational_theories/Preorder.lean
@@ -71,15 +71,15 @@ instance : Preorder (MagmaLaw α) where
theorem implies_eq_singleton_models {l₁ l₂ : MagmaLaw α} : l₁ ≤ l₂ ↔ {l₁} ⊧ l₂ := by
simp only [LE.le, implies, models, satisfiesSet, Ctx, Set.mem_singleton_iff, forall_eq]
-theorem Law.implies_fin_implies_nat {n : Nat} {l₁ l₂ : MagmaLaw (Fin n)}
+theorem Law.implies_fin_implies_nat {n : Nat} (hn : n ≠ 0) {l₁ l₂ : MagmaLaw (Fin n)}
(h : l₁.implies l₂) : (l₁.fmap Fin.val).implies (l₂.fmap Fin.val) := by
intro G inst hG
- rw [← satisfies_fin_satisfies_nat G l₂]
- rw [← satisfies_fin_satisfies_nat G l₁] at hG
+ rw [← satisfies_fin_satisfies_nat hn G l₂]
+ rw [← satisfies_fin_satisfies_nat hn G l₁] at hG
exact h hG
-theorem Law.leq_fin_leq_nat {n : Nat} {l₁ l₂ : MagmaLaw (Fin n)} (h : l₁ ≤ l₂) :
+theorem Law.leq_fin_leq_nat {n : Nat} (hn : n ≠ 0) {l₁ l₂ : MagmaLaw (Fin n)} (h : l₁ ≤ l₂) :
l₁.fmap Fin.val ≤ l₂.fmap Fin.val :=
- implies_fin_implies_nat h
+ implies_fin_implies_nat hn h
end Law.MagmaLaw
diff --git a/home_page/implications/index.html b/home_page/implications/index.html
index 09a92c974..34f25f7b3 100644
--- a/home_page/implications/index.html
+++ b/home_page/implications/index.html
@@ -142,7 +142,6 @@ Oops! There's an issue with your equation
Equation Details
-