val N:ℕ;
val M:ℕ; 

type int   = ℤ[-1,N];
type elem  = ℕ[M];
type array = Array[N,elem];

// we construct from array "a" a new array as follows: we remove the
// element at position "p", shifting all elements at positions greater 
// "p" one position to the left, and filling the gap at the the end
// by the new element "x" (the new array has the same length as "a")
proc remove(a:array,p:int,x:elem): array
{
  var b:array = Array[N,elem](0);
  var i:int ≔ 0;
  while i < p do
  {
    b[i] ≔ a[i]; 
    i ≔ i+1;
  }
  while i < N-1 do
  {
    b[i] ≔ a[i+1]; 
    i ≔ i+1;
  }
  b[N-1] ≔ x;
  return b;
}