diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index e2f5e90861c042a526205eec437db9b7c2475835..34a9dbfcce8ff62313a92ff8f9b7a0794982a526 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -360,7 +360,7 @@ To express the adequacy statement for functional correctness, we assume that the
 The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound.
 The adequacy statement now reads as follows:
 \begin{align*}
- &\All \mask, \expr, \val, \pred, \state.
+ &\All \mask, \expr, \val, \state.
  \\&( \TRUE \proves {\upd}_\mask \Exists S. S(\state) * \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
  \\&\expr, \state \vDash V
 \end{align*}