Merge

1 files changed, 1324 insertions, 1324 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 4dda19fe..3002d832 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -1,1324 +1,1324 @@
-using System; // for Func

-using System.Numerics;

-

-namespace Dafny

-{

-  using System.Collections.Generic;

-// set this option if you want to use System.Collections.Immutable and if you know what you're doing.

-#if DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE

-  using System.Collections.Immutable;

-  using System.Linq;

-

-  public class Set<T>

-  {

-    readonly ImmutableHashSet<T> setImpl;

-    Set(ImmutableHashSet<T> d) {

-      this.setImpl = d;

-    }

-    public static readonly Set<T> Empty = new Set<T>(ImmutableHashSet<T>.Empty);

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

-      return FromElements((IEnumerable<T>)values);

-    }

-    public static Set<T> FromElements(IEnumerable<T> values) {

-      var d = ImmutableHashSet<T>.Empty.ToBuilder();

-      foreach (T t in values)

-        d.Add(t);

-      return new Set<T>(d.ToImmutable());

-    }

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

-      var d = ImmutableHashSet<T>.Empty.ToBuilder();

-      foreach (T t in values)

-        d.Add(t);

-      return new Set<T>(d.ToImmutable());

-    }

-    public int Length {

-      get { return this.setImpl.Count; }

-    }

-    public long LongLength {

-      get { return this.setImpl.Count; }

-    }

-    public IEnumerable<T> Elements {

-      get {

-        return this.setImpl;

-      }

-    }

-    /// <summary>

-    /// This is an inefficient iterator for producing all subsets of "this".  Each set returned is the same

-    /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").

-    /// </summary>

-    public IEnumerable<Set<T>> AllSubsets {

-      get {

-        // Start by putting all set elements into a list

-        var elmts = new List<T>();

-        elmts.AddRange(this.setImpl);

-        var n = elmts.Count;

-        var which = new bool[n];

-        var s = ImmutableHashSet<T>.Empty.ToBuilder();

-        while (true) {

-          yield return new Set<T>(s.ToImmutable());

-          // "add 1" to "which", as if doing a carry chain.  For every digit changed, change the membership of the corresponding element in "s".

-          int i = 0;

-          for (; i < n && which[i]; i++) {

-            which[i] = false;

-            s.Remove(elmts[i]);

-          }

-          if (i == n) {

-            // we have cycled through all the subsets

-            break;

-          }

-          which[i] = true;

-          s.Add(elmts[i]);

-        }

-      }

-    }

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

-        return this.setImpl.SetEquals(other.setImpl);

-    }

-    public override bool Equals(object other) {

-        var otherSet = other as Set<T>;

-        return otherSet != null && this.Equals(otherSet);

-    }

-    public override int GetHashCode() {

-      var hashCode = 1;

-      foreach (var t in this.setImpl) {

-        hashCode = hashCode * (t.GetHashCode()+3);

-      }

-      return hashCode;

-    }

-    public override string ToString() {

-      var s = "{";

-      var sep = "";

-      foreach (var t in this.setImpl) {

-        s += sep + t.ToString();

-        sep = ", ";

-      }

-      return s + "}";

-    }

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

-        return IsProperSubsetOf(other);

-    }

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

-        return IsSubsetOf(other);

-    }

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

-      return other.IsSupersetOf(this);

-    }

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

-      return other.IsProperSupersetOf(this);

-    }

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

-      ImmutableHashSet<T> a, b;

-      if (this.setImpl.Count < other.setImpl.Count) {

-        a = this.setImpl; b = other.setImpl;

-      } else {

-        a = other.setImpl; b = this.setImpl;

-      }

-      foreach (T t in a) {

-        if (b.Contains(t))

-          return false;

-      }

-      return true;

-    }

-    public bool Contains(T t) {

-      return this.setImpl.Contains(t);

-    }

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

-        return new Set<T>(this.setImpl.Union(other.setImpl));

-    }

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

-      return new Set<T>(this.setImpl.Intersect(other.setImpl));

-    }

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

-        return new Set<T>(this.setImpl.Except(other.setImpl));

-    }

-  }

-  public partial class MultiSet<T>

-  {

-

-    readonly ImmutableDictionary<T, int> dict;

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

-      dict = d;

-    }

-    public static readonly MultiSet<T> Empty = new MultiSet<T>(ImmutableDictionary<T, int>.Empty);

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

-      var d = ImmutableDictionary<T, int>.Empty.ToBuilder();

-      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.ToImmutable());

-    }

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

-      var d = ImmutableDictionary<T, int>.Empty.ToBuilder();

-      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.ToImmutable());

-    }

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

-      var d = ImmutableDictionary<T, int>.Empty.ToBuilder();

-      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.ToImmutable());

-    }

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

-      var d = ImmutableDictionary<T, int>.Empty.ToBuilder();

-      foreach (T t in values.Elements) {

-        d[t] = 1;

-      }

-      return new MultiSet<T>(d.ToImmutable());

-    }

-

-    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() {

-      var hashCode = 1;

-      foreach (var kv in dict) {

-        var key = kv.Key.GetHashCode();

-        key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();

-        hashCode = hashCode * (key + 3);

-      }

-      return hashCode;

-    }

-    public override string ToString() {

-      var s = "multiset{";

-      var sep = "";

-      foreach (var kv in dict) {

-        var t = kv.Key.ToString();

-        for (int i = 0; i < kv.Value; i++) {

-          s += sep + t.ToString();

-          sep = ", ";

-        }

-      }

-      return s + "}";

-    }

-    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 = ImmutableDictionary<T, int>.Empty.ToBuilder();

-      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.ToImmutable());

-    }

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

-      if (dict.Count == 0)

-        return this;

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

-        return other;

-      var r = ImmutableDictionary<T, int>.Empty.ToBuilder();

-      foreach (T t in dict.Keys) {

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

-          r[t] = other.dict[t] < dict[t] ? other.dict[t] : dict[t];

-        }

-      }

