Metatheorem resolving all consequences of Equation1571

equational_theories/AllEquations.lean

@@ -3185,7 +3185,7 @@ equation 3163 := x = (((y ◇ y) ◇ z) ◇ y) ◇ x
 equation 3164 := x = (((y ◇ y) ◇ z) ◇ y) ◇ y
 equation 3165 := x = (((y ◇ y) ◇ z) ◇ y) ◇ z
 equation 3166 := x = (((y ◇ y) ◇ z) ◇ y) ◇ w
-equation 3167 := x = (((y ◇ y) ◇ z) ◇ z) ◇ x
+-- equation 3167 := x = (((y ◇ y) ◇ z) ◇ z) ◇ x
 equation 3168 := x = (((y ◇ y) ◇ z) ◇ z) ◇ y
 equation 3169 := x = (((y ◇ y) ◇ z) ◇ z) ◇ z
 equation 3170 := x = (((y ◇ y) ◇ z) ◇ z) ◇ w
@@ -4674,7 +4674,7 @@ equation 4652 := (x ◇ y) ◇ x = (z ◇ w) ◇ w
 equation 4653 := (x ◇ y) ◇ x = (z ◇ w) ◇ u
 equation 4654 := (x ◇ y) ◇ y = (x ◇ y) ◇ z
 equation 4655 := (x ◇ y) ◇ y = (x ◇ z) ◇ y
-equation 4656 := (x ◇ y) ◇ y = (x ◇ z) ◇ z
+-- equation 4656 := (x ◇ y) ◇ y = (x ◇ z) ◇ z
 equation 4657 := (x ◇ y) ◇ y = (x ◇ z) ◇ w
 equation 4658 := (x ◇ y) ◇ y = (y ◇ x) ◇ x
 equation 4659 := (x ◇ y) ◇ y = (y ◇ x) ◇ z

equational_theories/Equations.lean

@@ -90,6 +90,8 @@ equation 1689  :=  x = (y ◇ x) ◇ ((x ◇ z) ◇ z)
 
 equation 2662  :=  x = ((x ◇ y) ◇ (x ◇ y)) ◇ x
 
+abbrev Equation3167 (G: Type _) [Magma G] := ∀ x y z : G, x = (((y ◇ y) ◇ z) ◇ z) ◇ x
+
 /-- From Putnam 1978, Problem A4, part (a) -/
 equation 3722  :=  x ◇ y = (x ◇ y) ◇ (x ◇ y)
 
@@ -114,6 +116,7 @@ equation 4579  :=  x ◇ (y ◇ z) = (w ◇ u) ◇ z
 /-- all products of three values are the same, regardless bracketing -/
 equation 4582  :=  x ◇ (y ◇ z) = (w ◇ u) ◇ v
 
+abbrev Equation4656 (G: Type _) [Magma G] := ∀ x y z : G, (x ◇ y) ◇ y = (x ◇ z) ◇ z
 
 /- Some order 5 laws -/
 

equational_theories/FreeSemigroup.lean

