val N:ℕ;
val M:ℕ;

type index = ℤ[-N,N];
type elem  = ℤ[-M,M];
type array = Array[N,elem];

proc maximumValue(a:array): elem
{
  var m:elem ≔ -1;
  for i:index with 0 ≤ i ∧ i < N do
  {
    if a[i] > m then m ≔ a[i];
  }
  return m;
}

proc maximumIndex(a:array): index
{
  var m:elem = -1;
  var p:index;
  for i:index with 0 ≤ i ∧ i < N do
  {
    if a[i] > m then 
    {
      p ≔ i;
      m ≔ a[p];
    }
  }
  return p;
}