From a80976ccc77871b44d0716285260ceac920e1a21 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 29 Nov 2021 17:03:38 -0300
Subject: [PATCH] [Calculus] Fix conclusion of not_ite2
---
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 791852c..20d9816 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -915,7 +915,7 @@ with $1 \leq k \leq n$.
\begin{plContainer}
\begin{plList}
\proofsep& i.& \neg(\operatorname{ite}\varphi_1\;\varphi_2\;\varphi_3) &(\dots)\\
-\proofsep& j.& \neg\varphi_2 , \neg\varphi_2 &(\currule; i)\\
+\proofsep& j.& \neg\varphi_1 , \neg\varphi_2 &(\currule; i)\\
\end{plList}
\end{plContainer}
\end{proof-rule}
--
GitLab