Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories.

2 files changed, 0 insertions, 1223 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
deleted file mode 100644
index 342b72c1..00000000
--- a/Binaries/DafnyPrelude.bpl
+++ /dev/null
@@ -1,649 +0,0 @@
-// Dafny prelude

-// Created 9 February 2008 by Rustan Leino.

-// Converted to Boogie 2 on 28 June 2008.

-// Edited sequence axioms 20 October 2009 by Alex Summers.

-// Copyright (c) 2008-2010, Microsoft.

-

-const $$Language$Dafny: bool;  // To be recognizable to the ModelViewer as

-axiom $$Language$Dafny;        // coming from a Dafny program.

-

-// ---------------------------------------------------------------

-// -- References -------------------------------------------------

-// ---------------------------------------------------------------

-

-type ref;

-const null: ref;

-

-// ---------------------------------------------------------------

-// -- Axiomatization of sets -------------------------------------

-// ---------------------------------------------------------------

-

-type Set T = [T]bool;

-

-function Set#Empty<T>(): Set T;

-axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);

-

-function Set#Singleton<T>(T): Set T;

-axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);

-axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);

-

-function Set#UnionOne<T>(Set T, T): Set T;

-axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }

-  Set#UnionOne(a,x)[o] <==> o == x || a[o]);

-axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }

-  Set#UnionOne(a, x)[x]);

-axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }

-  a[y] ==> Set#UnionOne(a, x)[y]);

-

-function Set#Union<T>(Set T, Set T): Set T;

-axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }

-  Set#Union(a,b)[o] <==> a[o] || b[o]);

-axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), a[y] }

-  a[y] ==> Set#Union(a, b)[y]);

-axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), b[y] }

-  b[y] ==> Set#Union(a, b)[y]);

-axiom (forall<T> a, b: Set T :: { Set#Union(a, b) }

-  Set#Disjoint(a, b) ==>

-    Set#Difference(Set#Union(a, b), a) == b &&

-    Set#Difference(Set#Union(a, b), b) == a);

-

-function Set#Intersection<T>(Set T, Set T): Set T;

-axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }

-  Set#Intersection(a,b)[o] <==> a[o] && b[o]);

-

-axiom (forall<T> a, b: Set T :: { Set#Union(Set#Union(a, b), b) }

-  Set#Union(Set#Union(a, b), b) == Set#Union(a, b));

-axiom (forall<T> a, b: Set T :: { Set#Union(a, Set#Union(a, b)) }

-  Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));

-axiom (forall<T> a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) }

-  Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));

-axiom (forall<T> a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }

-  Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));

-

-function Set#Difference<T>(Set T, Set T): Set T;

-axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }

-  Set#Difference(a,b)[o] <==> a[o] && !b[o]);

-axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }

-  b[y] ==> !Set#Difference(a, b)[y] );

-

-function Set#Subset<T>(Set T, Set T): bool;

-axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }

-  Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));

-

-function Set#Equal<T>(Set T, Set T): bool;

-axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }

-  Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o]));

-axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }  // extensionality axiom for sets

-  Set#Equal(a,b) ==> a == b);

-

-function Set#Disjoint<T>(Set T, Set T): bool;

-axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }

-  Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));

-

-function Set#Choose<T>(Set T, TickType): T;

-axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }

-  a != Set#Empty() ==> a[Set#Choose(a, tick)]);

-

-

-// ---------------------------------------------------------------

-// -- Axiomatization of multisets --------------------------------

-// ---------------------------------------------------------------

-

-function Math#min(a: int, b: int): int;

-axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a);

-axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b);

-axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b);

-

-function Math#clip(a: int): int;

-axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a);

-axiom (forall a: int :: { Math#clip(a) } a < 0  ==> Math#clip(a) == 0);

-

-type MultiSet T = [T]int;

-

-function $IsGoodMultiSet<T>(ms: MultiSet T): bool;

-// ints are non-negative, used after havocing, and for conversion from sequences to multisets.

-axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) } 

-     $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o]));

-

-function MultiSet#Empty<T>(): MultiSet T;

-axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);

-

-function MultiSet#Singleton<T>(T): MultiSet T;

-axiom (forall<T> r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) &&

-                                                            (MultiSet#Singleton(r)[o] == 0 <==> r != o));

-axiom (forall<T> r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r));

-

-function MultiSet#UnionOne<T>(MultiSet T, T): MultiSet T;

-// pure containment axiom (in the original multiset or is the added element)

-axiom (forall<T> a: MultiSet T, x: T, o: T :: { MultiSet#UnionOne(a,x)[o] }

-  0 < MultiSet#UnionOne(a,x)[o] <==> o == x || 0 < a[o]);

-// union-ing increases count by one

-axiom (forall<T> a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) }

-  MultiSet#UnionOne(a, x)[x] == a[x] + 1);

-// non-decreasing

-axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }

-  0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]);

-// other elements unchanged

-axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }

-  x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);

-

-function MultiSet#Union<T>(MultiSet T, MultiSet T): MultiSet T;

-// union-ing is the sum of the contents

-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o] }

-  MultiSet#Union(a,b)[o] == a[o] + b[o]);

-

-// two containment axioms

-axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] }

-  0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]);

-axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] }

-  0 < b[y] ==> 0 < MultiSet#Union(a, b)[y]);

-

-// symmetry axiom

