val N:ℕ;
val M = 1;

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

fun num(a:array,e:elem):int = #k:int with 0 ≤ k ∧ k < N ∧ a[k] = e;

proc arrange(a:array):array
{
  var b:array ≔ a; var i:int ≔ 0; var j:int ≔ N-1;
  while i < j do
  {
    if b[i] = 0 then 
      i ≔ i+1;
    else if b[j] = 1 then
      j ≔ j-1;
    else
    { 
      var e:elem ≔ b[i]; b[i] ≔ b[j]; b[j] ≔ e; 
      i ≔ i+1; j ≔ j-1;
    }
  }
  return b;
}