-      return new MultiSet<T>(r.ToImmutable());

-    }

-    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 = ImmutableDictionary<T, int>.Empty.ToBuilder();

-      foreach (T t in dict.Keys) {

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

-          r[t] = dict[t];

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

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

-        }

-      }

-      return new MultiSet<T>(r.ToImmutable());

-    }

-    public IEnumerable<T> Elements {

-      get {

-        foreach (T t in dict.Keys) {

-          int n;

-          dict.TryGetValue(t, out n);

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

-            yield return t;

-          }

-        }

-      }

-    }

-  }

-

-  public partial class Map<U, V>

-  {

-    readonly ImmutableDictionary<U, V> dict;

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

-      dict = d;

-    }

-    public static readonly Map<U, V> Empty = new Map<U, V>(ImmutableDictionary<U, V>.Empty);

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

-      var d = ImmutableDictionary<U, V>.Empty.ToBuilder();

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

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

-      }

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

-    }

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

-      var d = ImmutableDictionary<U, V>.Empty.ToBuilder();

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

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

-      }

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

-    }

-    public int Length {

-      get { return dict.Count; }

-    }

-    public long LongLength {

-      get { return dict.Count; }

-    }

-    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() {

-      var hashCode = 1;

-      foreach (var kv in dict) {

-        var key = kv.Key.GetHashCode();

-        key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();

-        hashCode = hashCode * (key + 3);

-      }

-      return hashCode;

-    }

-    public override string ToString() {

-      var s = "map[";

-      var sep = "";

-      foreach (var kv in dict) {

-        s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();

-        sep = ", ";

-      }

-      return s + "]";

-    }

-    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) {

-      return new Map<U, V>(dict.SetItem(index, val));

-    }

-    public IEnumerable<U> Domain {

-      get {

-        return dict.Keys;

-      }

-    }

-  }

-#else // !def DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE

-  public class Set<T>

-  {

-    HashSet<T> set;

-    Set(HashSet<T> s) {

-      this.set = s;

-    }

-    public static Set<T> Empty {

-      get {

-        return new Set<T>(new HashSet<T>());

-      }

-    }

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

-      var s = new HashSet<T>();

-      foreach (T t in values)

-        s.Add(t);

-      return new Set<T>(s);

-    }

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

-      HashSet<T> s = new HashSet<T>();

-      foreach (T t in values)

-        s.Add(t);

-      return new Set<T>(s);

-    }

-    public int Length {

-      get { return this.set.Count; }

-    }

-    public long LongLength {

-      get { return this.set.Count; }

-    }

-    public IEnumerable<T> Elements {

-      get {

-        return this.set;

-      }

-    }

-    /// <summary>

-    /// This is an inefficient iterator for producing all subsets of "this".  Each set returned is the same

-    /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").

-    /// </summary>

-    public IEnumerable<Set<T>> AllSubsets {

-      get {

-        // Start by putting all set elements into a list

-        var elmts = new List<T>();

-        elmts.AddRange(this.set);

-        var n = elmts.Count;

-        var which = new bool[n];

-        var s = new Set<T>(new HashSet<T>());

-        while (true) {

-          yield return s;

-          // "add 1" to "which", as if doing a carry chain.  For every digit changed, change the membership of the corresponding element in "s".

-          int i = 0;

-          for (; i < n && which[i]; i++) {

-            which[i] = false;

-            s.set.Remove(elmts[i]);

-          }

-          if (i == n) {

-            // we have cycled through all the subsets

-            break;

-          }

-          which[i] = true;

-          s.set.Add(elmts[i]);

-        }

-      }

-    }

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

-      return this.set.Count == other.set.Count && IsSubsetOf(other);

-    }

-    public override bool Equals(object other) {

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

-    }

-    public override int GetHashCode() {

-      var hashCode = 1;

-      foreach (var t in this.set) {

-        hashCode = hashCode * (t.GetHashCode()+3);

-      }

-      return hashCode;

-    }

-    public override string ToString() {

-      var s = "{";

-      var sep = "";

-      foreach (var t in this.set) {

-        s += sep + t.ToString();

-        sep = ", ";

-      }

-      return s + "}";

-    }

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

-      return this.set.Count < other.set.Count && IsSubsetOf(other);

-    }

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

-      if (other.set.Count < this.set.Count)

-        return false;

-      foreach (T t in this.set) {

-        if (!other.set.Contains(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) {

-      HashSet<T> a, b;

-      if (this.set.Count < other.set.Count) {

-        a = this.set; b = other.set;

-      } else {

-        a = other.set; b = this.set;

-      }

-      foreach (T t in a) {

-        if (b.Contains(t))

-          return false;

-      }

-      return true;

-    }

-    public bool Contains(T t) {

-      return this.set.Contains(t);

-    }

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

-      if (this.set.Count == 0)

-        return other;

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

-        return this;

-      HashSet<T> a, b;

-      if (this.set.Count < other.set.Count) {

-        a = this.set; b = other.set;

-      } else {

-        a = other.set; b = this.set;

-      }

-      var r = new HashSet<T>();

-      foreach (T t in b)

-        r.Add(t);

-      foreach (T t in a)

-        r.Add(t);

-      return new Set<T>(r);

-    }

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

-      if (this.set.Count == 0)

-        return this;

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

-        return other;

-      HashSet<T> a, b;

-      if (this.set.Count < other.set.Count) {

-        a = this.set; b = other.set;

-      } else {

-        a = other.set; b = this.set;

-      }

-      var r = new HashSet<T>();

-      foreach (T t in a) {

-        if (b.Contains(t))

-          r.Add(t);

-      }

-      return new Set<T>(r);

-    }

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

-      if (this.set.Count == 0)

-        return this;

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

-        return this;

-      var r = new HashSet<T>();

-      foreach (T t in this.set) {

-        if (!other.set.Contains(t))

-          r.Add(t);

-      }

-      return new Set<T>(r);

-    }

-  }

-  public class MultiSet<T>

