1 files changed, 0 insertions, 59 deletions
diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy
deleted file mode 100644
index c5651c90..00000000
--- a/Test/dafny0/CoPredicates.dfy
+++ /dev/null
@@ -1,59 +0,0 @@
-codatatype Stream<T> = Cons(head: T, tail: Stream);
-
-function Upward(n: int): Stream<int>
-{
-  Cons(n, Upward(n + 1))
-}
-
-copredicate Pos(s: Stream<int>)
-{
-  0 < s.head && Pos(s.tail)
-}
-
-copredicate X(s: Stream)
-{
-  X(s)
-}
-
-ghost method AlwaysLemma(s: Stream)
-  ensures X(s);
-{
-}
-
-function Doubles(n: int): Stream<int>
-{
-  Cons(2*n, Doubles(n + 1))
-}
-
-copredicate Even(s: Stream<int>)
-{
-  s.head % 2 == 0 && Even(s.tail)
-}
-
-ghost method Lemma0(n: int)
-  ensures Even(Doubles(n));
-{
-}
-
-function UpwardBy2(n: int): Stream<int>
-{
-  Cons(n, UpwardBy2(n + 2))
-}
-
-ghost method Lemma1(n: int)
-  ensures Even(UpwardBy2(2*n));  // error:  this is true, but Dafny can't prove it
-{
-}
-
-function U2(n: int): Stream<int>
-  requires n % 2 == 0;
-{
-  UpwardBy2(n)
-}
-
-// Postponed:
-//ghost method Lemma2(n: int)
-//  ensures Even(UpwardBy2(2*n));  // this is true, and Dafny can prove it
-//{
-//  assert Even(U2(2*n));  // ... thanks to this lemma
-//}