sort color = {a:int | 0 <= a <= 1}

union tree with (color, nat, nat, nat) { /* color, black height, violation, size */
  E(0, 0, 0, 0);

  {cl:color,cr:color,bh:nat,sl:nat,sr:nat}
  B(0, bh+1, 0, sl+sr+1) of tree(cl, bh, 0, sl) * int * tree(cr, bh, 0, sr);

  {cl:color,cr:color,bh:nat,sl:nat,sr:nat}
  R(1, bh, cl+cr, sl+sr+1) of tree(cl, bh, 0, sl) * int * tree(cr, bh, 0, sr)
}

/* exception Item_already_exists */

{cl:color,cr:color,bh:nat,vl: nat,vr:nat | vl+vr <= 1,sl:nat,sr:nat}
[c:color] tree(c, bh+1, 0, sl+sr+1)
restore (left: tree(cl, bh, vl, sl), key: int, right: tree(cr, bh, vr, sr)) {
  var: tree a, b, c, d; int x, y;;

  switch (left, right) {         
  case (R(R(a, x, b), y, c), d): return R(B(a, x, b), y, B(c, key, d));
  case (R(a, x, R(b, y, c)), d): return R(B(a, x, b), y, B(c, key, d));
  case (a, R(R(b, x, c), y, d)): return R(B(a, key, b), x, B(c, y, d));
  case (a, R(b, x, R(c, y, d))): return R(B(a, key, b), x, B(c, y, d));
/*
  case (a, b): return B(a, key, b);
*/
  }
}

{c:color,bh:nat,s:nat}
[c1:color,v:nat | v <= c] tree(c1, bh, v, s+1)
ins (key: int, tree: tree(c, bh, 0, s)) {
  var: tree a, b; int x;;

  switch (tree) {
  case E: return R(E, key, E);
  case B(a, x, b):
    if (key < x) { a = ins(key, a); return restore(a, x, b); }
    else if (x < key) { b = ins(key, b); return restore(a, x, b); }
    else { exit; }
    case R(a, x, b):
    if (key < x) { a = ins(key, a); return R(a, x, b); }
    else if (x < key) { a = ins(key, a); return R(a, x, b); }
    else { exit; };
  }
}

{c:color,bh:nat,s:nat}
[bh:nat] tree(0, bh, 0, s+1)
insert (key: int, tree: tree(c, bh, 0, s)) {
  var: tree a, b; int x;;

  switch (ins(key, tree)) {
  case R(a, x, b): return B(a, x, b);
  case B(a, x, b): return B(a, x, b);
  }
}