From 5f5939fedb2e99bf3abea6a358ce3dcb9478f9f8 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Mon, 9 Jan 2023 09:25:50 -0600
Subject: [PATCH] Remove redundant simplification from `implies_simplify`

The simplification `(P -> Q) -> Q => P or Q` is already covered
by `bool_simplify`.
---
 spec/changelog.tex | 7 +++++++
 spec/rule_list.tex | 1 -
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/spec/changelog.tex b/spec/changelog.tex
index 0589563..49acb41 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -26,6 +26,13 @@ following changes were implemented in this release.
   \item An index that lists all proof rules was added.
 \end{itemize}
 
+Proof rules:
+\begin{itemize}
+  \item The rule \proofRule{implies_simplify} is no longer allowed to
+  perform the simplification $(\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2
+  ⇒  \varphi_1\lor \varphi_2$.  This is covered by \proofRule{bool_simplify}.
+\end{itemize}
+
 \subsection*{0.2 --- \DTMdisplaydate{2022}{12}{19}{-1}}
 
 This is an intermediate release.  It collects all changes to the original
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index c9c1b4d..83130c4 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1084,7 +1084,6 @@ The possible transformations are:
     \item $ \varphi \rightarrow  \varphi ⇒ \top$
     \item $\neg \varphi \rightarrow  \varphi ⇒  \varphi$
     \item $ \varphi \rightarrow \neg \varphi ⇒ \neg \varphi$
-    \item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2 ⇒  \varphi_1\lor \varphi_2$
 \end{itemize}
 \end{RuleDescription}
 
-- 
GitLab