From 1471cb81cd25dab2cd80423097c2250ce8925679 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Wed, 7 Aug 2024 16:46:30 -0500
Subject: [PATCH] Add or_intro rule
---
spec/changelog.tex | 2 ++
spec/rule_list.tex | 10 ++++++++++
2 files changed, 12 insertions(+)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index 807045a..65f5a42 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -11,6 +11,8 @@ Proof rules:
of equality explicitly but as an equivalence. Note that in principle this
could be done with the rule \proofRule{symm} above, but would require a long
and tedious use of \proofRule{subproof} for each direction of the equivalence.
+ \item Addition of the rule \proofRule{or_intro} to express weakening of a
+ clause.
\end{itemize}
\noindent
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 508cfa0..645b87d 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -263,6 +263,7 @@ simplifications.}
\label{rule-tab:cvc5}\\
Rule & Description \\
\hline
+\ruleref{or_intro} & Weakening of a clause. \\
\ruleref{eq_symmetric} & Symmetry of equality as equivalence. \\
\end{xltabular}
\subsection{Rule List}
@@ -844,6 +845,15 @@ An application of the \proofRule{or} rule.
\end{AletheVerb}
\end{RuleExample}
+\begin{RuleDescription}{or_intro}
+\begin{AletheX}
+$i$. & \ctxsep &
+$\varphi_1, \cdots, \varphi_n$ & ($\dots$) \\
+$j$. & \ctxsep & $\varphi_1, \cdots, \varphi_n, \psi_1, \dots, \psi_m$ & (\currule\;$i$) \\
+\end{AletheX}
+where $m \geq 1$.
+\end{RuleDescription}
+
\begin{RuleDescription}{not_and}
\begin{AletheX}
$i$. & \ctxsep & $\neg (\varphi_1 \land \dots \land \varphi_n)$ & ($\dots$) \\
--
GitLab