/*@
  axiomatic A
  {
    logic integer
    F(int* a, integer m, integer n, int v) =
      (n <= m) ? 
       0 : ((0 <= F(a, m, n-1, v) < n-m-1) ?
         F(a, m, n-1, v) : ((a[n-1] != v) ? n-m-1 : n-m));
  }

  logic integer
  Fix(int* a, integer x, integer n, int v) = x + F(a, x, n, v);

  logic integer
  R(int* a, integer n, int v, integer p) =
    \let c = n;
    \let x = R(a, n, v, p-1) + 1;
      p < 0 ? -1 : // 0 <= p
        (n <= 0 ? 0 : // 0 < n
          p < c ? x + F(a, x, n, v) : n
          //p < c ? Fix(a, x, n, v) : n
        );

  lemma R_1:
    \forall int *a, v, integer n, p;
      \let x = R(a, n, v, p-1) + 1;
      0 <= n      ==>
      0 <= p < n  ==> 
      R(a, n, v, p) == x + F(a, x, n, v);

  lemma R_2:
    \forall int *a, v, integer i, n, p;
      0 < n       ==>
      0 <= p < n  ==>
      0 <= R(a, n, v, p);
*/