global: a == a0 
static int search(int a[], int v)
  {
  for( int i = 0; i < a.length; i++ )
    {
    if( a[i] == v )
      { r = i;
      return i; a[r] == v
      } ((   k < i + 1) a[k] != v ô i < a.length)
    } r = -1;
  return -1; (("k) a[k] != v) ^ r == -1
  }
 [(($i) a[i] == v) ¨ a[r] == v] ^ [(("i) a[i] != v) ¨ r == -1]
Proving the Assertions (1)
Text Box: A
(("k < i) a[k] != v ô i < a.length)