From dedf61ebee001ee912f778c5fb2c2e7e769b0d08 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Fri, 5 Jan 2024 05:46:24 -0600
Subject: [PATCH] Fix typos in la_tautology
---
spec/rule_list.tex | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index b8f4cab..0f1b08d 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -518,7 +518,7 @@ $\varphi_1 \lor \varphi_2$ % Checked: this is a proper disjunction not a cl
& (\currule) \\
\end{AletheX}
-It can be checked by using the procedure for \proofRule{la_generic} with
+It can be checked by using the procedure for \proofRule{la_generic}
while setting the arguments to $1$. Informally, the rule follows one of several
cases:
\begin{itemize}
@@ -528,7 +528,7 @@ cases:
\item $s_1 \geq d_1 \lor \neg (s_1 \geq d_2)$ where $d_1 = d_2$
\item $\neg (s_1 \leq d_1) \lor \neg(s_1 \geq d_2)$ where $d_1 < d_2$
\end{itemize}
-The inequalities $s_1 \bowtie d$ are are the result of applying normalization
+The inequalities $s_1 \bowtie d$ are the result of applying normalization
as for the rule \proofRule{la_generic}.
\end{RuleDescription}
--
GitLab