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 shift
// the first "n" elements "r" positions to the left (dropping
// the first "r" elements and filling the resulting gaps with 0).
// the elements at positions greater equal "n" remain unchanged.
proc shiftLeft(a:array,n:int,r:int): array
{
  var b:array = a;
  var i:int ≔ 0;
  while i < n do
  {
    if i < n-r then
      b[i] ≔ a[i+r];
    else if i < n then
      b[i] ≔ 0; 
    i ≔ i+1;
  }
  return b;
}