@@ -0,0 +1,194 @@
+import Mathlib.Logic.Basic
+
+import equational_theories.Equations
+import equational_theories.FreeMagma
+import equational_theories.Homomorphisms
+import equational_theories.MagmaLaw
+
+open FreeMagma
+open Law
+
+def treeConcat {α : Type _} (t : FreeMagma α) : List α :=
+  match t with
+    | Lf a      => [a]
+    | (tl ⋆ tr) => treeConcat tl ++ treeConcat tr
+
+def rightJoinTrees {α : Type _} (t1 t2 : FreeMagma α) : FreeMagma α :=
+  match t1 with
+    | Lf a      =>  Lf a ⋆ t2
+    | (tl ⋆ tr) => tl ⋆ (rightJoinTrees tr t2)
+
+def rightAssociateTree {α : Type _} (t : FreeMagma α) : FreeMagma α :=
+  match t with
+    | Lf a      => Lf a
+    | (tl ⋆ tr) => rightJoinTrees (rightAssociateTree tl) (rightAssociateTree tr)
+
+theorem AssocImpliesForkEquivRightJoin {α : Type _} {G : Type _} [Magma G]
+  (assoc : Equation4512 G) (f : α → G) (tl tr : FreeMagma α)
+  : evalInMagma f (tl ⋆ tr) = evalInMagma f (rightJoinTrees tl tr) :=
+  match tl with
+    | Lf _        => Eq.refl _
+    | (tl1 ⋆ tl2) => Eq.trans
+      (Eq.symm $ assoc (evalInMagma f tl1) (evalInMagma f tl2) (evalInMagma f tr))
+      (congrArg (fun t ↦ (evalInMagma f tl1) ◇ t) (AssocImpliesForkEquivRightJoin assoc f tl2 tr))
+
+/- Associativity allows us to fully right-associate an entire operation tree -/
+theorem AssocFullyRightAssociate {α : Type _} {G : Type _} [Magma G]
+  (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α)
+  : evalInMagma f t = evalInMagma f (rightAssociateTree t) :=
+  match t with
+    | Lf _      => Eq.refl _
+    | (tl ⋆ tr) => Eq.trans
+      (congrArg (fun s ↦ s ◇ (evalInMagma f tr)) (AssocFullyRightAssociate assoc f tl)) $ Eq.trans
+      (congrArg (fun s ↦ (evalInMagma f (rightAssociateTree tl)) ◇ s) (AssocFullyRightAssociate assoc f tr))
+      (AssocImpliesForkEquivRightJoin assoc f (rightAssociateTree tl) (rightAssociateTree tr))
+
+/-- Example usage of AssocFullyRightAssociate -/
+theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G)
+  : ∀ x y z w : G, ((x ◇ y) ◇ z) ◇ w = x ◇ (y ◇ (z ◇ w)) :=
+  fun x y z w ↦ AssocFullyRightAssociate
+    assoc
+    (fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G)
+    (((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3)
+
+inductive FreeSemigroup (α : Type _)
+  | Singleton : α → FreeSemigroup α
+  | Cons : α → FreeSemigroup α → FreeSemigroup α
+
+local postfix:61 ".+" => FreeSemigroup.Singleton
+local infixr:60 " ,+ " => FreeSemigroup.Cons
+
+def semigroupConcat {α : Type _} (s1 s2 : FreeSemigroup α) : FreeSemigroup α :=
+  match s1 with
+    | a .+        => a ,+ s2
+    | a ,+ s1tail => a ,+ (semigroupConcat s1tail s2)
+
+instance (α : Type _) : Magma (FreeSemigroup α) where
+  op := semigroupConcat
+
+theorem FreeSgrAssoc {α : Type} : Equation4512 (FreeSemigroup α) :=
+  fun ls1 ls2 ls3 ↦ match ls1 with
+    | _ .+      => Eq.refl _
+    | a ,+ ls1' => congrArg (fun ls ↦ a ,+ ls) (FreeSgrAssoc ls1' ls2 ls3)
+
+/- "Flatten" a FreeMagma tree expression into its semigroup representation -/
+def freeMagmaToFreeSgr {α : Type _} : MagmaHom (FreeMagma α) (FreeSemigroup α) where
+  toFun := fun t ↦ evalInMagma FreeSemigroup.Singleton t
+  map_op' := fun s _ ↦ match s with
+    | Lf _ => Eq.refl _
+    | _ ⋆ _ => Eq.refl _
+
+local postfix:70 " ↠Sgr " => freeMagmaToFreeSgr.toFun
+
+def evalInSgr {α : Type _} {G : Type _} [Magma G] (f : α → G) (ls : FreeSemigroup α) : G :=
+  match ls with
+    | a .+ => f a
+    | a ,+ lstail => f a ◇ evalInSgr f lstail
+
+def evalInSgrHom {α : Type _} {G : Type _} [Magma G] (assoc : Equation4512 G) (f : α → G) : MagmaHom (FreeSemigroup α) G where
+  toFun := evalInSgr f
+  map_op' := let rec mapper : ∀ ls1 ls2 : FreeSemigroup α, evalInSgr f (ls1 ◇ ls2) = evalInSgr f ls1 ◇ evalInSgr f ls2 :=
+    fun ls1 ls2 ↦ match ls1 with
+      | _ .+      => Eq.refl _
+      | a ,+ ls1' => Eq.trans
+        (congrArg (fun x ↦ f a ◇ x) (mapper ls1' ls2))
+        (assoc (f a) (evalInSgr f ls1') (evalInSgr f ls2))
+    mapper
+
+def foldFreeSemigroup {G : Type _} [Magma G] (ls : FreeSemigroup G) : G :=
+  match ls with
+    | a .+        => a
+    | a ,+ lstail => a ◇ (foldFreeSemigroup lstail)
+
+/- When evaluating in an associative structure, we may reduce a FreeMagma tree to a FreeSemigroup list -/
+theorem AssocImpliesSgrProjFaithful {α : Type _} {G : Type _} [Magma G] (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α)
+  : evalInMagma f t = evalInSgr f (freeMagmaToFreeSgr t) :=
+  match t with
+    | Lf a => Eq.refl _
+    | Lf a ⋆ tr => congrArg (fun y ↦ (f a) ◇ y) (AssocImpliesSgrProjFaithful assoc f tr)
+    | (tl1 ⋆ tl2) ⋆ tr => by
+      apply Eq.symm
+      apply Eq.trans $ congrArg (evalInSgr f) $ freeMagmaToFreeSgr.map_op' (tl1 ⋆ tl2) tr
+      apply Eq.trans $ congrArg (fun s ↦ evalInSgr f (s ◇ tr ↠Sgr)) $ freeMagmaToFreeSgr.map_op' tl1 tl2
+      apply Eq.trans $ (evalInSgrHom assoc f).map_op' (tl1 ↠Sgr ◇ tl2 ↠Sgr) (tr ↠Sgr)
+      apply Eq.trans $ congrArg (fun s ↦ s ◇ (evalInSgr f (tr ↠Sgr))) $ (evalInSgrHom assoc f).map_op' (tl1 ↠Sgr) (tl2 ↠Sgr)
+      apply Eq.symm
+      apply Eq.trans $ congrArg (fun s ↦ _ ◇ s) (AssocImpliesSgrProjFaithful assoc f tr)
+      apply Eq.trans $ congrArg (fun s ↦ (s ◇ _) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl1)
+      apply Eq.trans $ congrArg (fun s ↦ (_ ◇ s) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl2)
+      trivial
+
+def insertSgrSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
+  match ls with
+    | j .+        => if i ≤ j then i ,+ j .+ else j ,+ i .+
+    | j ,+ lstail => if i ≤ j then i ,+ j ,+ lstail else j ,+ i ,+ lstail
+
+def insertionSortSgr {n : Nat} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) :=
+  match ls with
+    | i .+ => i .+
+    | i ,+ lstail => insertSgrSorted i (insertionSortSgr lstail)
+
+theorem CommSgrImpliesInsertSortedFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
+  : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSgrSorted i ls) = (f i) ◇ evalInSgr f ls :=
+  fun i ls ↦ match ls with
+  | j .+ => by
+    have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+)
+    cases eqor with
+    | inl eq1 => apply Eq.trans (congrArg (evalInSgr f) eq1); exact Eq.refl _
+    | inr eq2 => apply Eq.trans (congrArg (evalInSgr f) eq2); exact comm (f j) (f i)
+  | j ,+ lstail => by
+    have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j ,+ lstail) (j ,+ i ,+ lstail)
+    cases eqor with
+    | inl eq1 =>
+      apply Eq.trans (congrArg (evalInSgr f) eq1);
+      exact Eq.refl _
+    | inr eq2 =>
+      apply Eq.trans (congrArg (evalInSgr f) eq2);
+      apply Eq.trans $ assoc (f j) (f i) _;
+      rw [comm (f j) (f i)];
+      exact Eq.symm $ assoc (f i) (f j) _
+
+theorem CommSgrImpliesInsertionSortFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G)
+  : ∀ ls : FreeSemigroup (Fin n), evalInSgr f ls = evalInSgr f (insertionSortSgr ls)
+  | _ .+        => Eq.refl _
+  | i ,+ lstail => Eq.trans
+    (congrArg (fun s ↦ (f i) ◇ s) (CommSgrImpliesInsertionSortFaithful assoc comm f lstail))
+    (Eq.symm $ CommSgrImpliesInsertSortedFaithful assoc comm f i (insertionSortSgr lstail))
+
+def involutionReduce {α : Type _} [DecidableEq α] (ls : FreeSemigroup α) : FreeSemigroup α :=
+  match ls with
+  | a .+              => a .+
+  | a ,+ b .+         => a ,+ b .+
+  | a ,+ b ,+ lstail  => if (a = b) then involutionReduce lstail else a ,+ involutionReduce (b ,+ lstail)
+
+def InvolutiveImpliesInvolutionReduceFaithful {α : Type _} [DecidableEq α] {G : Type _} [Magma G] (ls : FreeSemigroup α) (invol : Equation16 G) (f : α → G)
+  : evalInSgr f ls = evalInSgr f (involutionReduce ls) :=
+  match ls with
+  | a .+              => Eq.refl _
+  | a ,+ b .+         => Eq.refl _
+  | a ,+ b ,+ lstail  => by
+    have eqor := dite_eq_or_eq (P := a = b) (A := fun _ ↦ involutionReduce lstail) (B := fun _ ↦ a ,+ involutionReduce (b ,+ lstail))
+    cases eqor with
+    | inl eqcase =>
+      apply Eq.trans $ congrArg (fun s ↦ (f s) ◇ (f b ◇ (evalInSgr f lstail))) eqcase.1
+      apply Eq.trans $ Eq.symm $ invol (evalInSgr f lstail) (f b)
+      apply Eq.trans $ InvolutiveImpliesInvolutionReduceFaithful lstail invol f
+      exact Eq.symm $ congrArg (evalInSgr f) eqcase.2
+    | inr neqcase =>
+      apply Eq.symm
+      apply Eq.trans $ congrArg (evalInSgr f) neqcase.2
+      exact congrArg (fun s ↦ f a ◇ s) $ Eq.symm $ InvolutiveImpliesInvolutionReduceFaithful (b ,+ lstail) invol f
+
+def equation1571Reducer {n : Nat} (t : FreeMagma (Fin (n+1))) : FreeSemigroup (Fin (n+1)) :=
+  involutionReduce $ insertionSortSgr $ freeMagmaToFreeSgr (t ⋆ (Lf (Fin.last n) ⋆ Lf (Fin.last n)))
+
+def AbGrpPow2ImpliesEquation1571ReducerFaithful {n : Nat} {G : Type _} [Magma G] (t : FreeMagma (Fin (n+1))) (f : Fin (n+1) → G)
+  (assoc : Equation4512 G) (comm : Equation43 G) (invol : Equation16 G)
+  : evalInMagma f t = evalInSgr f (equation1571Reducer t) := by
+  apply Eq.symm
+  apply Eq.trans $ Eq.symm $ InvolutiveImpliesInvolutionReduceFaithful _ invol f
+  apply Eq.trans $ Eq.symm $ CommSgrImpliesInsertionSortFaithful assoc comm f _
+  apply Eq.trans $ Eq.symm $ AssocImpliesSgrProjFaithful assoc f _
+  apply Eq.trans $ comm (evalInMagma f t) _
+  apply Eq.trans $ Eq.symm $ assoc _ _ _
+  exact Eq.symm $ invol (evalInMagma f t) (f $ Fin.last n)

