// has(a, n, x) <=> x occurs among the first n elements of a
/*@
  theory uses Base {
    int: TYPE = Base.int;
    intArray: TYPE = Base.IntArray;
    has: PREDICATE(intArray, int, int) =
      PRED(a:intArray, n:int, x:int):
        EXISTS(k:INT): 0 <= k AND k < n AND a.value[k] = x;
  }
@*/
class Exercise6 
{
  // removes duplicates from 'a' moving the non-duplicates to the front of 'a'
  // returns the number of distinct elements (all now at the beginning of 'a')
  public static int toSet(int[] a) 
  {
    int n = 0;
    int i = 0;
    while (i < a.length) 
    {
      boolean h = has(a, n, a[i]);
      if (!h)
      {
        a[n] = a[i];
        n = n+1;
      }
      i = i+1;
    }
    return n;
  }
  
  // true if and only if 'x' occurs among the first n elements of 'a'
  public static boolean has(int[] a, int n, int x) 
  {
    int i = 0;
    boolean result = false;
    while (i < n && !result) 
    {
      if (a[i] == x) 
        result = true;
      else
        i = i+1;
    }
    return result;
  }
}