-axiom (forall<T> a, b: MultiSet T :: { MultiSet#Union(a, b) }

-  MultiSet#Difference(MultiSet#Union(a, b), a) == b &&

-  MultiSet#Difference(MultiSet#Union(a, b), b) == a);

-

-function MultiSet#Intersection<T>(MultiSet T, MultiSet T): MultiSet T;

-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] }

-  MultiSet#Intersection(a,b)[o] == Math#min(a[o],  b[o]));

-

-// left and right pseudo-idempotence

-axiom (forall<T> a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) }

-  MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b));

-axiom (forall<T> a, b: MultiSet T :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) }

-  MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b));

-

-// multiset difference, a - b. clip() makes it positive.

-function MultiSet#Difference<T>(MultiSet T, MultiSet T): MultiSet T;

-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Difference(a,b)[o] }

-  MultiSet#Difference(a,b)[o] == Math#clip(a[o] - b[o]));

-axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), b[y], a[y] }

-  a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0 );

-

-// multiset subset means a must have at most as many of each element as b

-function MultiSet#Subset<T>(MultiSet T, MultiSet T): bool;

-axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Subset(a,b) }

-  MultiSet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <= b[o]));

-

-function MultiSet#Equal<T>(MultiSet T, MultiSet T): bool;

-axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }

-  MultiSet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == b[o]));

-// extensionality axiom for multisets

-axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }

-  MultiSet#Equal(a,b) ==> a == b);

-

-function MultiSet#Disjoint<T>(MultiSet T, MultiSet T): bool;

-axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) }

-  MultiSet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == 0 || b[o] == 0));

-

-// conversion to a multiset. each element in the original set has duplicity 1.

-function MultiSet#FromSet<T>(Set T): MultiSet T;

-axiom (forall<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] }

-  (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) &&

-  (MultiSet#FromSet(s)[a] == 1 <==> s[a]));

-

-// conversion to a multiset, from a sequence.

-function MultiSet#FromSeq<T>(Seq T): MultiSet T;

-// conversion produces a good map.

-axiom (forall<T> s: Seq T :: { MultiSet#FromSeq(s) } $IsGoodMultiSet(MultiSet#FromSeq(s)) );

-// building axiom

-axiom (forall<T> s: Seq T, v: T ::

-  { MultiSet#FromSeq(Seq#Build(s, v)) }

-    MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v)

-  );

-axiom (forall<T> :: MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T);

-

-// concatenation axiom

-axiom (forall<T> a: Seq T, b: Seq T ::

-  { MultiSet#FromSeq(Seq#Append(a, b)) }

-    MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)) );

-

-// update axiom

-axiom (forall<T> s: Seq T, i: int, v: T, x: T ::

-  { MultiSet#FromSeq(Seq#Update(s, i, v))[x] }

-    0 <= i && i < Seq#Length(s) ==>

-    MultiSet#FromSeq(Seq#Update(s, i, v))[x] ==

-      MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s,i))), MultiSet#Singleton(v))[x] );

-  // i.e. MS(Update(s, i, v)) == MS(s) - {{s[i]}} + {{v}}

-axiom (forall<T> s: Seq T, x: T :: { MultiSet#FromSeq(s)[x] }

-  (exists i : int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && x == Seq#Index(s,i)) <==> 0 < MultiSet#FromSeq(s)[x] );

-  

-// ---------------------------------------------------------------

-// -- Axiomatization of sequences --------------------------------

-// ---------------------------------------------------------------

-

-type Seq T;

-

-function Seq#Length<T>(Seq T): int;

-axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));

-

-function Seq#Empty<T>(): Seq T;

-axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);

-axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());

-

-function Seq#Singleton<T>(T): Seq T;

-axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);

-

-function Seq#Build<T>(s: Seq T, val: T): Seq T;

-axiom (forall<T> s: Seq T, v: T :: { Seq#Length(Seq#Build(s,v)) }

-  Seq#Length(Seq#Build(s,v)) == 1 + Seq#Length(s));

-axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Index(Seq#Build(s,v), i) }

-  (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == v) &&

-  (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == Seq#Index(s, i)));

-

-function Seq#Append<T>(Seq T, Seq T): Seq T;

-axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }

-  Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));

-

-function Seq#Index<T>(Seq T, int): T;

-axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);

-axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }

-  (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&

-  (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0))));

-

-function Seq#Update<T>(Seq T, int, T): Seq T;

-axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) }

-  0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s));

-axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) }

-  0 <= n && n < Seq#Length(s) ==>

-    (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) &&

-    (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n)));

-

-function Seq#Contains<T>(Seq T, T): bool;

-axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }

-  Seq#Contains(s,x) <==>

-    (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));

-axiom (forall x: ref ::

-  { Seq#Contains(Seq#Empty(), x) }

-  !Seq#Contains(Seq#Empty(), x));

-axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::

-  { Seq#Contains(Seq#Append(s0, s1), x) }

-  Seq#Contains(Seq#Append(s0, s1), x) <==>

-    Seq#Contains(s0, x) || Seq#Contains(s1, x));

-

-axiom (forall<T> s: Seq T, v: T, x: T ::

-  { Seq#Contains(Seq#Build(s, v), x) }

-    Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x)));

-

-axiom (forall<T> s: Seq T, n: int, x: T ::

-  { Seq#Contains(Seq#Take(s, n), x) }

-  Seq#Contains(Seq#Take(s, n), x) <==>

-    (exists i: int :: { Seq#Index(s, i) }

-      0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x));

-axiom (forall<T> s: Seq T, n: int, x: T ::

-  { Seq#Contains(Seq#Drop(s, n), x) }

-  Seq#Contains(Seq#Drop(s, n), x) <==>

-    (exists i: int :: { Seq#Index(s, i) }

-      0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));

-

-function Seq#Equal<T>(Seq T, Seq T): bool;

-axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }

-  Seq#Equal(s0,s1) <==>

-    Seq#Length(s0) == Seq#Length(s1) &&

-    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }

-        0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));

-axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) }  // extensionality axiom for sequences