equational_theories/Subgraph.lean

@@ -4,6 +4,8 @@ import equational_theories.EquationalResult
 import equational_theories.Closure
 import equational_theories.Equations
 import equational_theories.FactsSyntax
+import equational_theories.FreeSemigroup
+import equational_theories.MagmaLaw
 
 /- This is a subproject of the main project to completely describe a small subgraph of the entire
 implication graph. The list of equations under consideration can be found at https://teorth.github.io/equational_theories/blueprint/subgraph-eq.html
@@ -282,44 +284,66 @@ theorem Lemma_eq1689_implies_h8 (G: Type*) [Magma G] (h: Equation1689 G) : ∀ a
 
 /-- The below results for Equation1571 are out of order because early ones are lemmas for later ones -/
 @[equational_result]
-theorem Equation1571_implies_Equation2662 (G: Type*) [Magma G] (h: Equation1571 G) : Equation2662 G :=
-  fun _ _ ↦ (h _ _ _).trans (congrArg _ (h _ _ _).symm)
+theorem Equation1571_implies_Equation2662 (G: Type _) [Magma G] (h: Equation1571 G) : Equation2662 G :=
+  fun x y ↦ Eq.trans (h x (x ◇ y) (x ◇ y)) (congrArg (fun z ↦ ((x ◇ y) ◇ (x ◇ y)) ◇ z)
+    (Eq.symm $ h x x y))
 
 @[equational_result]
