From e8ebc33363dbf03c5ea9ab6412c271e0d5a104b3 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Fri, 26 Nov 2021 11:50:24 +0100
Subject: [PATCH] Fix eq_congruent_preg.
This was a copy past error from the definition of eq_congruent.
The special "power" of eq_congruent_preg is the additional negation
---
spec/rule_list.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 18c00ad..33a7f4c 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -500,7 +500,7 @@ f(t_1, \dots, t_n) \simeq f(u_1, \dots, u_n)
\begin{plList}
\proofsep& i.&
\neg (t_1 \simeq u_1) , \dots , \neg (t_n \simeq u_n) ,
-P(t_1, \dots, t_n) \simeq P(u_1, \dots, u_n)
+\neg (P(t_1, \dots, t_n) \simeq P(u_1, \dots, u_n))
&(\currule)\\
\end{plList}
\end{plContainer}
--
GitLab