diff options
Diffstat (limited to 'Test/dafny3/Dijkstra.dfy')
| -rw-r--r-- | Test/dafny3/Dijkstra.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy index d3ff244a..7497618c 100644 --- a/Test/dafny3/Dijkstra.dfy +++ b/Test/dafny3/Dijkstra.dfy @@ -28,8 +28,8 @@ ghost method lemma_ping(j: nat, n: nat) j <= n;
{ lemma_ping(j - 1, n - 1); }
j - 1 <= f(n - 1);
- { lemma_ping(j - 1, f(n - 1)); }
- ==> j - 1 <= f(f(n - 1));
+ ==> { lemma_ping(j - 1, f(n - 1)); }
+ j - 1 <= f(f(n - 1));
// (0)
j - 1 <= f(f(n - 1)) && f(f(n - 1)) < f(n);
==> j - 1 < f(n);
|