-theorem Equation1571_implies_Equation40 (G: Type*) [Magma G] (h: Equation1571 G) : Equation40 G := by
-  have sqRotate (x y z : G) : (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z) :=
-    (congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w)) (Equation1571_implies_Equation2662 G h _ _)).trans
-      (h _ _ _).symm
-  exact fun x y ↦ h x x x ▸ h y y y ▸ (sqRotate _ _ _).trans (sqRotate _ _ _)
+theorem Equation1571_implies_Equation40 (G: Type _) [Magma G] (h: Equation1571 G) : Equation40 G := by
+  have sqRotate : ∀ x y z : G, (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z) :=
+    fun x y z ↦ Eq.trans (congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w))
+      (Equation1571_implies_Equation2662 G h y z)) (Eq.symm $ h ((y ◇ z) ◇ (y ◇ z)) x y)
+  have sqConstInImage : ∀ x y z w : G, (x ◇ y) ◇ (x ◇ y) = (z ◇ w) ◇ (z ◇ w) :=
+    fun x y z w ↦ Eq.trans (sqRotate x y z) (sqRotate y z w)
+  exact fun x y ↦ h x x x ▸ h y y y ▸ sqConstInImage (x ◇ x) (x ◇ (x ◇ x)) (y ◇ y) (y ◇ (y ◇ y))
 
 @[equational_result]
