The following function computes John McCarthy's "91" function, in a non recursive way.

Show that it terminates, by providing a suitable variant for the while loop.

Hint: Why3 supports lexicographic variants, with syntax variant { t1, t2 }

use int.Int

let f91 (n0: int): int
= let ref e = 1 in
  let ref n = n0 in
  while e > 0 do
    variant { 101 - n + 10 * e, e }
    if n > 100 then begin
      n <- n - 10;
      e <- e - 1
    end else begin
      n <- n + 11;
      e <- e + 1
    end
  done;
  return n