-  Seq#Equal(a,b) ==> a == b);

-

-function Seq#SameUntil<T>(Seq T, Seq T, int): bool;

-axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }

-  Seq#SameUntil(s0,s1,n) <==>

-    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }

-        0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));

-

-function Seq#Take<T>(s: Seq T, howMany: int): Seq T;

-axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }

-  0 <= n ==>

-    (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&

-    (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));

-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}

-  0 <= j && j < n && j < Seq#Length(s) ==>

-    Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));

-

-function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;

-axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }

-  0 <= n ==>

-    (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&

-    (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));

-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}

-  0 <= n && 0 <= j && j < Seq#Length(s)-n ==>

-    Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));

-

-axiom (forall<T> s, t: Seq T ::

-  { Seq#Append(s, t) }

-  Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&

-  Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);

-

-function Seq#FromArray(h: HeapType, a: ref): Seq BoxType;

-axiom (forall h: HeapType, a: ref ::

-  { Seq#Length(Seq#FromArray(h,a)) }

-    Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));

-axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType }

-   (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));

-axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::

-  { Seq#FromArray(update(h, o, f, v), a) }

-    o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) );

-axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::

-  { Seq#FromArray(update(h, a, IndexField(i), v), a) }

-    0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );

-/**** Someday:

-axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) }

-    $IsGoodHeap(h) &&

-    a != null && read(h, a, alloc) && dtype(a) == class._System.array && TypeParams(a, 0) == class._System.bool

-    ==>

-    (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) }

-      0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==>  $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i))));

-****/

-

-// Commutability of Take and Drop with Update.

-axiom (forall<T> s: Seq T, i: int, v: T, n: int ::

-  { Seq#Take(Seq#Update(s, i, v), n) }

-    0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );

-axiom (forall<T> s: Seq T, i: int, v: T, n: int ::

-  { Seq#Take(Seq#Update(s, i, v), n) }

-    n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));

-axiom (forall<T> s: Seq T, i: int, v: T, n: int ::

-  { Seq#Drop(Seq#Update(s, i, v), n) }

-    0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) );

-axiom (forall<T> s: Seq T, i: int, v: T, n: int ::

-  { Seq#Drop(Seq#Update(s, i, v), n) }

-    0 <= i && i < n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));

-// Extension axiom, triggers only on Takes from arrays.

-axiom (forall h: HeapType, a: ref, n0, n1: int ::

-  { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) }

-    n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) );

-// drop commutes with build.

