diff --git a/docs/paradoxes.tex b/docs/paradoxes.tex index 6e005eaccdbe774805f7aa3f35ba57629ba3a15d..4a77596fa9c27ec91e6eba259d2b57538a2c7227 100644 --- a/docs/paradoxes.tex +++ b/docs/paradoxes.tex @@ -79,7 +79,7 @@ With this lemma in hand, the proof of \thmref{thm:counterexample-1} is simple. \label{app:section:invariants-without-a-later} Now we come to the main paradox: if we remove the $\later$ from \ruleref{inv-open}, the logic becomes inconsistent. -The theorem is stated as general as possible so taht it also applies to previous, less powerful versions of Iris. +The theorem is stated as general as possible so that it also applies to previous, less powerful versions of Iris. \begin{thm} \label{thm:counterexample-2}