From cec7d2de78c63bf6c959b2b861e03bfd2bcd5eab Mon Sep 17 00:00:00 2001
From: Nicholas Carlini <nicholas@carlini.com>
Date: Thu, 26 Sep 2024 19:51:36 -0700
Subject: [PATCH] Correct typo: Equation4522 is sometimes called Equation 4552

---
 blueprint/src/chapter/counterexamples.tex |  2 +-
 blueprint/src/chapter/equations.tex       |  2 +-
 equational_theories/Basic.lean            | 10 +++++-----
 images/implications.svg                   |  2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/blueprint/src/chapter/counterexamples.tex b/blueprint/src/chapter/counterexamples.tex
index 34c557eb..d3760035 100644
--- a/blueprint/src/chapter/counterexamples.tex
+++ b/blueprint/src/chapter/counterexamples.tex
@@ -55,7 +55,7 @@ \chapter{Counterexamples}
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := x \cdot y + 1$.
 \end{proof}
 
-\begin{theorem}[4513 does not imply 4552]\label{4513_not_imply_4552}\lean{Equation4513_not_implies_Equation4552}\leanok\uses{eq4513,eq4552} Definition \ref{eq4513} does not imply Definition \ref{eq4552}.
+\begin{theorem}[4513 does not imply 4522]\label{4513_not_imply_4522}\lean{Equation4513_not_implies_Equation4522}\leanok\uses{eq4513,eq4522} Definition \ref{eq4513} does not imply Definition \ref{eq4522}.
 \end{theorem}
 
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y$ equal to $1$ if $x=0$ and $y \leq 2$, $2$ if $x=0$ and $y>2$, and $x$ otherwise.
diff --git a/blueprint/src/chapter/equations.tex b/blueprint/src/chapter/equations.tex
index ecfe596a..b453dd23 100644
--- a/blueprint/src/chapter/equations.tex
+++ b/blueprint/src/chapter/equations.tex
@@ -57,7 +57,7 @@ \chapter{Equations}
 \begin{definition}[Equation 4513]\label{eq4513}\lean{Equation4513}\leanok\uses{magma-def}  Equation 4513 is the law $x \circ (y \circ z) = (x \circ y) \circ w$.
 \end{definition}
 
-\begin{definition}[Equation 4552]\label{eq4552}\lean{Equation4552}\leanok\uses{magma-def}  Equation 4552 is the law $x \circ (y \circ z) = (x \circ w) \circ u$.
+\begin{definition}[Equation 4522]\label{eq4522}\lean{Equation4522}\leanok\uses{magma-def}  Equation 4522 is the law $x \circ (y \circ z) = (x \circ w) \circ u$.
 \end{definition}
 
 \begin{definition}[Equation 4582]\label{eq4582}\lean{Equation4582}\leanok\uses{magma-def}  Equation 4582 is the law $x \circ (y \circ z) = (w \circ u) \circ v$.
diff --git a/equational_theories/Basic.lean b/equational_theories/Basic.lean
index 4acccc9c..98f86d28 100644
--- a/equational_theories/Basic.lean
+++ b/equational_theories/Basic.lean
@@ -59,7 +59,7 @@ def Equation4512 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ (y ∘ z) = (x ∘
 
 def Equation4513 (G: Type*) [Magma G] := ∀ x y z w : G, x ∘ (y ∘ z) = (x ∘ y) ∘ w
 
-def Equation4552 (G: Type*) [Magma G] := ∀ x y z w u : G, x ∘ (y ∘ z) = (x ∘ w) ∘ u
+def Equation4522 (G: Type*) [Magma G] := ∀ x y z w u : G, x ∘ (y ∘ z) = (x ∘ w) ∘ u
 
 def Equation4582 (G: Type*) [Magma G] := ∀ x y z w u v: G, x ∘ (y ∘ z) = (w ∘ u) ∘ v
 
@@ -97,7 +97,7 @@ theorem Equation4_implies_Equation42 (G: Type*) [Magma G] (h: Equation4 G) : Equ
   intro _ _ _
   rw [<-h, <-h]
 
-theorem Equation4_implies_Equation4552 (G: Type*) [Magma G] (h: Equation4 G) : Equation4552 G := by
+theorem Equation4_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4 G) : Equation4522 G := by
   intro x y z w u
   rw [<-h, <-h, <-h]
 
@@ -124,10 +124,10 @@ theorem Equation387_implies_Equation43 (G: Type*) [Magma G] (h: Equation387 G) :
 theorem Equation4513_implies_Equation4512 (G: Type*) [Magma G] (h: Equation4513 G) : Equation4512 G :=
   fun _ _ _ => h _ _ _ _
 
-theorem Equation4552_implies_Equation4513 (G: Type*) [Magma G] (h: Equation4552 G) : Equation4513 G :=
+theorem Equation4522_implies_Equation4513 (G: Type*) [Magma G] (h: Equation4522 G) : Equation4513 G :=
   fun _ _ _ _ => h _ _ _ _ _
 
-theorem Equation4582_implies_Equation4552 (G: Type*) [Magma G] (h: Equation4582 G) : Equation4552 G :=
+theorem Equation4582_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4582 G) : Equation4522 G :=
   fun _ _ _ _ _ => h _ _ _ _ _ _
 
 
@@ -339,7 +339,7 @@ theorem Equation4512_not_implies_Equation4513 : ∃ (G: Type) (_: Magma G), Equa
   dsimp [hG] at h
   linarith
 
-theorem Equation4513_not_implies_Equation4552 : ∃ (G: Type) (_: Magma G), Equation4513 G ∧ ¬ Equation4552 G := by
+theorem Equation4513_not_implies_Equation4522 : ∃ (G: Type) (_: Magma G), Equation4513 G ∧ ¬ Equation4522 G := by
   let hG : Magma Nat := {
     op := fun x y => if x = 0 then (if y ≤ 2 then 1 else 2) else x
   }
diff --git a/images/implications.svg b/images/implications.svg
index 7bdd19e7..84a76233 100644
--- a/images/implications.svg
+++ b/images/implications.svg
@@ -1419,7 +1419,7 @@
          ns6:version="1.10.2"
          ns6:texconverter="pdflatex"
          ns6:pdfconverter="inkscape"
-         ns6:text="$x\\circ (y\\circ z)=(x\\circ w)\\circ u\\ (4552)$"
+         ns6:text="$x\\circ (y\\circ z)=(x\\circ w)\\circ u\\ (4522)$"
          ns6:preamble="C:\Users\teort\AppData\Roaming\inkscape\extensions\textext\default_packages.tex"
          ns6:scale="1.0"
          ns6:alignment="middle center"