-axiom (forall<T> s: Seq T, v: T, n: int ::

-  { Seq#Drop(Seq#Build(s, v), n) }

-    0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );

-

-// Additional axioms about common things

-axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty();  // [][..0] == []

-axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty();  // [][0..] == []

-

-// ---------------------------------------------------------------

-// -- Axiomatization of Maps -------------------------------------

-// ---------------------------------------------------------------

-

-type Map U V;

-

-function Map#Domain<U, V>(Map U V): [U] bool;

-function Map#Elements<U, V>(Map U V): [U]V;

-

-function Map#Empty<U, V>(): Map U V;

-axiom (forall<U, V> u: U ::

-  { Map#Domain(Map#Empty(): Map U V)[u] }

-   !Map#Domain(Map#Empty(): Map U V)[u]);

-

-function Map#Glue<U, V>([U] bool, [U]V): Map U V;

-axiom (forall<U, V> a: [U] bool, b:[U]V ::

-  { Map#Domain(Map#Glue(a, b)) }

-    Map#Domain(Map#Glue(a, b)) == a);

-axiom (forall<U, V> a: [U] bool, b:[U]V ::

-  { Map#Elements(Map#Glue(a, b)) }

-    Map#Elements(Map#Glue(a, b)) == b);

-

-

-//Build is used in displays, and for map updates

-function Map#Build<U, V>(Map U V, U, V): Map U V;

-/*axiom (forall<U, V> m: Map U V, u: U, v: V ::

-  { Map#Domain(Map#Build(m, u, v))[u] } { Map#Elements(Map#Build(m, u, v))[u] }

-  Map#Domain(Map#Build(m, u, v))[u] && Map#Elements(Map#Build(m, u, v))[u] == v);*/

-

-axiom (forall<U, V> m: Map U V, u: U, u': U, v: V ::

-  { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Elements(Map#Build(m, u, v))[u'] }

-  (u' == u ==> Map#Domain(Map#Build(m, u, v))[u'] &&

-               Map#Elements(Map#Build(m, u, v))[u'] == v) &&

-  (u' != u ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] &&

-               Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u']));

-

-//equality for maps

-function Map#Equal<U, V>(Map U V, Map U V): bool;

-axiom (forall<U, V> m: Map U V, m': Map U V::

-  { Map#Equal(m, m') }

-    Map#Equal(m, m') <==> (forall u : U :: Map#Domain(m)[u] == Map#Domain(m')[u]) &&

-                          (forall u : U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]));

-// extensionality

-axiom  (forall<U, V> m: Map U V, m': Map U V::

-  { Map#Equal(m, m') }

-    Map#Equal(m, m') ==> m == m');

-

-function Map#Disjoint<U, V>(Map U V, Map U V): bool;

-axiom (forall<U, V> m: Map U V, m': Map U V ::

-  { Map#Disjoint(m, m') }

-    Map#Disjoint(m, m') <==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o]));

-

-// ---------------------------------------------------------------

-// -- Boxing and unboxing ----------------------------------------

-// ---------------------------------------------------------------

-

-type BoxType;

-

-function $Box<T>(T): BoxType;

-function $Unbox<T>(BoxType): T;

-

-axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

-axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);

-axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);

-axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);

-axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);

-axiom (forall b: BoxType :: { $Unbox(b): Map BoxType BoxType } $Box($Unbox(b): Map BoxType BoxType) == b);

-axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b);

-// Note: an axiom like this for bool would not be sound; instead, we do:

-function $IsCanonicalBoolBox(BoxType): bool;

-axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));

-axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);

-

-// ---------------------------------------------------------------

-// -- Encoding of type names -------------------------------------

-// ---------------------------------------------------------------

-

-type ClassName;

-const unique class._System.int: ClassName;

-const unique class._System.bool: ClassName;

-const unique class._System.set: ClassName;

-const unique class._System.seq: ClassName;

-const unique class._System.multiset: ClassName;

-const unique class._System.array: ClassName;

-

-function /*{:never_pattern true}*/ dtype(ref): ClassName;

-function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;

-

-function TypeTuple(a: ClassName, b: ClassName): ClassName;

-function TypeTupleCar(ClassName): ClassName;

-function TypeTupleCdr(ClassName): ClassName;

-// TypeTuple is injective in both arguments:

-axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }

-  TypeTupleCar(TypeTuple(a,b)) == a &&

-  TypeTupleCdr(TypeTuple(a,b)) == b);

-

-// ---------------------------------------------------------------

-// -- Datatypes --------------------------------------------------

-// ---------------------------------------------------------------

-

-type DatatypeType;

-

-function /*{:never_pattern true}*/ DtType(DatatypeType): ClassName;  // the analog of dtype for datatype values

-function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName;  // the analog of TypeParams

-

-type DtCtorId;

-function DatatypeCtorId(DatatypeType): DtCtorId;

-

-function DtRank(DatatypeType): int;

-

-// ---------------------------------------------------------------

-// -- Axiom contexts ---------------------------------------------

-// ---------------------------------------------------------------

-

-// used to make sure function axioms are not used while their consistency is being checked

-const $ModuleContextHeight: int;

-const $FunctionContextHeight: int;

-const $InMethodContext: bool;

-

-// ---------------------------------------------------------------

-// -- Fields -----------------------------------------------------

-// ---------------------------------------------------------------

-

-type Field alpha;

-

-function FDim<T>(Field T): int;

-

-function IndexField(int): Field BoxType;

-axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);

-function IndexField_Inverse<T>(Field T): int;

-axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);

-

-function MultiIndexField(Field BoxType, int): Field BoxType;

-axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } FDim(MultiIndexField(f,i)) == FDim(f) + 1);

-function MultiIndexField_Inverse0<T>(Field T): Field T;

-function MultiIndexField_Inverse1<T>(Field T): int;

-axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }

-  MultiIndexField_Inverse0(MultiIndexField(f,i)) == f &&

-  MultiIndexField_Inverse1(MultiIndexField(f,i)) == i);

-

-

-function DeclType<T>(Field T): ClassName;

-

-type NameFamily;

-function DeclName<T>(Field T): NameFamily;

-function FieldOfDecl<alpha>(ClassName, NameFamily): Field alpha;

-axiom (forall<T> cl : ClassName, nm: NameFamily :: 

-   {FieldOfDecl(cl, nm): Field T}

-   DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm);

-

-// ---------------------------------------------------------------

-// -- Allocatedness ----------------------------------------------

-// ---------------------------------------------------------------

-

-const unique alloc: Field bool;

-axiom FDim(alloc) == 0;

-

-function DtAlloc(DatatypeType, HeapType): bool;

-axiom (forall h, k: HeapType, d: DatatypeType ::

-  { $HeapSucc(h, k), DtAlloc(d, h) }

-  { $HeapSucc(h, k), DtAlloc(d, k) }

-  $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k));

-

-function GenericAlloc(BoxType, HeapType): bool;

-axiom (forall h: HeapType, k: HeapType, d: BoxType ::

-  { $HeapSucc(h, k), GenericAlloc(d, h) }

-  { $HeapSucc(h, k), GenericAlloc(d, k) }

-  $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k));

-// GenericAlloc ==>

-axiom (forall b: BoxType, h: HeapType ::

-  { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] }

-  GenericAlloc(b, h) ==>

-  $Unbox(b): ref == null || h[$Unbox(b): ref, alloc]);

-//seqs

