We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 7bb871c commit 48290b9Copy full SHA for 48290b9
Test/VeriFast/tasks/vTaskSwitchContext/README.md
@@ -504,7 +504,8 @@ Introducing lemmas to open and close the predicate helps us to hide this complex
504
Thereby, the main proof using these lemmas gets shorter.
505
However, the next section explains why this approach does not eliminate the complexity.
506
507
-Note that proofs for forward iteration cannot be reused for backwards iteration but requires separate proofs.
+Note that proofs for forward iteration cannot be reused for backwards iteration.
508
+Instead the latter requires separate proofs.
509
510
511
0 commit comments