/*@ predicate canSee(integer N, int *x, integer i) =
  @   \forall integer j; i < j < N ==> x[i] > x[j];
  @*/

/*@ predicate countRangeFrom(integer N, int *x, integer i, integer c) =
  @   i >= N ? c == 0 :
  @   canSee(N, x, i) ? countRange(N, x, i+1, c-1)
  @                   : countRange(N, x, i+1, c);
  @*/

/*@ requires  N > 0;
  @ requires  \valid(x + (0..N-1));
  @ assigns   \nothing;
  @ ensures   countRange(N, x, 0, \result);
  @*/
int countWhoCanSee (int N, int x[]) {
	int tallest = x[N-1];
	int count = 1;
  /*@ TRY TO FILL THIS ???
    @*/
  for (int i = N-2; i >= 0; i--)
		if (tallest < x[i]) {
			tallest = x[i];
			count++;
		}
	return count;
}