-  {

-    Dictionary<T, int> dict;

-    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() {

-      var hashCode = 1;

-      foreach (var kv in dict) {

-        var key = kv.Key.GetHashCode();

-        key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();

-        hashCode = hashCode * (key + 3);

-      }

-      return hashCode;

-    }

-    public override string ToString() {

-      var s = "multiset{";

-      var sep = "";

-      foreach (var kv in dict) {

-        var t = kv.Key.ToString();

-        for (int i = 0; i < kv.Value; i++) {

-          s += sep + t.ToString();

-          sep = ", ";

-        }

-      }

-      return s + "}";

-    }

-    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;

-    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 int Length {

-      get { return dict.Count; }

-    }

-    public long LongLength {

-      get { return dict.Count; }

-    }

-    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() {

-      var hashCode = 1;

-      foreach (var kv in dict) {

-        var key = kv.Key.GetHashCode();

-        key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();

-        hashCode = hashCode * (key + 3);

-      }

-      return hashCode;

-    }

-    public override string ToString() {

-      var s = "map[";

-      var sep = "";

-      foreach (var kv in dict) {

-        s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();

-        sep = ", ";

-      }

-      return s + "]";

-    }

-    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;

-      }

-    }

-  }

-#endif

-  public class Sequence<T>

-  {

-    T[] elmts;

-    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 static Sequence<char> FromString(string s) {

-      return new Sequence<char>(s.ToCharArray());

-    }

-    public int Length {

-      get { return elmts.Length; }

-    }

-    public long LongLength {

-      get { return elmts.LongLength; }

-    }

-    public T[] Elements {

-      get {

-        return elmts;

-      }

-    }

-    public IEnumerable<T> UniqueElements {

-      get {

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

-        return st.Elements;

-      }

-    }

-    public T Select(ulong index) {

-      return elmts[index];

-    }

-    public T Select(long index) {

-      return elmts[index];

-    }

-    public T Select(uint index) {

-      return elmts[index];

-    }

-    public T Select(int index) {

-      return elmts[index];

-    }

-    public T Select(BigInteger index) {

-      return elmts[(int)index];

-    }

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

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

-      a[index] = t;

-      return new Sequence<T>(a);

-    }

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

-      return Update((long)index, t);

-    }

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

-      return Update((long)index, t);

-    }

-    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() {

-      if (elmts == null || elmts.Length == 0)

-        return 0;

-      var hashCode = 0;

-      for (var i = 0; i < elmts.Length; i++) {

-        hashCode = (hashCode << 3) | (hashCode >> 29) ^ elmts[i].GetHashCode();

-      }

-      return hashCode;

-    }

-    public override string ToString() {

-      if (elmts is char[]) {

-        var s = "";

-        foreach (var t in elmts) {

-          s += t.ToString();

-        }

-        return s;

-      } else {

-        var s = "[";

-        var sep = "";

-        foreach (var t in elmts) {

-          s += sep + t.ToString();

-          sep = ", ";

-        }

-        return s + "]";

-      }

-    }

-    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(long m) {

-      if (elmts.LongLength == m)

-        return this;

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

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

-      return new Sequence<T>(a);

-    }

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

-      return Take((long)n);

-    }

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

-      return Take((long)n);

-    }

-    public Sequence<T> Drop(long m) {

-      if (m == 0)

-        return this;

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

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

-      return new Sequence<T>(a);

-    }

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

-      return Drop((long)n);

-    }

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

-      if (n.IsZero)

-        return this;

-      return Drop((long)n);

-    }

-  }

-  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 QuantChar(bool frall, System.Predicate<char> pred) {

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

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

-      }

-      return frall;

-    }

-    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;

-      }

-    }

-    public static IEnumerable<char> AllChars {

-      get {

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

-          yield return (char)i;

-        }

-      }

-    }

-    public static IEnumerable<BigInteger> AllIntegers {

-      get {

-        yield return new BigInteger(0);

-        for (var j = new BigInteger(1);; j++) {

-          yield return j;

-          yield return -j;

-        }

-      }

-    }

-    public static IEnumerable<BigInteger> IntegerRange(BigInteger lo, BigInteger hi) {

-      for (var j = lo; j < hi; j++) {

-        yield return j;

-      }

-    }

-    // pre: b != 0

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

-    public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) {

-      return (sbyte)EuclideanDivision_int(a, b);

-    }

-    public static short EuclideanDivision_short(short a, short b) {

-      return (short)EuclideanDivision_int(a, b);

-    }

-    public static int EuclideanDivision_int(int a, int b) {

-      if (0 <= a) {

-        if (0 <= b) {

-          // +a +b: a/b

-          return (int)(((uint)(a)) / ((uint)(b)));

-        } else {

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

-          return -((int)(((uint)(a)) / ((uint)(unchecked(-b)))));

-        }

-      } else {

-        if (0 <= b) {

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

-          return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1;

-        } else {

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

-          return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1;

-        }

-      }

-    }

-    public static long EuclideanDivision_long(long a, long b) {

-      if (0 <= a) {

-        if (0 <= b) {

-          // +a +b: a/b

-          return (long)(((ulong)(a)) / ((ulong)(b)));

-        } else {

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

-          return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b)))));

-        }

-      } else {

-        if (0 <= b) {

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

-          return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1;

-        } else {

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

-          return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1;

-        }

-      }

-    }

-    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 sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) {

-      return (sbyte)EuclideanModulus_int(a, b);

-    }

-    public static short EuclideanModulus_short(short a, short b) {

-      return (short)EuclideanModulus_int(a, b);

-    }

-    public static int EuclideanModulus_int(int a, int b) {

-      uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b));

-      if (0 <= a) {

-        // +a: a % b'

-        return (int)(((uint)a) % bp);

-      } else {

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

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

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

-        uint c = ((uint)(unchecked(-a))) % bp;

-        return (int)(c == 0 ? c : bp - c);

-      }

-    }

-    public static long EuclideanModulus_long(long a, long b) {

-      ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b));

