From df8503acb5d53f3a4a350e3ec3a0fc171a6d8185 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Wed, 17 Jul 2024 18:45:46 -0500
Subject: [PATCH] Add index to and_pos, or_neg, and, not_or
---
spec/changelog.tex | 6 +++++-
spec/rule_list.tex | 10 ++++++----
2 files changed, 11 insertions(+), 5 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index e2e3410..3904918 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -22,7 +22,11 @@ Breaking changes:
be \texttt{(x S) (:= (y S) x)}.
\item The arguments for \proofRule{forall_inst} have been changed to
no longer take the shape of bindings using \texttt{(:= x c)}.
- Instead, the list of instatiation terms must follow the variable order and cover all the respective bound variables.
+ Instead, the list of instatiation terms must follow the variable
+ order and cover all the respective bound variables.
+ \item The rules \proofRule{and_pos}, \proofRule{or_neg}, \proofRule{and},
+ \proofRule{not_or} now have one argument that indicates which subterm
+ they use.
\end{itemize}
\noindent
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 4b89550..44c3099 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -810,7 +810,7 @@ done during clausification.
\begin{RuleDescription}{and}
\begin{AletheX}
$i$. & \ctxsep & $\varphi_1 \land \cdots \land \varphi_n$ & ($\dots$) \\
-$j$. & \ctxsep & $\varphi_k$ & (\currule\;$i$) \\
+$j$. & \ctxsep & $\varphi_k$ & (\currule\;$i$)\, k\\
\end{AletheX}
and $1 \leq k \leq n$.
\end{RuleDescription}
@@ -818,7 +818,7 @@ and $1 \leq k \leq n$.
\begin{RuleDescription}{not_or}
\begin{AletheX}
$i$. & \ctxsep & $\neg (\varphi_1 \lor \cdots \lor \varphi_n)$ & ($\dots$) \\
-$j$. & \ctxsep & $\neg \varphi_k$ & (\currule\;$i$) \\
+$j$. & \ctxsep & $\neg \varphi_k$ & (\currule\;$i$)\, k\\
\end{AletheX}
and $1 \leq k \leq n$.
\end{RuleDescription}
@@ -931,7 +931,8 @@ $j$. & \ctxsep & $\neg\varphi_1, \neg\varphi_2$ & (\currule\;$i$) \\
\begin{RuleDescription}{and_pos}
\begin{AletheX}
-$i$. & \ctxsep & $\neg (\varphi_1 \land \cdots \land \varphi_n) , \varphi_k$ & \currule \\
+$i$. & \ctxsep & $\neg (\varphi_1 \land \cdots \land \varphi_n) , \varphi_k$ &
+ \currule\, k\\
\end{AletheX}
with $1 \leq k \leq n$.
\end{RuleDescription}
@@ -950,7 +951,8 @@ $i$. & \ctxsep & $\neg (\varphi_1 \lor \cdots \lor \varphi_n) , \varphi_1 , \dot
\begin{RuleDescription}{or_neg}
\begin{AletheX}
-$i$. & \ctxsep & $(\varphi_1 \lor \cdots \lor \varphi_n), \neg \varphi_k$ & \currule \\
+$i$. & \ctxsep & $(\varphi_1 \lor \cdots \lor \varphi_n), \neg \varphi_k$ &
+ \currule\, k\\
\end{AletheX}
with $1 \leq k \leq n$.
\end{RuleDescription}
--
GitLab