-axiom (forall b: BoxType, h: HeapType, i: int ::

-  { GenericAlloc(b, h), Seq#Index($Unbox(b): Seq BoxType, i) }

-  GenericAlloc(b, h) &&

-  0 <= i && i < Seq#Length($Unbox(b): Seq BoxType) ==>

-  GenericAlloc( Seq#Index($Unbox(b): Seq BoxType, i), h ) );

-

-//maps

-//seq-like axiom, talking about the range elements

-axiom (forall b: BoxType, h: HeapType, i: BoxType ::

-  { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[i] }

-  GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[i] ==>

-  GenericAlloc( Map#Elements($Unbox(b): Map BoxType BoxType)[i], h ) );

-//set-like axiom, talking about the domain elements

-axiom (forall b: BoxType, h: HeapType, t: BoxType ::

-  { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[t] }

-  GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[t] ==>

-  GenericAlloc(t, h));

-

-//sets

-axiom (forall b: BoxType, h: HeapType, t: BoxType ::

-  { GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] }

-  GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==>

-  GenericAlloc(t, h));

-axiom (forall b: BoxType, h: HeapType ::

-  { GenericAlloc(b, h), DtType($Unbox(b): DatatypeType) }

-  GenericAlloc(b, h) ==> DtAlloc($Unbox(b): DatatypeType, h));

-// ==> GenericAlloc

-axiom (forall b: bool, h: HeapType ::

-  $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));

-axiom (forall x: int, h: HeapType ::

-  $IsGoodHeap(h) ==> GenericAlloc($Box(x), h));

-axiom (forall r: ref, h: HeapType ::

-  { GenericAlloc($Box(r), h) }

-  $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));

-// boxes in the heap

-axiom (forall r: ref, f: Field BoxType, h: HeapType ::

-  { GenericAlloc(read(h, r, f), h) }

-  $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>

-  GenericAlloc(read(h, r, f), h));

-

-// ---------------------------------------------------------------

-// -- Arrays -----------------------------------------------------

-// ---------------------------------------------------------------

-

-function _System.array.Length(a: ref): int;

-axiom (forall o: ref :: 0 <= _System.array.Length(o));

-

-// ---------------------------------------------------------------

-// -- The heap ---------------------------------------------------

-// ---------------------------------------------------------------

-

-type HeapType = <alpha>[ref,Field alpha]alpha;

-function {:inline true} read<alpha>(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] }

-function {:inline true} update<alpha>(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] }

-

-function $IsGoodHeap(HeapType): bool;

-var $Heap: HeapType where $IsGoodHeap($Heap);

-

-function $HeapSucc(HeapType, HeapType): bool;

-axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }

-  $IsGoodHeap(update(h, r, f, x)) ==>

-  $HeapSucc(h, update(h, r, f, x)));

-axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }

-  $HeapSucc(a,b) && $HeapSucc(b,c) ==> $HeapSucc(a,c));

-axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }

-  $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));

-

-// ---------------------------------------------------------------

-// -- Useful macros ----------------------------------------------

-// ---------------------------------------------------------------

-

-// havoc everything in $Heap, except {this}+rds+nw

-procedure $YieldHavoc(this: ref, rds: Set BoxType, nw: Set BoxType);

-  modifies $Heap;

-  ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }

-            $o != null && read(old($Heap), $o, alloc) ==>

-            $o == this || rds[$Box($o)] || nw[$Box($o)] ==>

-              read($Heap, $o, $f) == read(old($Heap), $o, $f));

-  ensures $HeapSucc(old($Heap), $Heap);

-

-// havoc everything in $Heap, except rds-modi-{this}

-procedure $IterHavoc0(this: ref, rds: Set BoxType, modi: Set BoxType);

-  modifies $Heap;

-  ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }

-            $o != null && read(old($Heap), $o, alloc) ==>

-            rds[$Box($o)] && !modi[$Box($o)] && $o != this ==>

-              read($Heap, $o, $f) == read(old($Heap), $o, $f));

-  ensures $HeapSucc(old($Heap), $Heap);

-

-// havoc $Heap at {this}+modi+nw

-procedure $IterHavoc1(this: ref, modi: Set BoxType, nw: Set BoxType);

-  modifies $Heap;

-  ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }

-            $o != null && read(old($Heap), $o, alloc) ==>

-              read($Heap, $o, $f) == read(old($Heap), $o, $f) ||

-              $o == this || modi[$Box($o)] || nw[$Box($o)]);

-  ensures $HeapSucc(old($Heap), $Heap);

-

-procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType))

-                        returns (s: Set BoxType);

-  ensures (forall bx: BoxType :: { s[bx] } s[bx] <==>

-              read(newHeap, this, NW)[bx] ||

-              ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc)));

-

-// ---------------------------------------------------------------

-// -- Non-determinism --------------------------------------------

-// ---------------------------------------------------------------

-

-type TickType;

-var $Tick: TickType;

-

-// ---------------------------------------------------------------

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
deleted file mode 100644
index ac688143..00000000
--- a/Binaries/DafnyRuntime.cs
+++ /dev/null
@@ -1,574 +0,0 @@
-using System.Numerics;

-

-namespace Dafny

