Skip to content
Snippets Groups Projects
Commit e935525c authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Fix typos in example

parent dedf61eb
No related branches found
No related tags found
No related merge requests found
Pipeline #20303 passed
\subsection*{Unreleased} \subsection*{Unreleased}
Braking changes: Breaking changes:
\begin{itemize} \begin{itemize}
\item Allow arbitrary extra annotations in \texttt{assume} commands. \item Allow arbitrary extra annotations in \texttt{assume} commands.
\end{itemize} \end{itemize}
......
...@@ -858,12 +858,12 @@ expressed as a concrete proof. ...@@ -858,12 +858,12 @@ expressed as a concrete proof.
\begin{AletheVerb} \begin{AletheVerb}
(assume h1 (forall ((x S)) (P x))) (assume h1 (forall ((x S)) (P x)))
(assume h2 (not (forall ((y S)) (P y)))) (assume h2 (not (forall ((y S)) (P y))))
(anchor :step t5 :args ((:= x y))) (anchor :step t5 :args ((y S) (:= x y)))
(step t3 (cl (= x y)) :rule refl) (step t3 (cl (= x y)) :rule refl)
(step t4 (cl (= (P x) (P y))) :rule cong :premises (t3)) (step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))) (step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
:rule bind) :rule bind)
(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))) (step t6 (cl (not (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
(not (forall ((x S)) (P x))) (not (forall ((x S)) (P x)))
(forall ((y S)) (P y))) :rule equiv_pos2) (forall ((y S)) (P y))) :rule equiv_pos2)
(step t7 (cl) :rule resolution :premises (h1 h2 t5 t6)) (step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment