diff options
Diffstat (limited to 'Test/vstte2012/Combinators.dfy')
| -rw-r--r-- | Test/vstte2012/Combinators.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy index 46daf48d..dcc2e22d 100644 --- a/Test/vstte2012/Combinators.dfy +++ b/Test/vstte2012/Combinators.dfy @@ -225,7 +225,7 @@ ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term) // that FindAndStep(b) gives C[Step(u)].
return Apply(t.car, r), value_C(t.car, C), u;
} else {
- parallel (C,u | IsContext(C) && t == EvalExpr(C,u))
+ forall C,u | IsContext(C) && t == EvalExpr(C,u)
ensures Step(u) == u;
{
// The following assert and the first assert of each "case" are
@@ -442,7 +442,7 @@ ghost method VerificationTask3() ensures forall n: nat ::
TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);
{
- parallel (n: nat) {
+ forall n: nat {
VT3(n);
}
}
|