-theorem Equation1571_implies_Equation23 (G: Type*) [Magma G] (h: Equation1571 G) : Equation23 G := by
-  refine fun x ↦ (h x (x ◇ x) (x ◇ x)).trans ?_
+theorem Equation1571_implies_Equation23 (G: Type _) [Magma G] (h: Equation1571 G) : Equation23 G := by
+  refine fun x ↦ Eq.trans (h x (x ◇ x) (x ◇ x)) ?_
   rw [← h x x x, ← Equation1571_implies_Equation40 G h x (x ◇ x)]
 
 @[equational_result]
-theorem Equation1571_implies_Equation8 (G: Type*) [Magma G] (h: Equation1571 G) : Equation8 G :=
-  fun x ↦ (h x x x).trans ((congrArg (· ◇ (x ◇ (x ◇ x))) (Equation1571_implies_Equation40 G h x
-    (x ◇ (x ◇ x)))).trans (Equation1571_implies_Equation23 G h (x ◇ (x ◇ x))).symm)
+theorem Equation1571_implies_Equation8 (G: Type _) [Magma G] (h: Equation1571 G) : Equation8 G :=
+  fun x ↦ Eq.trans (h x x x) (((congrArg (fun a ↦ a ◇ (x ◇ (x ◇ x))))
+    (Equation1571_implies_Equation40 G h x (x ◇ (x ◇ x)))).trans
+      (((Equation1571_implies_Equation23 G h (x ◇ (x ◇ x))).symm).trans rfl))
 
 @[equational_result]
