/*
{i:nat} /* metric: ( i==91, max(0, 101-i), i) */
int(91)
ninetyone (x: int(i)) {
  if ( x == 91) {
    return 91;
  } else if (x <= 100) {
    return ninetyone (ninetyone (x+11));
  } else {
    return ninetyone (x-10);
  }
}
*/

{i:nat}
[j:int | (i <= 100 /\ j = 91) \/ (i > 100 /\ j = i-10)] int(j)
ninetyone (x:int(i)) {
  if (x <= 100) {
    return ninetyone (ninetyone (x+11));
  } else {
   return (x-10);
  }
}