From 74c140930a9cf8226325ab658af5e69c7074b78b Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Mon, 6 May 2024 12:10:25 -0500
Subject: [PATCH] Fix example for onepoint proof rule
Addresses https://gitlab.uliege.be/verit/alethe/-/issues/40
---
spec/changelog.tex | 1 +
spec/rule_list.tex | 4 ++--
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index 9f203ea..0da3149 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -23,6 +23,7 @@ Clarifications and corrected errors:
omitted if the list is empty.
\item Fix mistake in proof grammar. It now uses the \texttt{context\_annotation}
non-terminal in the rule for the \texttt{anchor} command.
+ \item Fix the example of \proofRule{onepoint}.
\end{itemize}
\subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}}
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 2152cda..f19f928 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1227,7 +1227,7 @@ An application of the \proofRule{onepoint} rule on the term $(\forall x, y.\, x
\rightarrow (f\,x)\land (f\,y))$ look like this:
\begin{AletheVerb}
-(anchor :step t3 :args ((:= y x)))
+(anchor :step t3 :args ((x S) (:= (y S) x)))
(step t3.t1 (cl (= x y)) :rule refl)
(step t3.t2 (cl (= (= x y) (= x x)))
:rule cong :premises (t3.t1))
@@ -1242,7 +1242,7 @@ An application of the \proofRule{onepoint} rule on the term $(\forall x, y.\, x
(step t3 (cl (=
(forall ((x S) (y S)) (=> (= x y) (and (f x) (f y))))
(forall ((x S)) (=> (= x x) (and (f x) (f x))))))
- :rule qnt_simplify)
+ :rule onepoint)
\end{AletheVerb}
\end{RuleExample}
--
GitLab