-theorem Equation1571_implies_Equation16 (G: Type*) [Magma G] (h: Equation1571 G) : Equation16 G :=
+theorem Equation1571_implies_Equation16 (G: Type _) [Magma G] (h: Equation1571 G) : Equation16 G :=
   fun x y ↦ ((congrArg (fun w ↦ y ◇ (y ◇ w)) (Equation1571_implies_Equation8 G h x)).trans
-    (Equation1571_implies_Equation40 G h x y ▸ ((congrArg (· ◇ (y ◇ (x ◇ (y ◇ y)))))
-      (Equation1571_implies_Equation8 G h y)).trans (h x y (y ◇ y)).symm)).symm
+    ((Equation1571_implies_Equation40 G h x y ▸ ((congrArg (fun w ↦ w ◇ (y ◇ (x ◇ (y ◇ y)))))
+      (Equation1571_implies_Equation8 G h y)).trans (h x y (y ◇ y)).symm))).symm
 
 @[equational_result]
-theorem Equation1571_implies_Equation43 (G: Type*) [Magma G] (h: Equation1571 G) : Equation43 G := by
+theorem Equation1571_implies_Equation43 (G: Type _) [Magma G] (h: Equation1571 G) : Equation43 G := by
   refine fun x y ↦ (h _ (x ◇ x) (x ◇ (x ◇ y))).trans ?_
   rw [← h x x y, ← Equation1571_implies_Equation23 G h x, ← Equation1571_implies_Equation16 G h y x,
     Equation1571_implies_Equation40 G h x y, ← Equation1571_implies_Equation23 G h y]
 
 @[equational_result]
-theorem Equation1571_implies_Equation4512 (G: Type*) [Magma G] (h: Equation1571 G) : Equation4512 G := by
+theorem Equation1571_implies_Equation4512 (G: Type _) [Magma G] (h: Equation1571 G) : Equation4512 G := by
   refine fun x y z ↦ (h (x ◇ (y ◇ z)) y x).trans ?_
-  rw [Equation1571_implies_Equation43 G h (x ◇ (y ◇ z)) x,
-    ← Equation1571_implies_Equation16 G h (y ◇ z) x, ← Equation1571_implies_Equation16 G h z y,
-      Equation1571_implies_Equation43 G h y x]
+  rw [Equation1571_implies_Equation43 G h (x ◇ (y ◇ z)) x, ← Equation1571_implies_Equation16 G h (y ◇ z) x, ← Equation1571_implies_Equation16 G h z y, Equation1571_implies_Equation43 G h y x]
+
+theorem ProveEquation1571Consequence {n : Nat} {G : Type _} [Magma G] (eq1571 : Equation1571 G)
+    (law : Law.MagmaLaw (Fin (n+1))) (eq : equation1571Reducer law.lhs = equation1571Reducer law.rhs)
+    : G ⊧ law :=
+  fun _ ↦ (AbGrpPow2ImpliesEquation1571ReducerFaithful law.lhs _
+    (Equation1571_implies_Equation4512 G eq1571) (Equation1571_implies_Equation43 G eq1571)
+      (Equation1571_implies_Equation16 G eq1571)).trans ((congrArg (evalInSgr _) eq).trans
+        (AbGrpPow2ImpliesEquation1571ReducerFaithful law.rhs _
+          (Equation1571_implies_Equation4512 G eq1571) (Equation1571_implies_Equation43 G eq1571)
+            (Equation1571_implies_Equation16 G eq1571)).symm)
+
+/- Example usage of the general-purpose prover ProveEquation1571Consequence -/
+theorem Equation1571_implies_Equation3167 {G : Type} [Magma G] (h : Equation1571 G) : Equation3167 G :=
+  fun x y z ↦ ProveEquation1571Consequence (n := 2) h
+    {lhs := Lf 0, rhs := (((Lf 1 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 2) ⋆ Lf 0} rfl fun | 0 => x | 1 => y | 2 => z
+
+/- Example usage of the general-purpose prover ProveEquation1571Consequence -/
+theorem Equation1571_implies_Equation4656 {G : Type} [Magma G] (h : Equation1571 G) : Equation4656 G :=
+  fun x y z ↦ ProveEquation1571Consequence (n := 2) h
+    {lhs := (Lf 0 ⋆ Lf 1) ⋆ Lf 1, rhs := (Lf 0 ⋆ Lf 2) ⋆ Lf 2} rfl fun | 0 => x | 1 => y | 2 => z
 
 /-- This result was first obtained by Kisielewicz in 1997 via computer assistance. -/
 @[equational_result]