-{

-  using System.Collections.Generic;

-

-  public class Set<T>

-  {

-    Dictionary<T, bool> dict;

-    public Set() { }

-    Set(Dictionary<T, bool> d) {

-      dict = d;

-    }

-    public static Set<T> Empty {

-      get {

-        return new Set<T>(new Dictionary<T, bool>(0));

-      }

-    }

-    public static Set<T> FromElements(params T[] values) {

-      Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);

-      foreach (T t in values)

-        d[t] = true;

-      return new Set<T>(d);

-    }

-    public static Set<T> FromCollection(ICollection<T> values) {

-      Dictionary<T, bool> d = new Dictionary<T, bool>();

-      foreach (T t in values)

-        d[t] = true;

-      return new Set<T>(d);

-    }

-    

-    public IEnumerable<T> Elements {

-      get {

-        return dict.Keys;

-      }

-    }

-    public bool Equals(Set<T> other) {

-      return dict.Count == other.dict.Count && IsSubsetOf(other);

-    }

-    public override bool Equals(object other) {

-      return other is Set<T> && Equals((Set<T>)other);

-    }

-    public override int GetHashCode() {

-      return dict.GetHashCode();

-    }

-    public bool IsProperSubsetOf(Set<T> other) {

-      return dict.Count < other.dict.Count && IsSubsetOf(other);

-    }

-    public bool IsSubsetOf(Set<T> other) {

-      if (other.dict.Count < dict.Count)

-        return false;

-      foreach (T t in dict.Keys) {

-        if (!other.dict.ContainsKey(t))

-          return false;

-      }

-      return true;

-    }

-    public bool IsSupersetOf(Set<T> other) {

-      return other.IsSubsetOf(this);

-    }

-    public bool IsProperSupersetOf(Set<T> other) {

-      return other.IsProperSubsetOf(this);

-    }

-    public bool IsDisjointFrom(Set<T> other) {

-      Dictionary<T, bool> a, b;

-      if (dict.Count < other.dict.Count) {

-        a = dict; b = other.dict;

-      } else {

-        a = other.dict; b = dict;

-      }

-      foreach (T t in a.Keys) {

-        if (b.ContainsKey(t))

-          return false;

-      }

-      return true;

-    }

-    public bool Contains(T t) {

-      return dict.ContainsKey(t);

-    }

-    public Set<T> Union(Set<T> other) {

-      if (dict.Count == 0)

-        return other;

-      else if (other.dict.Count == 0)

-        return this;

-      Dictionary<T, bool> a, b;

-      if (dict.Count < other.dict.Count) {

-        a = dict; b = other.dict;

-      } else {

-        a = other.dict; b = dict;

-      }

-      Dictionary<T, bool> r = new Dictionary<T, bool>();

-      foreach (T t in b.Keys)

-        r[t] = true;

-      foreach (T t in a.Keys)

-        r[t] = true;

-      return new Set<T>(r);

-    }

-    public Set<T> Intersect(Set<T> other) {

-      if (dict.Count == 0)

-        return this;

-      else if (other.dict.Count == 0)

-        return other;

-      Dictionary<T, bool> a, b;

-      if (dict.Count < other.dict.Count) {

-        a = dict; b = other.dict;

-      } else {

-        a = other.dict; b = dict;

-      }

-      var r = new Dictionary<T, bool>();

-      foreach (T t in a.Keys) {

-        if (b.ContainsKey(t))

-          r.Add(t, true);

-      }

-      return new Set<T>(r);

-    }

-    public Set<T> Difference(Set<T> other) {

-      if (dict.Count == 0)

-        return this;

-      else if (other.dict.Count == 0)

-        return this;

-      var r = new Dictionary<T, bool>();

-      foreach (T t in dict.Keys) {

-        if (!other.dict.ContainsKey(t))

-          r.Add(t, true);

-      }

-      return new Set<T>(r);

-    }

-    public T Choose() {

-      foreach (T t in dict.Keys) {

-        // return the first one

-        return t;

-      }

-      return default(T);

-    }

-  }

-  public class MultiSet<T>

-  {

-    Dictionary<T, int> dict;

-    public MultiSet() { }

-    MultiSet(Dictionary<T, int> d) {

-      dict = d;

-    }

-    public static MultiSet<T> Empty {

-      get {

-        return new MultiSet<T>(new Dictionary<T, int>(0));

-      }

-    }

-    public static MultiSet<T> FromElements(params T[] values) {

-      Dictionary<T, int> d = new Dictionary<T, int>(values.Length);

-      foreach (T t in values) {

-        var i = 0;

-        if (!d.TryGetValue(t, out i)) {

-          i = 0;

-        }

-        d[t] = i + 1;

-      }

-      return new MultiSet<T>(d);

-    }

-    public static MultiSet<T> FromCollection(ICollection<T> values) {

-      Dictionary<T, int> d = new Dictionary<T, int>();

-      foreach (T t in values) {

-        var i = 0;

-        if (!d.TryGetValue(t, out i)) {

-          i = 0;

-        }

-        d[t] = i + 1;

-      }

-      return new MultiSet<T>(d);

-    }

-    public static MultiSet<T> FromSeq(Sequence<T> values) {

-      Dictionary<T, int> d = new Dictionary<T, int>();

-      foreach (T t in values.Elements) {

-        var i = 0;

-        if (!d.TryGetValue(t, out i)) {

-          i = 0;

-        }

-        d[t] = i + 1;

-      }

-      return new MultiSet<T>(d);

-    }

-    public static MultiSet<T> FromSet(Set<T> values) {

-      Dictionary<T, int> d = new Dictionary<T, int>();

-      foreach (T t in values.Elements) {

-        d[t] = 1;

-      }

-      return new MultiSet<T>(d);

-    }

-

-    public bool Equals(MultiSet<T> other) {

-      return other.IsSubsetOf(this) && this.IsSubsetOf(other);

-    }

-    public override bool Equals(object other) {

-      return other is MultiSet<T> && Equals((MultiSet<T>)other);

-    }

-    public override int GetHashCode() {

-      return dict.GetHashCode();

-    }

-    public bool IsProperSubsetOf(MultiSet<T> other) {

-      return !Equals(other) && IsSubsetOf(other);

-    }

-    public bool IsSubsetOf(MultiSet<T> other) {

-      foreach (T t in dict.Keys) {

-        if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])

-          return false;

-      }

-      return true;

-    }

-    public bool IsSupersetOf(MultiSet<T> other) {

-      return other.IsSubsetOf(this);

-    }

-    public bool IsProperSupersetOf(MultiSet<T> other) {

-      return other.IsProperSubsetOf(this);

-    }

