From 26b99f88f261046d41de26c2bbf18efa6778fd44 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 29 Nov 2021 17:20:41 -0300
Subject: [PATCH] [Calculus] Fix transitivity rule
It's n-ary.
---
spec/rule_list.tex | 14 ++++++++------
1 file changed, 8 insertions(+), 6 deletions(-)
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 20d9816..5f0decf 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -410,17 +410,19 @@ the context.
Either
\begin{plContainer}
\begin{plList}
-\Gamma\proofsep& i.& t_1 \simeq t_2 &(\dots)\\
-\Gamma\proofsep& j.& t_2 \simeq t_3 &(\dots)\\
-\Gamma\proofsep& k.& t_1 \simeq t_3 &(\currule; i, j)\\
+\Gamma\proofsep& i_1.& t_1 \simeq t_2 &(\dots)\\
+\Gamma\proofsep& i_2.& t_2 \simeq t_3 &(\dots)\\
+\Gamma\proofsep& i_n.& t_n \simeq t_{n+1} &(\dots)\\
+\Gamma\proofsep& j.& t_1 \simeq t_{n+1} &(\currule; i_1, \dots, i_n, j)\\
\end{plList}
\end{plContainer}
or
\begin{plContainer}
\begin{plList}
-\Gamma\proofsep& i.& \varphi_1 \leftrightarrow \varphi_2 &(\dots)\\
-\Gamma\proofsep& j.& \varphi_2 \leftrightarrow \varphi_3 &(\dots)\\
-\Gamma\proofsep& k.& \varphi_1 \leftrightarrow \varphi_3 &(\currule; i, j)\\
+\Gamma\proofsep& i_1.& \varphi_1 \leftrightarrow \varphi_2 &(\dots)\\
+\Gamma\proofsep& i_2.& \varphi_2 \leftrightarrow \varphi_3 &(\dots)\\
+\Gamma\proofsep& i_n.& \varphi_n \leftrightarrow \varphi_{n+1} &(\dots)\\
+\Gamma\proofsep& j.& \varphi_1 \leftrightarrow \varphi_{n+1} &(\currule; i_1,\dots, i_n, j)\\
\end{plList}
\end{plContainer}
--
GitLab