-      if (0 <= a) {

-        // +a: a % b'

-        return (long)(((ulong)a) % bp);

-      } else {

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

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

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

-        ulong c = ((ulong)(unchecked(-a))) % bp;

-        return (long)(c == 0 ? c : bp - c);

-      }

-    }

-    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;

-    }

-

-    public static U Let<T, U>(T t, Func<T,U> f) {

-      return f(t);

-    }

-

-    public delegate Result Function<Input,Result>(Input input);

-

-    public static A Id<A>(A a) {

-      return a;

-    }

-  }

-

-  public struct BigRational

-  {

-    public static readonly BigRational ZERO = new BigRational(0);

-

-    BigInteger num, den;  // invariant 1 <= den

-    public override string ToString() {

-      return string.Format("({0}.0 / {1}.0)", num, den);

-    }

-    public BigRational(int n) {

-      num = new BigInteger(n);

-      den = BigInteger.One;

-    }

-    public BigRational(BigInteger n, BigInteger d) {

-      // requires 1 <= d

-      num = n;

-      den = d;

-    }

-    public BigInteger ToBigInteger() {

-      if (0 <= num) {

-        return num / den;

-      } else {

-        return (num - den + 1) / den;

-      }

-    }

-    /// <summary>

-    /// Returns values such that aa/dd == a and bb/dd == b.

-    /// </summary>

-    private static void Normalize(BigRational a, BigRational b, out BigInteger aa, out BigInteger bb, out BigInteger dd) {

-      var gcd = BigInteger.GreatestCommonDivisor(a.den, b.den);

-      var xx = a.den / gcd;

-      var yy = b.den / gcd;

-      // We now have a == a.num / (xx * gcd) and b == b.num / (yy * gcd).

-      aa = a.num * yy;

-      bb = b.num * xx;

-      dd = a.den * yy;

-    }

-    public int CompareTo(BigRational that) {

-      // simple things first

-      int asign = this.num.Sign;

-      int bsign = that.num.Sign;

-      if (asign < 0 && 0 <= bsign) {

-        return 1;

-      } else if (asign <= 0 && 0 < bsign) {

-        return 1;

-      } else if (bsign < 0 && 0 <= asign) {

-        return -1;

-      } else if (bsign <= 0 && 0 < asign) {

-        return -1;

-      }

-      BigInteger aa, bb, dd;

-      Normalize(this, that, out aa, out bb, out dd);

-      return aa.CompareTo(bb);

-    }

-    public override int GetHashCode() {

-      return num.GetHashCode() + 29 * den.GetHashCode();

-    }

-    public override bool Equals(object obj) {

-      if (obj is BigRational) {

-        return this == (BigRational)obj;

-      } else {

-        return false;

-      }

-    }

-    public static bool operator ==(BigRational a, BigRational b) {

-      return a.CompareTo(b) == 0;

-    }

-    public static bool operator !=(BigRational a, BigRational b) {

-      return a.CompareTo(b) != 0;

-    }

-    public static bool operator >(BigRational a, BigRational b) {

-      return 0 < a.CompareTo(b);

-    }

-    public static bool operator >=(BigRational a, BigRational b) {

-      return 0 <= a.CompareTo(b);

-    }

-    public static bool operator <(BigRational a, BigRational b) {

-      return a.CompareTo(b) < 0;

-    }

-    public static bool operator <=(BigRational a, BigRational b) {

-      return a.CompareTo(b) <= 0;

-    }

-    public static BigRational operator +(BigRational a, BigRational b) {

-      BigInteger aa, bb, dd;

-      Normalize(a, b, out aa, out bb, out dd);

-      return new BigRational(aa + bb, dd);

-    }

-    public static BigRational operator -(BigRational a, BigRational b) {

-      BigInteger aa, bb, dd;

-      Normalize(a, b, out aa, out bb, out dd);

-      return new BigRational(aa - bb, dd);

-    }

-    public static BigRational operator -(BigRational a) {

-      return new BigRational(-a.num, a.den);

-    }

-    public static BigRational operator *(BigRational a, BigRational b) {

-      return new BigRational(a.num * b.num, a.den * b.den);

-    }

-    public static BigRational operator /(BigRational a, BigRational b) {

-      // Compute the reciprocal of b

-      BigRational bReciprocal;

-      if (0 < b.num) {

-        bReciprocal = new BigRational(b.den, b.num);

-      } else {

-        // this is the case b.num < 0

-        bReciprocal = new BigRational(-b.den, -b.num);

-      }

-      return a * bReciprocal;

-    }

-  }

-}

