Clarification of some rules (indices etc.)

spec/rule_list.tex

@@ -82,15 +82,15 @@ serves only informational purpose.
   \begin{plContainer}
     \begin{plList}
       \proofsep& i.&
-      \varphi_1 , \dots , \varphi_i , \dots , \varphi_j ,\dots , \varphi_n
+      \varphi_1 , \dots , \varphi_k , \dots , \varphi_l ,\dots , \varphi_n
       &(\dots)\\
       \proofsep& j.& \top &(\currule\; i)\\
     \end{plList}
   \end{plContainer}
   and $\varphi_i$, $\varphi_j$ are such that
   \begin{align*}
-  \varphi_i &= \underbrace{\neg \dots \neg}_n \psi \\
-  \varphi_j &= \underbrace{\neg \dots \neg}_m \psi
+  \varphi_k &= \underbrace{\neg \dots \neg}_n \psi \\
+  \varphi_l &= \underbrace{\neg \dots \neg}_m \psi
   \end{align*}
   and one of $n, m$ is odd and the other even.  Either can be $0$.
 \end{proof-rule}
@@ -417,8 +417,9 @@ Either
 \begin{plList}
 \Gamma\proofsep& i_1.& t_1 \simeq t_2 &(\dots)\\
 \Gamma\proofsep& i_2.& t_2 \simeq t_3 &(\dots)\\
+      \plLine\\
 \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)\\
+\Gamma\proofsep& j.& t_1 \simeq t_{n+1} &(\currule\; i_1, \dots, i_n)\\
 \end{plList}
 \end{plContainer}
 or
@@ -426,8 +427,9 @@ or
 \begin{plList}
 \Gamma\proofsep& i_1.& \varphi_1 \leftrightarrow \varphi_2 &(\dots)\\
 \Gamma\proofsep& i_2.& \varphi_2 \leftrightarrow \varphi_3 &(\dots)\\
+      \plLine\\
 \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)\\
+\Gamma\proofsep& j.& \varphi_1 \leftrightarrow \varphi_{n+1} &(\currule\; i_1,\dots, i_n)\\
 \end{plList}
 \end{plContainer}
 
@@ -449,6 +451,7 @@ Either
 \begin{plContainer}
 \begin{plList}
 \Gamma\proofsep& i_1.& t_1 \simeq u_1 &(\dots)\\
+      \plLine\\
 \Gamma\proofsep& i_n.& t_n \simeq u_n &(\dots)\\
 \Gamma\proofsep& j.& \operatorname{f}(t_1, \dots, t_n) \simeq
 \operatorname{f}(u_1, \dots, u_n) &(\currule\;i_1, \dots, i_n)\\
@@ -459,6 +462,7 @@ or
 \begin{plContainer}
 \begin{plList}
 \Gamma\proofsep& i_1.& \varphi_1 \simeq \psi_1 &(\dots)\\
+      \plLine\\
 \Gamma\proofsep& i_n.& \varphi_n \simeq \psi_n &(\dots)\\
 \Gamma\proofsep& j.& \operatorname{P}(\varphi_1, \dots, \varphi_n) \leftrightarrow
 \operatorname{P}(\psi_1, \dots, \psi_n) &(\currule\;i_1, \dots, i_n)\\
@@ -566,20 +570,21 @@ done during clausification.
   \begin{plContainer}
     \begin{plList}
       \proofsep& i.& \varphi_1 \land \dots \land \varphi_n&(\dots)\\
-      \proofsep& j.& \varphi_i &(\currule\; i)\\
+      \proofsep& j.& \varphi_k &(\currule\; i)\\
     \end{plList}
   \end{plContainer}
 \end{proof-rule}
-
+and $1 \leq k \leq n$.
 
 \begin{proof-rule}{not_or}{veriT}
 \begin{plContainer}
 \begin{plList}
 \proofsep& i.& \neg (\varphi_1 \lor \dots \lor \varphi_n) &(\dots)\\
-\proofsep& j.& \neg \varphi_i &(\currule\; i)\\
+\proofsep& j.& \neg \varphi_k &(\currule\; i)\\
 \end{plList}
 \end{plContainer}
 \end{proof-rule}
+and $1 \leq k \leq n$.
 
 \begin{proof-rule}{or}{veriT}
 \begin{plContainer}