-    public bool IsDisjointFrom(MultiSet<T> other) {

-      foreach (T t in dict.Keys) {

-        if (other.dict.ContainsKey(t))

-          return false;

-      }

-      foreach (T t in other.dict.Keys) {

-        if (dict.ContainsKey(t))

-          return false;

-      }

-      return true;

-    }

-    public bool Contains(T t) {

-      return dict.ContainsKey(t);

-    }

-    public MultiSet<T> Union(MultiSet<T> other) {

-      if (dict.Count == 0)

-        return other;

-      else if (other.dict.Count == 0)

-        return this;

-      var r = new Dictionary<T, int>();

-      foreach (T t in dict.Keys) {

-        var i = 0;

-        if (!r.TryGetValue(t, out i)) {

-          i = 0;

-        }

-        r[t] = i + dict[t];

-      }

-      foreach (T t in other.dict.Keys) {

-        var i = 0;

-        if (!r.TryGetValue(t, out i)) {

-          i = 0;

-        }

-        r[t] = i + other.dict[t];

-      }

-      return new MultiSet<T>(r);

-    }

-    public MultiSet<T> Intersect(MultiSet<T> other) {

-      if (dict.Count == 0)

-        return this;

-      else if (other.dict.Count == 0)

-        return other;

-      var r = new Dictionary<T, int>();

-      foreach (T t in dict.Keys) {

-        if (other.dict.ContainsKey(t)) {

-          r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);

-        }

-      }

-      return new MultiSet<T>(r);

-    }

-    public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other

-      if (dict.Count == 0)

-        return this;

-      else if (other.dict.Count == 0)

-        return this;

-      var r = new Dictionary<T, int>();

-      foreach (T t in dict.Keys) {

-        if (!other.dict.ContainsKey(t)) {

-          r.Add(t, dict[t]);

-        } else if (other.dict[t] < dict[t]) {

-          r.Add(t, dict[t] - other.dict[t]);

-        }

-      }

-      return new MultiSet<T>(r);

-    }

-    public IEnumerable<T> Elements {

-      get {

-        List<T> l = new List<T>();

-        foreach (T t in dict.Keys) {

-          int n;

-          dict.TryGetValue(t, out n);

-          for (int i = 0; i < n; i ++) {

-            l.Add(t);

-          }

-        }

-        return l;

-      }

-    }

-  }

-

-  public class Map<U, V>

-  {

-    Dictionary<U, V> dict;

-    public Map() { }

-    Map(Dictionary<U, V> d) {

-      dict = d;

-    }

-    public static Map<U, V> Empty {

-      get {

-        return new Map<U, V>(new Dictionary<U,V>());

-      }

-    }

-    public static Map<U, V> FromElements(params Pair<U, V>[] values) {

-      Dictionary<U, V> d = new Dictionary<U, V>(values.Length);

-      foreach (Pair<U, V> p in values) {

-        d[p.Car] = p.Cdr;

-      }

-      return new Map<U, V>(d);

-    }

-    public static Map<U, V> FromCollection(List<Pair<U, V>> values) {

-      Dictionary<U, V> d = new Dictionary<U, V>(values.Count);

-      foreach (Pair<U, V> p in values) {

-        d[p.Car] = p.Cdr;

-      }

-      return new Map<U, V>(d);

-    }

-    public bool Equals(Map<U, V> other) {

-      foreach (U u in dict.Keys) {

-        V v1, v2;

-        if (!dict.TryGetValue(u, out v1)) {

-          return false; // this shouldn't happen

-        }

-        if (!other.dict.TryGetValue(u, out v2)) {

-          return false; // other dictionary does not contain this element

-        }

-        if (!v1.Equals(v2)) {

-          return false;

-        }

-      }

-      foreach (U u in other.dict.Keys) {

-        if (!dict.ContainsKey(u)) {

-          return false; // this shouldn't happen

-        }

-      }

-      return true;

-    }

-    public override bool Equals(object other) {

-      return other is Map<U, V> && Equals((Map<U, V>)other);

-    }

-    public override int GetHashCode() {

-      return dict.GetHashCode();

-    }

-    public bool IsDisjointFrom(Map<U, V> other) {

-      foreach (U u in dict.Keys) {

-        if (other.dict.ContainsKey(u))

-          return false;

-      }

-      foreach (U u in other.dict.Keys) {

-        if (dict.ContainsKey(u))

-          return false;

-      }

-      return true;

-    }

-    public bool Contains(U u) {

-      return dict.ContainsKey(u);

-    }

-    public V Select(U index) {

-      return dict[index];

-    }

-    public Map<U, V> Update(U index, V val) {

-      Dictionary<U, V> d = new Dictionary<U, V>(dict);

-      d[index] = val;

-      return new Map<U, V>(d);

-    }

-    public IEnumerable<U> Domain {

-      get {

-        return dict.Keys;

-      }

-    }

-  }

-  public class Sequence<T>

