val N:ℕ;
val M:ℕ;
axiom notZero ⇔ N > 0;
  
type int   = ℤ[-N,N];
type elem  = ℤ[-M,M];
type array = Array[N,elem];

proc minimumElement(a:array): elem
{
  var m:elem ≔ a[0];
  for var i:int ≔ 1; i < N; i ≔ i+1 do
  {
    if a[i] < m then m ≔ a[i];
  }
  return m;
}

proc minimumIndex(a:array): int
{
  var m:elem ≔ a[0];
  var p:int ≔ 0;
  for var i:int ≔ 1; i < N; i ≔ i+1 do
  {
    if a[i] < m then 
    {
      m ≔ a[p];
      p ≔ i;
    }
  }
  return p;
}

proc main(): ()
{
  // execution for N=5 and M=3
  val a = Array[N,elem](1,2,3,0,2);
  print a, minimumElement(a);
  print a, minimumIndex(a);
}