1 files changed, 0 insertions, 54 deletions
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
deleted file mode 100644
index c7e4bc63..00000000
--- a/Test/dafny1/pow2.dfy
+++ /dev/null
@@ -1,54 +0,0 @@
-// This is a Dafny adaptation of a Coq program by David Pichardie.
-
-function IsEven(n: int): bool
-  requires 0 <= n;
-  ensures IsEven(n) ==> n == (n/2)+(n/2);
-{
-  (n/2)*2 == n
-}
-
-function Square(n: int): int { n * n }
-
-function pow2(n: int): int
-  requires 0 <= n;
-  ensures 0 <= pow2(n);
-{
-  if n == 0 then
-    1
-  else if IsEven(n) then
-    Square(pow2(n / 2))
-  else
-    2*pow2(n-1)
-
-}
-
-function pow2_slow(n: int): int
-  requires 0 <= n;
-{
-  if n == 0 then
-    1
-  else
-    2*pow2_slow(n-1)
-}
-
-ghost method Lemma(n: int)
-  requires 0 <= n && IsEven(n);
-  ensures pow2_slow(n) == Square(pow2_slow(n/2));
-{
-  if (n != 0) {
-    Lemma(n-2);
-  }
-}
-
-ghost method Theorem(n: int)
-  requires 0 <= n;
-  ensures pow2(n) == pow2_slow(n);
-{
-  if (n == 0) {
-  } else if (IsEven(n)) {
-    Lemma(n);
-    Theorem(n/2);
-  } else {
-    Theorem(n-1);
-  }
-}