// MULTIMI
// set (multime finita)
// iset (multime potential infinita)

function seqAsSet(s : seq<int>) : set<int>
{
  if |s| == 0 then
  {}
  else
  { s[0] } + seqAsSet(s[1..])
}

method Main()
{
  var x : set<int> := { 1, 1, 2, 3 };
  assert 1 in x;
  assert 5 !in x;
  var y : set<int> := { 3, 4, 5 };
  var z := x + y;
  assert 5 in z;
  assert 7 !in z;
  print x, "\n";
  var empty : set<int> := {};
  assert forall x : int :: x !in empty;
  var z' := x * y;
  assert z' == { 3 };
  var z'' := y - x;
  assert z'' == { 4, 5 };
  assert x - y == { 1, 2, 2, 2, 2, 2 };
  assert { 1, 2 } <= { 1, 2, 3 };
  assert { 1, 2 } < { 1, 2, 3 };
  assert { 1, 2, 3 } <= { 1, 2, 3 };
  assert !({ 1, 2, 3 } < { 1, 2, 3 });
  assert { 1, 2, 3 } !! { 4, 5, 6 };
  assert !({ 1, 2, 3 } !! { 3, 4, 5, 6 });
  assert | { 1, 1, 2, 3 } | == 3;
  print "seqAsSet: ", seqAsSet([1, 3, 2, 1, 3]), "\n";
  //var s : set<int> := set x : int | 0 <= x < 10 :: x * x;
  //print s, "\n";
  ghost var s' : iset<int> := iset x : int | x < 100;
  ghost var s'' : iset<int> := iset x : int | x > 0;
  ghost var s''' : iset<int> := s' * s'';
  assert 55 in s''';
  //assert -100 in s''';
  assert 99 in s';
  assert -19291293921327136729178372183721831 in s';
  //assert 101 in s';
  //print s', "\n";
}