summaryrefslogtreecommitdiff
path: root/Test/dafny1/UltraFilter.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny1/UltraFilter.dfy')
-rw-r--r--Test/dafny1/UltraFilter.dfy10
1 files changed, 5 insertions, 5 deletions
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 61e86836..189ff2b5 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -22,9 +22,9 @@ class UltraFilter<G> {
{
if (M !in f) {
// instantiate 'g' with the following 'h'
- call h := H(f, S, M);
- call Lemma_HIsFilter(h, f, S, M);
- call Lemma_FHOrdering0(h, f, S, M);
+ var h := H(f, S, M);
+ Lemma_HIsFilter(h, f, S, M);
+ Lemma_FHOrdering0(h, f, S, M);
}
}
@@ -44,9 +44,9 @@ class UltraFilter<G> {
// call Lemma_H1(h, f, S, M, *, *);
assume (forall C, D :: C in h && D in h ==> C * D in h);
- call Lemma_H2(h, f, S, M);
+ Lemma_H2(h, f, S, M);
- call Lemma_H3(h, f, S, M);
+ Lemma_H3(h, f, S, M);
}
method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)