-  {

-    T[] elmts;

-    public Sequence() { }

-    public Sequence(T[] ee) {

-      elmts = ee;

-    }

-    public static Sequence<T> Empty {

-      get {

-        return new Sequence<T>(new T[0]);

-      }

-    }

-    public static Sequence<T> FromElements(params T[] values) {

-      return new Sequence<T>(values);

-    }

-    public BigInteger Length {

-      get { return new BigInteger(elmts.Length); }

-    }

-    public T[] Elements {

-      get {

-        return elmts;

-      }

-    }

-    public IEnumerable<T> UniqueElements {

-      get {

-        var st = Set<T>.FromElements(elmts);

-        return st.Elements;

-      }

-    }

-    public T Select(BigInteger index) {

-      return elmts[(int)index];

-    }

-    public Sequence<T> Update(BigInteger index, T t) {

-      T[] a = (T[])elmts.Clone();

-      a[(int)index] = t;

-      return new Sequence<T>(a);

-    }

-    public bool Equals(Sequence<T> other) {

-      int n = elmts.Length;

-      return n == other.elmts.Length && EqualUntil(other, n);

-    }

-    public override bool Equals(object other) {

-      return other is Sequence<T> && Equals((Sequence<T>)other);

-    }

-    public override int GetHashCode() {

-      return elmts.GetHashCode();

-    }

-    bool EqualUntil(Sequence<T> other, int n) {

-      for (int i = 0; i < n; i++) {

-        if (!elmts[i].Equals(other.elmts[i]))

-          return false;

-      }

-      return true;

-    }

-    public bool IsProperPrefixOf(Sequence<T> other) {

-      int n = elmts.Length;

-      return n < other.elmts.Length && EqualUntil(other, n);

-    }

-    public bool IsPrefixOf(Sequence<T> other) {

-      int n = elmts.Length;

-      return n <= other.elmts.Length && EqualUntil(other, n);

-    }

-    public Sequence<T> Concat(Sequence<T> other) {

-      if (elmts.Length == 0)

-        return other;

-      else if (other.elmts.Length == 0)

-        return this;

-      T[] a = new T[elmts.Length + other.elmts.Length];

-      System.Array.Copy(elmts, 0, a, 0, elmts.Length);

-      System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);

-      return new Sequence<T>(a);

-    }

-    public bool Contains(T t) {

-      int n = elmts.Length;

-      for (int i = 0; i < n; i++) {

-        if (t.Equals(elmts[i]))

-          return true;

-      }

-      return false;

-    }

-    public Sequence<T> Take(BigInteger n) {

-      int m = (int)n;

-      if (elmts.Length == m)

-        return this;

-      T[] a = new T[m];

-      System.Array.Copy(elmts, a, m);

-      return new Sequence<T>(a);

-    }

-    public Sequence<T> Drop(BigInteger n) {

-      if (n.IsZero)

-        return this;

-      int m = (int)n;

-      T[] a = new T[elmts.Length - m];

-      System.Array.Copy(elmts, m, a, 0, elmts.Length - m);

-      return new Sequence<T>(a);

-    }

-  }

-  public struct Pair<A, B>

-  {

-    public readonly A Car;

-    public readonly B Cdr;

-    public Pair(A a, B b) {

-      this.Car = a;

-      this.Cdr = b;

-    }

-  }

-  public partial class Helpers {

-    // Computing forall/exists quantifiers

-    public static bool QuantBool(bool frall, System.Predicate<bool> pred) {

-      if (frall) {

-        return pred(false) && pred(true);

-      } else {

-        return pred(false) || pred(true);

-      }

-    }

-    public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {

-      for (BigInteger i = lo; i < hi; i++) {

-        if (pred(i) != frall) { return !frall; }

-      }

-      return frall;

-    }

-    public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {

-      foreach (var u in set.Elements) {

-        if (pred(u) != frall) { return !frall; }

-      }

-      return frall;

-    }

-    public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {

-      foreach (var u in map.Domain) {

-        if (pred(u) != frall) { return !frall; }

-      }

-      return frall;

-    }

-    public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {

-      foreach (var u in seq.Elements) {

-        if (pred(u) != frall) { return !frall; }

-      }

-      return frall;

-    }

-    public static bool QuantDatatype<U>(IEnumerable<U> set, bool frall, System.Predicate<U> pred) {

-      foreach (var u in set) {

-        if (pred(u) != frall) { return !frall; }

-      }

-      return frall;

-    }

-    // Enumerating other collections

-    public delegate Dafny.Set<T> ComprehensionDelegate<T>();

-    public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();

-    public static IEnumerable<bool> AllBooleans {

-      get {

-        yield return false;

-        yield return true;

-      }

-    }

-    // pre: b != 0

-    // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)

-    public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {

-      if (0 <= a.Sign) {

-        if (0 <= b.Sign) {

-          // +a +b: a/b

-          return BigInteger.Divide(a, b);

-        } else {

-          // +a -b: -(a/(-b))

-          return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));

-        }

-      } else {

-        if (0 <= b.Sign) {

-          // -a +b: -((-a-1)/b) - 1

-          return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;

-        } else {

-          // -a -b: ((-a-1)/(-b)) + 1

-          return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;

-        }

-      }

-    }

-    // pre: b != 0

-    // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)

-    public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {

-      var bp = BigInteger.Abs(b);

-      if (0 <= a.Sign) {

-        // +a: a % b'

-        return BigInteger.Remainder(a, bp);

-      } else {

-        // c = ((-a) % b')

-        // -a: b' - c if c > 0

-        // -a: 0 if c == 0

-        var c = BigInteger.Remainder(BigInteger.Negate(a), bp);

-        return c.IsZero ? c : BigInteger.Subtract(bp, c);

-      }

-    }

-    public static Sequence<T> SeqFromArray<T>(T[] array) {

-      return new Sequence<T>(array);

-    }

-    // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the

-    // method if possible.  Method "ExpressionSequence" would be a good candidate for it:

-    // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]

-    public static U ExpressionSequence<T, U>(T t, U u)

-    {

-      return u;

-    }

-  }

-}