+using System; // for Func
+using System.Numerics;
+
+namespace Dafny
+{
+  using System.Collections.Generic;
+// set this option if you want to use System.Collections.Immutable and if you know what you're doing.
+#if DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE
+  using System.Collections.Immutable;
+  using System.Linq;
+
+  public class Set<T>
+  {
+    readonly ImmutableHashSet<T> setImpl;
+    Set(ImmutableHashSet<T> d) {
+      this.setImpl = d;
+    }
+    public static readonly Set<T> Empty = new Set<T>(ImmutableHashSet<T>.Empty);
+    public static Set<T> FromElements(params T[] values) {
+      return FromElements((IEnumerable<T>)values);
+    }
+    public static Set<T> FromElements(IEnumerable<T> values) {
+      var d = ImmutableHashSet<T>.Empty.ToBuilder();
+      foreach (T t in values)
+        d.Add(t);
+      return new Set<T>(d.ToImmutable());
+    }
+    public static Set<T> FromCollection(ICollection<T> values) {
+      var d = ImmutableHashSet<T>.Empty.ToBuilder();
+      foreach (T t in values)
+        d.Add(t);
+      return new Set<T>(d.ToImmutable());
+    }
+    public int Length {
+      get { return this.setImpl.Count; }
+    }
+    public long LongLength {
+      get { return this.setImpl.Count; }
+    }
+    public IEnumerable<T> Elements {
+      get {
+        return this.setImpl;
+      }
+    }
+    /// <summary>
+    /// This is an inefficient iterator for producing all subsets of "this".  Each set returned is the same
+    /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").
+    /// </summary>
+    public IEnumerable<Set<T>> AllSubsets {
+      get {
+        // Start by putting all set elements into a list
+        var elmts = new List<T>();
+        elmts.AddRange(this.setImpl);
+        var n = elmts.Count;
+        var which = new bool[n];
+        var s = ImmutableHashSet<T>.Empty.ToBuilder();
+        while (true) {
+          yield return new Set<T>(s.ToImmutable());
+          // "add 1" to "which", as if doing a carry chain.  For every digit changed, change the membership of the corresponding element in "s".
+          int i = 0;
+          for (; i < n && which[i]; i++) {
+            which[i] = false;
+            s.Remove(elmts[i]);
+          }
+          if (i == n) {
+            // we have cycled through all the subsets
+            break;
+          }
+          which[i] = true;
+          s.Add(elmts[i]);
+        }
+      }
+    }
+    public bool Equals(Set<T> other) {
+        return this.setImpl.SetEquals(other.setImpl);
+    }
+    public override bool Equals(object other) {
+        var otherSet = other as Set<T>;
+        return otherSet != null && this.Equals(otherSet);
+    }
+    public override int GetHashCode() {
+      var hashCode = 1;
+      foreach (var t in this.setImpl) {
+        hashCode = hashCode * (t.GetHashCode()+3);
+      }
+      return hashCode;
+    }
+    public override string ToString() {
+      var s = "{";
+      var sep = "";
+      foreach (var t in this.setImpl) {
+        s += sep + t.ToString();
+        sep = ", ";
+      }
+      return s + "}";
+    }
+    public bool IsProperSubsetOf(Set<T> other) {
+        return IsProperSubsetOf(other);
+    }
+    public bool IsSubsetOf(Set<T> other) {
+        return IsSubsetOf(other);
+    }
+    public bool IsSupersetOf(Set<T> other) {
+      return other.IsSupersetOf(this);
+    }
+    public bool IsProperSupersetOf(Set<T> other) {
+      return other.IsProperSupersetOf(this);
+    }
+    public bool IsDisjointFrom(Set<T> other) {
+      ImmutableHashSet<T> a, b;
+      if (this.setImpl.Count < other.setImpl.Count) {
+        a = this.setImpl; b = other.setImpl;
+      } else {
+        a = other.setImpl; b = this.setImpl;
+      }
+      foreach (T t in a) {
+        if (b.Contains(t))
+          return false;
+      }
+      return true;
+    }
+    public bool Contains(T t) {
+      return this.setImpl.Contains(t);
+    }
+    public Set<T> Union(Set<T> other) {
+        return new Set<T>(this.setImpl.Union(other.setImpl));
+    }
+    public Set<T> Intersect(Set<T> other) {
+      return new Set<T>(this.setImpl.Intersect(other.setImpl));
+    }
+    public Set<T> Difference(Set<T> other) {
+        return new Set<T>(this.setImpl.Except(other.setImpl));
+    }
+  }
+  public partial class MultiSet<T>
+  {
+
+    readonly ImmutableDictionary<T, int> dict;
+    MultiSet(ImmutableDictionary<T, int> d) {
+      dict = d;
+    }
+    public static readonly MultiSet<T> Empty = new MultiSet<T>(ImmutableDictionary<T, int>.Empty);
+    public static MultiSet<T> FromElements(params T[] values) {
+      var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+      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.ToImmutable());
+    }
+    public static MultiSet<T> FromCollection(ICollection<T> values) {
+      var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+      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.ToImmutable());
+    }
+    public static MultiSet<T> FromSeq(Sequence<T> values) {
+      var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+      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.ToImmutable());
+    }
+    public static MultiSet<T> FromSet(Set<T> values) {
+      var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+      foreach (T t in values.Elements) {
+        d[t] = 1;
+      }
+      return new MultiSet<T>(d.ToImmutable());
+    }
+
+    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() {
+      var hashCode = 1;
+      foreach (var kv in dict) {
+        var key = kv.Key.GetHashCode();
+        key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+        hashCode = hashCode * (key + 3);
+      }
+      return hashCode;
+    }
+    public override string ToString() {
+      var s = "multiset{";
+      var sep = "";
+      foreach (var kv in dict) {
+        var t = kv.Key.ToString();
+        for (int i = 0; i < kv.Value; i++) {
+          s += sep + t.ToString();
+          sep = ", ";
+        }
+      }
+      return s + "}";
+    }
+    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 = ImmutableDictionary<T, int>.Empty.ToBuilder();
+      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.ToImmutable());
+    }
+    public MultiSet<T> Intersect(MultiSet<T> other) {
+      if (dict.Count == 0)
+        return this;
+      else if (other.dict.Count == 0)
+        return other;
+      var r = ImmutableDictionary<T, int>.Empty.ToBuilder();
+      foreach (T t in dict.Keys) {
+        if (other.dict.ContainsKey(t)) {
+          r[t] = other.dict[t] < dict[t] ? other.dict[t] : dict[t];
+        }
+      }
+      return new MultiSet<T>(r.ToImmutable());
+    }
+    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 = ImmutableDictionary<T, int>.Empty.ToBuilder();
+      foreach (T t in dict.Keys) {
+        if (!other.dict.ContainsKey(t)) {
+          r[t] = dict[t];
+        } else if (other.dict[t] < dict[t]) {
+          r[t] = dict[t] - other.dict[t];
+        }
+      }
+      return new MultiSet<T>(r.ToImmutable());
+    }
+    public IEnumerable<T> Elements {
+      get {
+        foreach (T t in dict.Keys) {
+          int n;
+          dict.TryGetValue(t, out n);
+          for (int i = 0; i < n; i ++) {
+            yield return t;
+          }
+        }
+      }
+    }
+  }
+
+  public partial class Map<U, V>
+  {
+    readonly ImmutableDictionary<U, V> dict;
+    Map(ImmutableDictionary<U, V> d) {
+      dict = d;
+    }
+    public static readonly Map<U, V> Empty = new Map<U, V>(ImmutableDictionary<U, V>.Empty);
+    public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+      var d = ImmutableDictionary<U, V>.Empty.ToBuilder();
+      foreach (Pair<U, V> p in values) {
+        d[p.Car] = p.Cdr;
+      }
+      return new Map<U, V>(d.ToImmutable());
+    }
+    public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+      var d = ImmutableDictionary<U, V>.Empty.ToBuilder();
+      foreach (Pair<U, V> p in values) {
+        d[p.Car] = p.Cdr;
+      }
+      return new Map<U, V>(d.ToImmutable());
+    }
+    public int Length {
+      get { return dict.Count; }
+    }
+    public long LongLength {
+      get { return dict.Count; }
+    }
+    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() {
+      var hashCode = 1;
+      foreach (var kv in dict) {
+        var key = kv.Key.GetHashCode();
+        key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+        hashCode = hashCode * (key + 3);
+      }
+      return hashCode;
+    }
+    public override string ToString() {
+      var s = "map[";
+      var sep = "";
+      foreach (var kv in dict) {
+        s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();
+        sep = ", ";
+      }
+      return s + "]";
+    }
+    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) {
+      return new Map<U, V>(dict.SetItem(index, val));
+    }
+    public IEnumerable<U> Domain {
+      get {
+        return dict.Keys;
+      }
+    }
+  }
+#else // !def DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE
+  public class Set<T>
+  {
+    HashSet<T> set;
+    Set(HashSet<T> s) {
+      this.set = s;
+    }
+    public static Set<T> Empty {
+      get {
+        return new Set<T>(new HashSet<T>());
+      }
+    }
+    public static Set<T> FromElements(params T[] values) {
+      var s = new HashSet<T>();
+      foreach (T t in values)
+        s.Add(t);
+      return new Set<T>(s);
+    }
+    public static Set<T> FromCollection(ICollection<T> values) {
+      HashSet<T> s = new HashSet<T>();
+      foreach (T t in values)
+        s.Add(t);
+      return new Set<T>(s);
+    }
+    public int Length {
+      get { return this.set.Count; }
+    }
+    public long LongLength {
+      get { return this.set.Count; }
+    }
+    public IEnumerable<T> Elements {
+      get {
+        return this.set;
+      }
+    }
+    /// <summary>
+    /// This is an inefficient iterator for producing all subsets of "this".  Each set returned is the same
+    /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").
+    /// </summary>
+    public IEnumerable<Set<T>> AllSubsets {
+      get {
+        // Start by putting all set elements into a list
+        var elmts = new List<T>();
+        elmts.AddRange(this.set);
+        var n = elmts.Count;
+        var which = new bool[n];
+        var s = new Set<T>(new HashSet<T>());
+        while (true) {
+          yield return s;
+          // "add 1" to "which", as if doing a carry chain.  For every digit changed, change the membership of the corresponding element in "s".
+          int i = 0;
+          for (; i < n && which[i]; i++) {
+            which[i] = false;
+            s.set.Remove(elmts[i]);
+          }
+          if (i == n) {
+            // we have cycled through all the subsets
+            break;
+          }
+          which[i] = true;
+          s.set.Add(elmts[i]);
+        }
+      }
+    }
+    public bool Equals(Set<T> other) {
+      return this.set.Count == other.set.Count && IsSubsetOf(other);
+    }
+    public override bool Equals(object other) {
+      return other is Set<T> && Equals((Set<T>)other);
+    }
+    public override int GetHashCode() {
+      var hashCode = 1;
+      foreach (var t in this.set) {
+        hashCode = hashCode * (t.GetHashCode()+3);
+      }
+      return hashCode;
+    }
+    public override string ToString() {
+      var s = "{";
+      var sep = "";
+      foreach (var t in this.set) {
+        s += sep + t.ToString();
+        sep = ", ";
+      }
+      return s + "}";
+    }
+    public bool IsProperSubsetOf(Set<T> other) {
+      return this.set.Count < other.set.Count && IsSubsetOf(other);
+    }
+    public bool IsSubsetOf(Set<T> other) {
+      if (other.set.Count < this.set.Count)
+        return false;
+      foreach (T t in this.set) {
+        if (!other.set.Contains(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) {
+      HashSet<T> a, b;
+      if (this.set.Count < other.set.Count) {
+        a = this.set; b = other.set;
+      } else {
+        a = other.set; b = this.set;
+      }
+      foreach (T t in a) {
+        if (b.Contains(t))
+          return false;
+      }
+      return true;
+    }
+    public bool Contains(T t) {
+      return this.set.Contains(t);
+    }
+    public Set<T> Union(Set<T> other) {
+      if (this.set.Count == 0)
+        return other;
+      else if (other.set.Count == 0)
+        return this;
+      HashSet<T> a, b;
+      if (this.set.Count < other.set.Count) {
+        a = this.set; b = other.set;
+      } else {
+        a = other.set; b = this.set;
+      }
+      var r = new HashSet<T>();
+      foreach (T t in b)
+        r.Add(t);
+      foreach (T t in a)
+        r.Add(t);
+      return new Set<T>(r);
+    }
+    public Set<T> Intersect(Set<T> other) {
+      if (this.set.Count == 0)
+        return this;
+      else if (other.set.Count == 0)
+        return other;
+      HashSet<T> a, b;
+      if (this.set.Count < other.set.Count) {
+        a = this.set; b = other.set;
+      } else {
+        a = other.set; b = this.set;
+      }
+      var r = new HashSet<T>();
+      foreach (T t in a) {
+        if (b.Contains(t))
+          r.Add(t);
+      }
+      return new Set<T>(r);
+    }
+    public Set<T> Difference(Set<T> other) {
+      if (this.set.Count == 0)
+        return this;
+      else if (other.set.Count == 0)
+        return this;
+      var r = new HashSet<T>();
+      foreach (T t in this.set) {
+        if (!other.set.Contains(t))
+          r.Add(t);
+      }
+      return new Set<T>(r);
+    }
+  }
+  public class MultiSet<T>
+  {
+    Dictionary<T, int> dict;
+    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() {
+      var hashCode = 1;
+      foreach (var kv in dict) {
+        var key = kv.Key.GetHashCode();
+        key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+        hashCode = hashCode * (key + 3);
+      }
+      return hashCode;
+    }
+    public override string ToString() {
+      var s = "multiset{";
+      var sep = "";
+      foreach (var kv in dict) {
+        var t = kv.Key.ToString();
+        for (int i = 0; i < kv.Value; i++) {
+          s += sep + t.ToString();
+          sep = ", ";
+        }
+      }
+      return s + "}";
+    }
+    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;
+    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 int Length {
+      get { return dict.Count; }
+    }
+    public long LongLength {
+      get { return dict.Count; }
+    }
+    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() {
+      var hashCode = 1;
+      foreach (var kv in dict) {
+        var key = kv.Key.GetHashCode();
+        key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+        hashCode = hashCode * (key + 3);
+      }
+      return hashCode;
+    }
+    public override string ToString() {
+      var s = "map[";
+      var sep = "";
+      foreach (var kv in dict) {
+        s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();
+        sep = ", ";
+      }
+      return s + "]";
+    }
+    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;
+      }
+    }
+  }
+#endif
+  public class Sequence<T>
+  {
+    T[] elmts;
+    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 static Sequence<char> FromString(string s) {
+      return new Sequence<char>(s.ToCharArray());
+    }
+    public int Length {
+      get { return elmts.Length; }
+    }
+    public long LongLength {
+      get { return elmts.LongLength; }
+    }
+    public T[] Elements {
+      get {
+        return elmts;
+      }
+    }
+    public IEnumerable<T> UniqueElements {
+      get {
+        var st = Set<T>.FromElements(elmts);
+        return st.Elements;
+      }
+    }
+    public T Select(ulong index) {
+      return elmts[index];
+    }
+    public T Select(long index) {
+      return elmts[index];
+    }
+    public T Select(uint index) {
+      return elmts[index];
+    }
+    public T Select(int index) {
+      return elmts[index];
+    }
+    public T Select(BigInteger index) {
+      return elmts[(int)index];
+    }
+    public Sequence<T> Update(long index, T t) {
+      T[] a = (T[])elmts.Clone();
+      a[index] = t;
+      return new Sequence<T>(a);
+    }
+    public Sequence<T> Update(ulong index, T t) {
+      return Update((long)index, t);
+    }
+    public Sequence<T> Update(BigInteger index, T t) {
+      return Update((long)index, t);
+    }
+    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() {
+      if (elmts == null || elmts.Length == 0)
+        return 0;
+      var hashCode = 0;
+      for (var i = 0; i < elmts.Length; i++) {
+        hashCode = (hashCode << 3) | (hashCode >> 29) ^ elmts[i].GetHashCode();
+      }
+      return hashCode;
+    }
+    public override string ToString() {
+      if (elmts is char[]) {
+        var s = "";
+        foreach (var t in elmts) {
+          s += t.ToString();
+        }
+        return s;
+      } else {
+        var s = "[";
+        var sep = "";
+        foreach (var t in elmts) {
+          s += sep + t.ToString();
+          sep = ", ";
+        }
+        return s + "]";
+      }
+    }
+    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(long m) {
+      if (elmts.LongLength == m)
+        return this;
+      T[] a = new T[m];
+      System.Array.Copy(elmts, a, m);
+      return new Sequence<T>(a);
+    }
+    public Sequence<T> Take(ulong n) {
+      return Take((long)n);
+    }
+    public Sequence<T> Take(BigInteger n) {
+      return Take((long)n);
+    }
+    public Sequence<T> Drop(long m) {
+      if (m == 0)
+        return this;
+      T[] a = new T[elmts.Length - m];
+      System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+      return new Sequence<T>(a);
+    }
+    public Sequence<T> Drop(ulong n) {
+      return Drop((long)n);
+    }
+    public Sequence<T> Drop(BigInteger n) {
+      if (n.IsZero)
+        return this;
+      return Drop((long)n);
+    }
+  }
+  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 QuantChar(bool frall, System.Predicate<char> pred) {
+      for (int i = 0; i < 0x10000; i++) {
+        if (pred((char)i) != frall) { return !frall; }
+      }
+      return frall;
+    }
+    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;
+      }
+    }
+    public static IEnumerable<char> AllChars {
+      get {
+        for (int i = 0; i < 0x10000; i++) {
+          yield return (char)i;
+        }
+      }
+    }
+    public static IEnumerable<BigInteger> AllIntegers {
+      get {
+        yield return new BigInteger(0);
+        for (var j = new BigInteger(1);; j++) {
+          yield return j;
+          yield return -j;
+        }
+      }
+    }
+    public static IEnumerable<BigInteger> IntegerRange(BigInteger lo, BigInteger hi) {
+      for (var j = lo; j < hi; j++) {
+        yield return j;
+      }
+    }
+    // pre: b != 0
+    // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+    public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) {
+      return (sbyte)EuclideanDivision_int(a, b);
+    }
+    public static short EuclideanDivision_short(short a, short b) {
+      return (short)EuclideanDivision_int(a, b);
+    }
+    public static int EuclideanDivision_int(int a, int b) {
+      if (0 <= a) {
+        if (0 <= b) {
+          // +a +b: a/b
+          return (int)(((uint)(a)) / ((uint)(b)));
+        } else {
+          // +a -b: -(a/(-b))
+          return -((int)(((uint)(a)) / ((uint)(unchecked(-b)))));
+        }
+      } else {
+        if (0 <= b) {
+          // -a +b: -((-a-1)/b) - 1
+          return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1;
+        } else {
+          // -a -b: ((-a-1)/(-b)) + 1
+          return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1;
+        }
+      }
+    }
+    public static long EuclideanDivision_long(long a, long b) {
+      if (0 <= a) {
+        if (0 <= b) {
+          // +a +b: a/b
+          return (long)(((ulong)(a)) / ((ulong)(b)));
+        } else {
+          // +a -b: -(a/(-b))
+          return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b)))));
+        }
+      } else {
+        if (0 <= b) {
+          // -a +b: -((-a-1)/b) - 1
+          return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1;
+        } else {
+          // -a -b: ((-a-1)/(-b)) + 1
+          return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1;
+        }
+      }
+    }
+    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 sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) {
+      return (sbyte)EuclideanModulus_int(a, b);
+    }
+    public static short EuclideanModulus_short(short a, short b) {
+      return (short)EuclideanModulus_int(a, b);
+    }
+    public static int EuclideanModulus_int(int a, int b) {
+      uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b));
+      if (0 <= a) {
+        // +a: a % b'
+        return (int)(((uint)a) % bp);
+      } else {
+        // c = ((-a) % b')
+        // -a: b' - c if c > 0
+        // -a: 0 if c == 0
+        uint c = ((uint)(unchecked(-a))) % bp;
+        return (int)(c == 0 ? c : bp - c);
+      }
+    }
+    public static long EuclideanModulus_long(long a, long b) {
+      ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b));
+      if (0 <= a) {
+        // +a: a % b'
+        return (long)(((ulong)a) % bp);
+      } else {
+        // c = ((-a) % b')
+        // -a: b' - c if c > 0
+        // -a: 0 if c == 0
+        ulong c = ((ulong)(unchecked(-a))) % bp;
+        return (long)(c == 0 ? c : bp - c);
+      }
+    }
+    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>((T[])array.Clone());
+    }
+    // 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;
+    }
+
+    public static U Let<T, U>(T t, Func<T,U> f) {
+      return f(t);
+    }
+
+    public delegate Result Function<Input,Result>(Input input);
+
+    public static A Id<A>(A a) {
+      return a;
+    }
+  }
+
+  public struct BigRational
+  {
+    public static readonly BigRational ZERO = new BigRational(0);
+
+    BigInteger num, den;  // invariant 1 <= den
+    public override string ToString() {
+      return string.Format("({0}.0 / {1}.0)", num, den);
+    }
+    public BigRational(int n) {
+      num = new BigInteger(n);
+      den = BigInteger.One;
+    }
+    public BigRational(BigInteger n, BigInteger d) {
+      // requires 1 <= d
+      num = n;
+      den = d;
+    }
+    public BigInteger ToBigInteger() {
+      if (0 <= num) {
+        return num / den;
+      } else {
+        return (num - den + 1) / den;
+      }
+    }
+    /// <summary>
+    /// Returns values such that aa/dd == a and bb/dd == b.
+    /// </summary>
+    private static void Normalize(BigRational a, BigRational b, out BigInteger aa, out BigInteger bb, out BigInteger dd) {
+      var gcd = BigInteger.GreatestCommonDivisor(a.den, b.den);
+      var xx = a.den / gcd;
+      var yy = b.den / gcd;
+      // We now have a == a.num / (xx * gcd) and b == b.num / (yy * gcd).
+      aa = a.num * yy;
+      bb = b.num * xx;
+      dd = a.den * yy;
+    }
+    public int CompareTo(BigRational that) {
+      // simple things first
+      int asign = this.num.Sign;
+      int bsign = that.num.Sign;
+      if (asign < 0 && 0 <= bsign) {
+        return 1;
+      } else if (asign <= 0 && 0 < bsign) {
+        return 1;
+      } else if (bsign < 0 && 0 <= asign) {
+        return -1;
+      } else if (bsign <= 0 && 0 < asign) {
+        return -1;
+      }
+      BigInteger aa, bb, dd;
+      Normalize(this, that, out aa, out bb, out dd);
+      return aa.CompareTo(bb);
+    }
+    public override int GetHashCode() {
+      return num.GetHashCode() + 29 * den.GetHashCode();
+    }
+    public override bool Equals(object obj) {
+      if (obj is BigRational) {
+        return this == (BigRational)obj;
+      } else {
+        return false;
+      }
+    }
+    public static bool operator ==(BigRational a, BigRational b) {
+      return a.CompareTo(b) == 0;
+    }
+    public static bool operator !=(BigRational a, BigRational b) {
+      return a.CompareTo(b) != 0;
+    }
+    public static bool operator >(BigRational a, BigRational b) {
+      return 0 < a.CompareTo(b);
+    }
+    public static bool operator >=(BigRational a, BigRational b) {
+      return 0 <= a.CompareTo(b);
+    }
+    public static bool operator <(BigRational a, BigRational b) {
+      return a.CompareTo(b) < 0;
+    }
+    public static bool operator <=(BigRational a, BigRational b) {
+      return a.CompareTo(b) <= 0;
+    }
+    public static BigRational operator +(BigRational a, BigRational b) {
+      BigInteger aa, bb, dd;
+      Normalize(a, b, out aa, out bb, out dd);
+      return new BigRational(aa + bb, dd);
+    }
+    public static BigRational operator -(BigRational a, BigRational b) {
+      BigInteger aa, bb, dd;
+      Normalize(a, b, out aa, out bb, out dd);
+      return new BigRational(aa - bb, dd);
+    }
+    public static BigRational operator -(BigRational a) {
+      return new BigRational(-a.num, a.den);
+    }
+    public static BigRational operator *(BigRational a, BigRational b) {
+      return new BigRational(a.num * b.num, a.den * b.den);
+    }
+    public static BigRational operator /(BigRational a, BigRational b) {
+      // Compute the reciprocal of b
+      BigRational bReciprocal;
+      if (0 < b.num) {
+        bReciprocal = new BigRational(b.den, b.num);
+      } else {
+        // this is the case b.num < 0
+        bReciprocal = new BigRational(-b.den, -b.num);
+      }
+      return a * bReciprocal;
+    }
+  }
+}