/*@predicate descending(unsigned N, unsigned *tab) = \valid(tab+(0..N-1)) 
  && \forall unsigned r1, unsigned r2; 0 <= r1 <= r2 < N ==> tab[r1] >= tab[r2];

  @predicate reduced(unsigned n, unsigned *orig, unsigned *red) = 
  descending(n, orig) && 
  descending(n, red) && 
  \forall unsigned r; 0 <= r < n ==> red[r] == orig[r] - orig[n-1];
 */

/*@ requires descending(n, tab);
  @ terminates \true;
  @ assigns tab+(0..n-1);
  @ ensures reduced(n, \old(tab), \result);
 */
unsigned *reduce(unsigned n, unsigned *tab)
{
    unsigned r;
    for (r = 0; r<n; r++)
    {
	tab[r] -= tab[n-1];
    }
    return tab;
}

int main()
{
    return 0;
}